-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem ker_noncommProd_eq_of_supIndep_ker [FiniteDimensional K V] {ι : Type*} {f : ι → V →ₗ[K] V}
    (s : Finset ι) (comm) (h : s.SupIndep fun i ↦ ker (f i)) :
    ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i)

Proof state:
case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ Disjoint (ker (f i)) (ker (s.noncommProd f ⋯))

Tactic:
replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)

Result:
case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
h : Disjoint (ker (f i)) (((insert i s).erase i).sup fun i => ker (f i))
⊢ Disjoint (ker (f i)) (ker (s.noncommProd f ⋯))

Proof state:
case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ Commute (f i) (s.noncommProd f ⋯)

Tactic:
exact s.noncommProd_commute _ _ _ fun j hj ↦
  comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by aesop)

Result:
no goals

Proof state:
case empty
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
comm : (↑∅).Pairwise (Commute on f)
h : ∅.SupIndep fun i => ker (f i)
⊢ ker (∅.noncommProd f comm) = ⨆ i ∈ ∅, ker (f i)

Tactic:
simp [one_eq_id]

Result:
no goals

Proof state:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ ker ((insert i s).noncommProd f comm) = ⨆ i_1 ∈ insert i s, ker (f i_1)

Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, mul_eq_comp,
  ker_comp_eq_of_commute_of_disjoint_ker]

Result:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ ker (f i) ⊔ ker (s.noncommProd f ⋯) = ⨆ i_1 ∈ insert i s, ker (f i_1)

case insert.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ Commute (f i) (s.noncommProd f ⋯)

case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ Disjoint (ker (f i)) (ker (s.noncommProd f ⋯))

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
j : ι
hj : j ∈ s
⊢ i ≠ j

Tactic:
aesop

Result:
no goals

Proof state:
case insert.h'
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
h : Disjoint (ker (f i)) (((insert i s).erase i).sup fun i => ker (f i))
⊢ Disjoint (ker (f i)) (ker (s.noncommProd f ⋯))

Tactic:
simpa [ih, hi, Finset.sup_eq_iSup] using h

Result:
no goals

Proof state:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Commute on f)),
    (s.SupIndep fun i => ker (f i)) → ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i)
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
⊢ ker ((insert i s).noncommProd f comm) = ⨆ i_1 ∈ insert i s, ker (f i_1)

Tactic:
replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
    ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))

Result:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ ker ((insert i s).noncommProd f comm) = ⨆ i_1 ∈ insert i s, ker (f i_1)

Proof state:
case insert
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s)).Pairwise (Commute on f)
h : (insert i s).SupIndep fun i => ker (f i)
ih : ker (s.noncommProd f ⋯) = ⨆ x ∈ s, ker (f x)
⊢ ker (f i) ⊔ ker (s.noncommProd f ⋯) = ⨆ i_1 ∈ insert i s, ker (f i_1)

Tactic:
simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]

Result:
no goals