-- 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
⊢ ∀ (a : α) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}

Tactic:
simp only [mem_sdiff, mem_insert, mem_singleton, not_or, g_mem, true_and]

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 ∧ ¬a = x ∧ ¬a = g x hx), ¬g a ⋯ = x ∧ ¬g a ⋯ = g x hx

Proof state:
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

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

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

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
⊢ ∏ 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
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) ⋯
⊢ a = x

Tactic:
simpa [hg₄] using this

Result:
no goals

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 ⋯ = x
⊢ False

Tactic:
simp [← h, hg₄] at ha₃

Result:
no goals

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}
⊢ ∀ (a : α) (ha : a ∈ s \ {x, g x hx}), f a * f (g a ⋯) = 1

Tactic:
simp [hg₁]

Result:
no goals

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 : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
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:
no goals