awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
refine : ∀ (n : ℕ) {f g : End K (Fin n → K)} (hfg : f * g = 1), g * f = 1
⊢ IsStablyFiniteRing K

Tactic:
refine isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd.mpr fun n ↦ ⟨fun {f g} hfg ↦ ?_⟩

Premises used: Iff.mpr, IsDedekindFiniteMonoid.mk, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
x : Fin n → K
rw rw₁ :
  Eq (α := Fin n → K) ((1 : (a : Fin n → K) → Fin n → K) x : Fin n → K)
    ((1 : (a : Fin n → K) → Fin n → K) x : Fin n → K)
⊢ Eq (α := Fin n → K) ((f * g : (a : Fin n → K) → Fin n → K) x : Fin n → K)
    ((1 : (a : Fin n → K) → Fin n → K) x : Fin n → K)

Tactic:
rw [hfg]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
⊢ Injective (α := Fin n → K) (β := Fin n → K) (⇑g : (a : Fin n → K) → Fin n → K)

Tactic:
have ginj : Injective g :=
    HasLeftInverse.injective ⟨f, fun x => show (f * g) x = (1 : End K (Fin n → K)) x by rw [hfg]⟩
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective (α := Fin n → K) (β := Fin n → K) (⇑g : (a : Fin n → K) → Fin n → K)
let : ∀ (i : (Fin n → K) →ₗ[K] Fin n → K) (hi : g ∘ₗ i = id), g * f = 1
⊢ g * f = 1

Tactic:
let ⟨i, hi⟩ := g.exists_rightInverse_of_surjective
    (range_eq_top.2 (injective_iff_surjective.1 ginj))
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective (α := Fin n → K) (β := Fin n → K) (⇑g : (a : Fin n → K) → Fin n → K)
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
⊢ f * (g * i) = f * 1

Tactic:
have : f * (g * i) = f * 1 := congr_arg _ hi
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective (α := Fin n → K) (β := Fin n → K) (⇑g : (a : Fin n → K) → Fin n → K)
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : f * (g * i) = f * 1
⊢ i = f

Tactic:
rw [← mul_assoc, hfg, one_mul, mul_one] at this

Premises used: mul_assoc, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective (α := Fin n → K) (β := Fin n → K) (⇑g : (a : Fin n → K) → Fin n → K)
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
rwa rwa₁ rwa₂ rwa₃ : g * i = 1
⊢ g * f = 1

Tactic:
rwa [← this]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
R : Type u_1
M : Type u_2
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
inst_8 : Free R M
inst_9 : Module.Finite R M
inst_10 : IsStablyFiniteRing R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M → R :=
  Basis.repr (Free.chooseBasis R M) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Free.ChooseBasisIndex R M)
rw : IsStablyFiniteRing (End R (Free.ChooseBasisIndex R M → R))
⊢ IsStablyFiniteRing.{u_2} (End R M)

Tactic:
rw [RingEquiv.isStablyFiniteRing_iff e.conjRingEquiv]

Premises used: RingEquiv.isStablyFiniteRing_iff, LinearEquiv.conjRingEquiv
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
V₂ : Type v'
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
R : Type u_1
M : Type u_2
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
inst_8 : Free R M
inst_9 : Module.Finite R M
inst_10 : IsStablyFiniteRing R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M → R :=
  Basis.repr (Free.chooseBasis R M) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Free.ChooseBasisIndex R M)
⊢ IsStablyFiniteRing (End R (Free.ChooseBasisIndex R M → R))

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inst_5 : IsStablyFiniteRing R
f : End R M
hf : Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ Injective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
have ⟨_, eq⟩ := projective_lifting_property _ .id hf
  injective_of_comp_eq_id _ _ (mul_eq_one_symm eq)

Premises used: IsDedekindFiniteMonoid.mul_eq_one_symm, LinearMap.id, _private.0.Module.End.injective_of_surjective.match_1, LinearMap.injective_of_comp_eq_id, Module.projective_lifting_property, Function.Injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
inst_5 : IsStablyFiniteRing R
f g : M →ₗ[R] M
⊢ f ∘ₗ g = id ↔ g ∘ₗ f = id

Tactic:
mul_eq_one_comm

Premises used: mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
hfg : f * g = 1
⊢ g * f = 1

Tactic:
mul_eq_one_symm hfg

Premises used: IsDedekindFiniteMonoid.mul_eq_one_symm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
⊢ f * g = 1 ↔ g * f = 1

Tactic:
mul_eq_one_comm

Premises used: mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
⊢ comap f p = p ⊔ f.ker

Tactic:
le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)

Premises used: Iff.mpr, le_antisymm, sup_le_iff, And.intro, LinearMap.ker_le_comap
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
refine : ∀ (x : V) (hx : x ∈ comap f p), x ∈ p ⊔ f.ker
⊢ comap f p = p ⊔ f.ker

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)

Premises used: Iff.mpr, le_antisymm, sup_le_iff, And.intro
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
obtain :
  ∀ (y : V) (hy : y ∈ p)
    (hxy :
      Eq (α := ↥p) ((f.restrict h : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : V) ↦ x ∈ p) y hy) : ↥p)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ p) ((f : (a : V) → V) x) hx : ↥p)),
    x ∈ p ⊔ f.ker
⊢ x ∈ p ⊔ f.ker

Tactic:
obtain ⟨⟨y, hy⟩, hxy⟩ :=
    surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩

Premises used: Iff.mpr, LinearMap.injective_restrict_iff_disjoint, Subtype.mk, LinearMap.surjective_of_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy :
  Eq (α := ↥p) ((f.restrict h : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : V) ↦ x ∈ p) y hy) : ↥p)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ p) ((f : (a : V) → V) x) hx : ↥p)
⊢ Eq (α := V) ((f : (a : V) → V) y : V) ((f : (a : V) → V) x : V)

Tactic:
simpa [Subtype.ext_iff] using hxy

Premises used: Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy :
  Eq (α := ↥p) ((f.restrict h : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : V) ↦ x ∈ p) y hy) : ↥p)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ p) ((f : (a : V) → V) x) hx : ↥p)
⊢ Eq (α := V) ((f : (a : V) → V) y : V) ((f : (a : V) → V) x : V)

Tactic:
replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : Eq (α := V) ((f : (a : V) → V) y : V) ((f : (a : V) → V) x : V)
⊢ x - y ∈ f.ker

Tactic:
simp [hxy]
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : Eq (α := V) ((f : (a : V) → V) y : V) ((f : (a : V) → V) x : V)
⊢ x ∈ p ⊔ f.ker

Tactic:
exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel y x⟩

Premises used: Iff.mpr, HSub.hSub, add_sub_cancel, And.intro, Exists.intro, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : V) (0 : V) →
      Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
rw : ∀ x ∈ f.ker, Membership.mem (α := V) f.ker ((g : (a : V) → V) x : V)
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']

Premises used: LinearMap.ker_comp, LinearMap.comap_eq_sup_ker_of_disjoint
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : V) (0 : V) →
      Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
⊢ ∀ x ∈ f.ker, Membership.mem (α := V) f.ker ((g : (a : V) → V) x : V)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
suffices :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : V) (0 : V) →
      Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : Eq (α := V) ((f : (a : V) → V) x : V) (0 : V)
rw : Eq (α := V) ((f ∘ₗ g : (a : V) → V) x : V) (0 : V)
rw₁ : Eq (α := V) ((f * g : (a : V) → V) x : V) (0 : V)
rw₂ : Eq (α := V) ((g * f : (a : V) → V) x : V) (0 : V)
rw₃ : Eq (α := V) ((g : (a : V) → V) ((f : (a : V) → V) x : V) : V) (0 : V)
rw₄ : Eq (α := V) ((g : (a : V) → V) 0 : V) (0 : V)
rw₅ rw₆ : Eq.{v + 1} (α := V) 0 0
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)

Tactic:
rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_apply, map_zero, Module.End.mul_apply, Commute.eq
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
comm : (↑∅ : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker
⊢ (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker

Tactic:
simp [Module.End.one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker),
    (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker
⊢ (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker

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))
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
insert : (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
insert₁ : Commute (f i) (s.noncommProd f ⋯)
insert₂ : Disjoint (f i).ker (s.noncommProd f ⋯).ker
⊢ ((Insert.insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]

Premises used: Module.End.mul_eq_comp, Finset.noncommProd_insert_of_notMem, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
insert : (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i (↑s : Set ι), (f i_1).ker
insert₁ : (f i).ker ⊔ (s.noncommProd f ⋯).ker = (f i).ker ⊔ ⨆ x ∈ (↑s : Set ι), (f x).ker
insert₂ : (f i).ker ⊔ (s.noncommProd f ⋯).ker = (f i).ker ⊔ ⨆ x ∈ s, (f x).ker
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker

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

Premises used: iSup_insert, Finset.mem_insert_coe, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
j : ι
hj : j ∈ s
⊢ i ≠ j

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ 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 lia)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, Finset.noncommProd_commute
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (insert i s) fun (i : ι) ↦ (f i).ker
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
⊢ Disjoint (f i).ker (((insert i s).erase i).sup fun (i : ι) ↦ (f i).ker)

Tactic:
replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
i : ι
s : Finset ι
hi : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Commute on f)
ih : (s.noncommProd f ⋯).ker = ⨆ x ∈ s, (f x).ker
h : Disjoint (f i).ker (((insert i s).erase i).sup fun (i : ι) ↦ (f i).ker)
⊢ Disjoint (f i).ker (s.noncommProd f ⋯).ker

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

Premises used: Finset.sup_eq_iSup
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
empty :
  ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
    (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      ∀ (comm : (↑s : Set ι).Pairwise (Commute on f))
        (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker),
        (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker)
    (comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker),
    ((Insert.insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker

Tactic:
induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    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))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h

Premises used: iSup_insert, Module.End.mul_eq_comp, Module.End.one_eq_id, Finset.mem_insert_coe, Insert.insert, Finset.sup_eq_iSup, Finset.mem_coe, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s : Set ι).Pairwise (Commute on f)
h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker
empty :
  ∀ (comm : (↑∅ : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) ∅ fun (i : ι) ↦ (f i).ker),
    (Finset.noncommProd ∅ f comm).ker = ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) ∅ i), (f i).ker
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      ∀ (comm : (↑s : Set ι).Pairwise (Commute on f))
        (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) s fun (i : ι) ↦ (f i).ker),
        (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker)
    (comm : (↑(Insert.insert i s) : Set ι).Pairwise (Commute on f))
    (h : Finset.SupIndep.{v, u_1} (α := Submodule K V) (Insert.insert i s) fun (i : ι) ↦ (f i).ker),
    ((Insert.insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    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))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h

Premises used: iSup_insert, Module.End.mul_eq_comp, Module.End.one_eq_id, Finset.mem_insert_coe, Insert.insert, Finset.sup_eq_iSup, Finset.mem_coe, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ Eq (α := (a : V) → V) (⇑(ofInjectiveEndo f h_inj) : (a : V) → V) (⇑f : (a : V) → V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ f * (↑(ofInjectiveEndo f h_inj).symm : V →ₗ[K] V) = 1

Tactic:
LinearMap.ext <| (ofInjectiveEndo f h_inj).apply_symm_apply

Premises used: LinearMap.ext, LinearEquiv.apply_symm_apply, LinearEquiv.ofInjectiveEndo
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ (↑(ofInjectiveEndo f h_inj).symm : V →ₗ[K] V) * f = 1

Tactic:
LinearMap.ext <| (ofInjectiveEndo f h_inj).symm_apply_apply

Premises used: LinearMap.ext, LinearEquiv.symm_apply_apply, LinearEquiv.ofInjectiveEndo