-- 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.inl
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝ : CommMonoid β
ih :
  ∀ t ⊂ ∅,
    ∀ (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 ∈ ∅ → α
hg₁ : ∀ (a : α) (ha : a ∈ ∅), f a * f (g a ha) = 1
hg₃ : ∀ (a : α) (ha : a ∈ ∅), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : α) (ha : a ∈ ∅), g a ha ∈ ∅
hg₄ : ∀ (a : α) (ha : a ∈ ∅), g (g a ha) ⋯ = a
⊢ ∏ x ∈ ∅, f x = 1

Tactic:
simp

Result:
no goals

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, f x = 1

Tactic:
suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1 by
  rw [← prod_sdiff this, h, one_mul]
  cases eq_or_ne (g x hx) x with
  | inl hx' => simpa [hx'] using hg₃ x hx
  | inr hx' => rw [prod_pair hx'.symm, 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
⊢ ∏ x ∈ s \ {x, g x hx}, f x = 1

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
⊢ False

Tactic:
have : g (g a ha₁) (g_mem _ _) = g (g x hx) (g_mem _ _) := by simp only [h]

Result:
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

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
a : α
ha₁ : a ∈ s
ha₂ : ¬a = x
ha₃ : ¬a = g x hx
h : g a ⋯ = g x hx
⊢ g (g a ha₁) ⋯ = g (g x hx) ⋯

Tactic:
simp only [h]

Result:
no goals

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
⊢ ∀ (a : α) (ha : a ∈ s ∧ ¬a = x ∧ ¬a = g x hx), ¬g a ⋯ = x ∧ ¬g a ⋯ = g x hx

Tactic:
rintro a ⟨ha₁, ha₂, ha₃⟩

Result:
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
⊢ ¬g a ⋯ = x ∧ ¬g a ⋯ = g x hx