awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
⊢ (fun (w : V) ↦
        (Finsupp.single default
            (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
              ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
          ι →₀ K))
      ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) =
    f
have h₁ : Eq.{u + 1} (α := K)
  (((fun (w : V) ↦
            (Finsupp.single default
                (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                  ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
              ι →₀ K))
          ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) :
        (a : ι) → K)
      default :
    K)
  ((f : (a : ι) → K) default : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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₂
ι : Type u_1
inst_5 : Unique ι
h_1 : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h_1
h : Ne.{u + 1} (α := K) ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) (0 : K)
f : ι →₀ K
⊢ Eq.{u + 1} (α := K)
    (((fun (w : V) ↦
              (Finsupp.single default
                  (HDiv.hDiv (α := K) (β := K) ((((b.repr : (a : V) → ι →₀ K) w : ι →₀ K) : (a : ι) → K) default : K)
                    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K)) :
                ι →₀ K))
            ((fun (f : ι →₀ K) ↦ HSMul.hSMul.{u, v, v} (α := K) ((f : (a : ι) → K) default : K) v) f) :
          (a : ι) → K)
        default :
      K)
    ((f : (a : ι) → K) default : K)
have h₁ : HDiv.hDiv (β := K)
    (HMul.hMul (α := K) (β := K) ((f : (a : ι) → K) default : K)
      ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K))
    ((((b.repr : (a : V) → ι →₀ K) v : ι →₀ K) : (a : ι) → K) default : K) =
  (f : (a : ι) → K) default
Tactic: simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          RingHom.id_apply, smul_eq_mul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
i : ι
⊢ (basisSingleton ι h v hv : (a : ι) → V) i = v
have refl : (basisSingleton ι h v hv : (a : ι) → V) default = v
Tactic: cases Unique.uniq ‹Unique ι› i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ Eq (α := Set V) (Set.range.{v, u_1 + 1} (ι := ι) (⇑(basisSingleton ι h v hv) : (a : ι) → V)) {v}
have rw : Eq (α := Set V) (singleton (α := V) ((basisSingleton ι h v hv : (a : ι) → V) default : V)) {v}
Tactic: rw [Set.range_unique, basisSingleton_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type u_1
inst_3 : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
rw : Eq (α := Set V) (singleton (α := V) ((basisSingleton ι h v hv : (a : ι) → V) default : V)) {v}
⊢ Eq (α := Set V) (Set.range.{v, u_1 + 1} (ι := ι) (⇑(basisSingleton ι h v hv) : (a : ι) → V)) {v}
have rw₁ : Eq (α := Set V) {v} {v}
Tactic: rw [Set.range_unique, basisSingleton_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S₁ S₂ : Submodule K V
inst_3 : FiniteDimensional.{u, v} K ↥S₂
hle : S₁ ≤ S₂
hd : finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥S₁
⊢ S₁ = S₂
have hd₁ : finrank.{u, v} K ↥S₂ ≤ finrank.{u, v} K ↥(comap S₂.subtype S₁)
Tactic: rw [← LinearEquiv.finrank_eq (Submodule.comapSubtypeEquivOfLe hle)] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
have h : Module.rank K ↥f.range = Module.rank K V
Tactic: have h := rank_range_of_injective _ hinj
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
hinj : Injective (α := V) (β := V) (⇑f : (a : V) → V)
h : Module.rank K ↥f.range = Module.rank K V
⊢ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
have h₁ : finrank.{u, v} K ↥f.range = finrank K V
Tactic: rw [← finrank_eq_rank, ← finrank_eq_rank, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Set.InjOn (β := V) (⇑f : (a : V) → V) (↑p : Set V) ↔ Set.SurjOn (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V)
have rw : Injective.{v + 1, v + 1} (α := (↑(↑p : Set V) : Type v)) (β := V)
    ((↑p : Set V).restrict (π := fun (a : V) ↦ V) (⇑f : (a : V) → V)) ↔
  Surjective (Set.MapsTo.restrict (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V) h)
Tactic: rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Injective.{v + 1, v + 1} (α := (↑(↑p : Set V) : Type v)) (β := V)
      ((↑p : Set V).restrict (π := fun (a : V) ↦ V) (⇑f : (a : V) → V)) ↔
    Surjective (Set.MapsTo.restrict (⇑f : (a : V) → V) (↑p : Set V) (↑p : Set V) h)
have change : Injective (α := ↥p) (β := V) (⇑(f.domRestrict p) : (a : ↥p) → V) ↔
  Surjective (α := ↥p) (β := ↥p) (⇑(f.restrict h) : (a : ↥p) → ↥p)
Tactic: change Injective (f.domRestrict p) ↔ Surjective (f.restrict h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw : f.ker = ⊥ ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
rw : f.ker = ⊥ ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw₁ : Injective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
rw : f.ker = ⊥ ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
rw₁ : Injective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
⊢ f.ker = ⊥ ↔ f.range = ⊤
have rw₂ : Surjective (α := V) (β := V) (⇑f : (a : V) → V) ↔ Surjective (α := V) (β := V) (⇑f : (a : V) → V)
Tactic: rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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₂
⊢ IsStablyFiniteRing K
have refine : ∀ (n : ℕ) {f g : End K (Fin n → K)} (hfg : f * g = 1), g * f = 1
Tactic: refine isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd.mpr fun n ↦ ⟨fun {f g} hfg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
⊢ g * f = 1
have ginj : 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]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ g * f = 1
have let : ∀ (i : (Fin n → K) →ₗ[K] Fin n → K) (hi : g ∘ₗ i = id), g * f = 1
Tactic: let ⟨i, hi⟩ := g.exists_rightInverse_of_surjective
    (range_eq_top.2 (injective_iff_surjective.1 ginj))
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
⊢ g * f = 1
have this : f * (g * i) = f * 1
Tactic: have : f * (g * i) = f * 1 := congr_arg _ hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
⊢ g * f = 1
have this₁ : i = f
Tactic: rw [← mul_assoc, hfg, one_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ g * f = 1
have rwa : g * i = 1
Tactic: rwa [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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.{u_2} (End R M)
have rw : IsStablyFiniteRing (End R (Free.ChooseBasisIndex R M → R))
Tactic: rw [RingEquiv.isStablyFiniteRing_iff e.conjRingEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
have refine : ∀ (x : V) (hx : x ∈ comap f p), x ∈ p ⊔ f.ker
Tactic: refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ x ∈ p ⊔ f.ker
have 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
Tactic: obtain ⟨⟨y, hy⟩, hxy⟩ :=
    surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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)
⊢ x ∈ p ⊔ f.ker
have hxy₁ : 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
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker
have rw : ∀ x ∈ f.ker, Membership.mem (α := V) f.ker ((g : (a : V) → V) x : V)
Tactic: rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker
have 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)
Tactic: suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw : Eq (α := V) ((f ∘ₗ g : (a : V) → V) x : V) (0 : V)
Tactic: rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw₁ : Eq (α := V) ((f * g : (a : V) → V) x : V) (0 : V)
Tactic: rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw₂ : Eq (α := V) ((g * f : (a : V) → V) x : V) (0 : V)
Tactic: rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw₃ : Eq (α := V) ((g : (a : V) → V) ((f : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw₄ : Eq (α := V) ((g : (a : V) → V) 0 : V) (0 : V)
Tactic: rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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)
⊢ Eq (α := V) ((f : (a : V) → V) ((g : (a : V) → V) x : V) : V) (0 : V)
have rw₅ : Eq.{v + 1} (α := V) 0 0
Tactic: rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (hypothesis)
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
⊢ ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
have ih₁ : (s.noncommProd f sorry).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))
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ ((insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
have insert : (f i).ker ⊔ (s.noncommProd f sorry).ker = ⨆ i_1 ∈ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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.insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
have insert₁ : Commute (f i) (s.noncommProd f sorry)
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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.insert i s).noncommProd f comm).ker = ⨆ i_1 ∈ Insert.insert i s, (f i_1).ker
have insert₂ : Disjoint (f i).ker (s.noncommProd f sorry).ker
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteDimensional.Basic (goal)
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
⊢ (f i).ker ⊔ (s.noncommProd f ⋯).ker = ⨆ i_1 ∈ insert i s, (f i_1).ker
have insert : (f i).ker ⊔ (s.noncommProd f sorry).ker = ⨆ i_1 ∈ insert i (↑s : Set ι), (f i_1).ker
Tactic: simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]