Theorem: Finset.noncommProd_eq_one (Jordan/ConjClassCount.lean)

State before:
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hf : ∀ a ∈ s, f a = 1
⊢ Finset.noncommProd s f comm = 1
Tactic:
induction s using Finset.induction_on with
| empty => simp only [Finset.noncommProd_empty]
| insert ha hs =>
    rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha]
    rw [hf _ (Finset.mem_insert_self _ _), one_mul]
    apply hs
    intro a ha
    exact hf _ (Finset.mem_insert_of_mem ha)
State after:
no goals

State before:
case empty
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
comm : Set.Pairwise ↑∅ fun a b => Commute (f a) (f b)
hf : ∀ a ∈ ∅, f a = 1
⊢ Finset.noncommProd ∅ f comm = 1
Tactic:
simp only [Finset.noncommProd_empty]
State after:
no goals

State before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd (insert a✝ s✝) f comm = 1
Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ ha]
State after:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ f a✝ * Finset.noncommProd s✝ f ⋯ = 1

State before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ f a✝ * Finset.noncommProd s✝ f ⋯ = 1
Tactic:
rw [hf _ (Finset.mem_insert_self _ _), one_mul]
State after:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd s✝ f ⋯ = 1

State before:
case insert
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ Finset.noncommProd s✝ f ⋯ = 1
Tactic:
apply hs
State after:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ ∀ a ∈ s✝, f a = 1

State before:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
⊢ ∀ a ∈ s✝, f a = 1
Tactic:
intro a ha
State after:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha✝ : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
a : α
ha : a ∈ s✝
⊢ f a = 1

State before:
case insert.hf
α✝ : Type ?u.304426
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
g : Equiv.Perm α✝
α : Type u_3
inst✝¹ : DecidableEq α
β : Type u_4
inst✝ : Monoid β
f : α → β
a✝ : α
s✝ : Finset α
ha✝ : a✝ ∉ s✝
hs : ∀ (comm : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)), (∀ a ∈ s✝, f a = 1) → Finset.noncommProd s✝ f comm = 1
comm : Set.Pairwise ↑(insert a✝ s✝) fun a b => Commute (f a) (f b)
hf : ∀ a ∈ insert a✝ s✝, f a = 1
a : α
ha : a ∈ s✝
⊢ f a = 1
Tactic:
exact hf _ (Finset.mem_insert_of_mem ha)
State after:
no goals