-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- The difference with `Finset.prod_ninvolution` is that the involution is allowed to use
membership of the domain of the product, rather than being a non-dependent function. -/
@[to_additive "The difference with `Finset.sum_ninvolution` is that the involution is allowed to use
membership of the domain of the sum, rather than being a non-dependent function."]
lemma prod_involution (g : ∀ a ∈ s, α) (hg₁ : ∀ a ha, f a * f (g a ha) = 1)
    (hg₃ : ∀ a ha, f a ≠ 1 → g a ha ≠ a)
    (g_mem : ∀ a ha, g a ha ∈ s) (hg₄ : ∀ a ha, g (g a ha) (g_mem a ha) = a) :
    ∏ x ∈ s, f x = 1

Proof state:
case H.inr.intro
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : α) → a ∈ t → α),
      (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t), (∀ (a : α) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
x : α
hx : x ∈ s
this : {x, g x hx} ⊆ s
⊢ ∏ x ∈ s \ {x, g x hx}, f x = 1

Tactic:
suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
  ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
    (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃ (fun _ _ => hg₄ _ _)

Result:
case H.inr.intro
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : α) → a ∈ t → α),
      (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t), (∀ (a : α) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
x : α
hx : x ∈ s
this : {x, g x hx} ⊆ s
⊢ ∀ (a : α) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
⊢ ∏ x ∈ s, f x = 1

Tactic:
induction s using Finset.strongInduction with | H s ih => ?_

Result:
case H
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : α) → a ∈ t → α),
      (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t), (∀ (a : α) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
⊢ ∏ x ∈ s, f x = 1

Proof state:
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : α) → a ∈ t → α),
      (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t), (∀ (a : α) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
x : α
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : α) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ x ∉ s \ {x, g x hx} ∧ insert x (s \ {x, g x hx}) ⊆ s

Tactic:
simp [insert_subset_iff, hx]

Result:
no goals

Proof state:
case H.inr.intro.intro.intro
α : Type u_3
β : Type u_4
s✝ : Finset α
f : α → β
inst✝ : CommMonoid β
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : α) → a ∈ t → α),
      (∀ (a : α) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : α) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : α) (ha : a ∈ t), g a ha ∈ t), (∀ (a : α) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : α) → a ∈ s → α
hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a
x : α
hx : x ∈ s
this✝ : {x, g x hx} ⊆ s
a : α
ha₁ : a ∈ s
ha₂ : ¬a = x
ha₃ : ¬a = g x hx
h : g a ⋯ = g x hx
this : g (g a ha₁) ⋯ = g (g x hx) ⋯
⊢ False

Tactic:
exact ha₂ (by simpa [hg₄] using this)

Result:
no goals