case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂

case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
⊢ ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
⊢ ∏ x in s, f x = ∏ x in t, g x
refine' prod_bij i hi h _ _
case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
a1 a2 : α
h1 : a1 ∈ s
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2
case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
intro a1 a2 h1 h2 eq
case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
a1 a2 : α
h1 : a1 ∈ s
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) (_ : i a1 h1 ∈ t) = j (i a2 h2) (_ : i a2 h2 ∈ t)
case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
a1 a2 : α
h1 : a1 ∈ s
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2
rw [← left_inv a1 h1, ← left_inv a2 h2]
no goals
case refine'_1
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
a1 a2 : α
h1 : a1 ∈ s
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) (_ : i a1 h1 ∈ t) = j (i a2 h2) (_ : i a2 h2 ∈ t)
simp only [eq]
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ ∃ a ha, b = i a ha
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
⊢ ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha
intro b hb
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ ∃ ha, b = i (j b hb) ha
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ ∃ a ha, b = i a ha
use j b hb
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ b = i (j b hb) (_ : j b hb ∈ s)
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ ∃ ha, b = i (j b hb) ha
use hj b hb
no goals
case refine'_2
ι : Type ?u.315211
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → γ
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
j : (a : γ) → a ∈ t → α
hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (_ : i a ha ∈ t) = a
right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (_ : j a ha ∈ s) = a
b : γ
hb : b ∈ t
⊢ b = i (j b hb) (_ : j b hb ∈ s)
exact (right_inv b hb).symm