-- 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 inr
α : 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
hx' : g x hx ≠ x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
rw [prod_pair hx'.symm, 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 ∈ s, f x = 1

Tactic:
rw [← prod_sdiff this, h, one_mul]

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

Proof state:
case inl
α : 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
hx' : g x hx = x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
simpa [hx'] using hg₃ x 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
⊢ ¬g a ⋯ = x ∧ ¬g a ⋯ = g x hx

Tactic:
refine ⟨fun h => by simp [← h, hg₄] at ha₃, fun 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
⊢ False

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
⊢ ∏ x ∈ s, f x = 1

Tactic:
have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]

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, 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
⊢ {x, g x hx} ⊆ s

Tactic:
simp [insert_subset_iff, hx, g_mem]

Result:
no goals