-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β}
    (i : ∀ a ∈ s, f a ≠ 1 → γ) (hi : ∀ a h₁ h₂, i a h₁ h₂ ∈ t)
    (i_inj : ∀ a₁ h₁₁ h₁₂ a₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, i a h₁ h₂ = b) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x

Proof state:
case calc_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a : α
ha : a ∈ filter (fun x => f x ≠ 1) s
h₁ : a ∈ s
h₂ : f a ≠ 1
⊢ (fun a ha => i a ⋯ ⋯) a ha ∈ filter (fun x => g x ≠ 1) t

Tactic:
refine (mem_filter.mpr ⟨hi a h₁ _, ?_⟩)

Result:
case calc_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a : α
ha : a ∈ filter (fun x => f x ≠ 1) s
h₁ : a ∈ s
h₂ : f a ≠ 1
⊢ g ((fun a ha => i a ⋯ ⋯) a ha) ≠ 1

Proof state:
case calc_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a₁ : α
ha₁ : a₁ ∈ filter (fun x => f x ≠ 1) s
a₂ : α
ha₂ : a₂ ∈ filter (fun x => f x ≠ 1) s
⊢ (fun a ha => i a ⋯ ⋯) a₁ ha₁ = (fun a ha => i a ⋯ ⋯) a₂ ha₂ → a₁ = a₂

Tactic:
refine (mem_filter.mp ha₁).elim fun _ha₁₁ _ha₁₂ ↦ ?_

Result:
case calc_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a₁ : α
ha₁ : a₁ ∈ filter (fun x => f x ≠ 1) s
a₂ : α
ha₂ : a₂ ∈ filter (fun x => f x ≠ 1) s
_ha₁₁ : a₁ ∈ s
_ha₁₂ : f a₁ ≠ 1
⊢ (fun a ha => i a ⋯ ⋯) a₁ ha₁ = (fun a ha => i a ⋯ ⋯) a₂ ha₂ → a₁ = a₂

Proof state:
case calc_3
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : γ
hb : b ∈ filter (fun x => g x ≠ 1) t
h₁ : b ∈ t
h₂ : g b ≠ 1
⊢ ∃ a, ∃ (ha : a ∈ filter (fun x => f x ≠ 1) s), (fun a ha => i a ⋯ ⋯) a ha = b

Tactic:
obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂

Result:
case calc_3.intro.intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : γ
hb : b ∈ filter (fun x => g x ≠ 1) t
h₁ : b ∈ t
h₂ : g b ≠ 1
a : α
ha₁ : a ∈ s
ha₂ : f a ≠ 1
eq : i a ha₁ ha₂ = b
⊢ ∃ a, ∃ (ha : a ∈ filter (fun x => f x ≠ 1) s), (fun a ha => i a ⋯ ⋯) a ha = b

Proof state:
case calc_4
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : α) (ha : a ∈ filter (fun x => f x ≠ 1) s), f a = g ((fun a ha => i a ⋯ ⋯) a ha)

Tactic:
refine (fun a ha => (mem_filter.mp ha).elim fun h₁ h₂ ↦ ?_)

Result:
case calc_4
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
i : (a : α) → a ∈ s → f a ≠ 1 → γ
hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a : α
ha : a ∈ filter (fun x => f x ≠ 1) s
h₁ : a ∈ s
h₂ : f a ≠ 1
⊢ f a = g ((fun a ha => i a ⋯ ⋯) a ha)