awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
refine_1 :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_2 : ∀ (c : R) (x : ↥W),
  (fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      (c • x) =
    HSMul.hSMul (β := m → R) c
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        x)
Tactic: refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
refine_1 :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2 :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_3 : ∀ (i : m),
  Eq (α := m → R)
    ((fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      ((bW : (a : m) → ↥W) i))
    (⇑(Finsupp.single i 1) : (a : m) → R)
Tactic: refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_1 : ∀ (x y : ↥W),
  (fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      (x + y) =
    HAdd.hAdd (α := m → R)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        x)
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        y)
Tactic: classical
  refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
refine_1 :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_2 : ∀ (c : R) (x : ↥W),
  (fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      (c • x) =
    HSMul.hSMul (β := m → R) c
      ((fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        x)
Tactic: classical
  refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
w : ↥W
i : m
refine_1 :
  ∀ (x y : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (x + y) =
      HAdd.hAdd (α := m → R)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          y)
refine_2 :
  ∀ (c : R) (x : ↥W),
    (fun (w : ↥W) (i : m) ↦
          (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                (a : m ⊕ n) → R)
              (Sum.inl i) :
            R))
        (c • x) =
      HSMul.hSMul (β := m → R) c
        ((fun (w : ↥W) (i : m) ↦
            (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) :
                  (a : m ⊕ n) → R)
                (Sum.inl i) :
              R))
          x)
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑w : V) : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) w : m →₀ R) : (a : m) → R) i : R)
have refine_3 : ∀ (i : m),
  Eq (α := m → R)
    ((fun (w : ↥W) (i : m) ↦
        (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) ((W.subtype : (a : ↥W) → V) w) : m ⊕ n →₀ R) : (a : m ⊕ n) → R)
            (Sum.inl i) :
          R))
      ((bW : (a : m) → ↥W) i))
    (⇑(Finsupp.single i 1) : (a : m) → R)
Tactic: classical
  refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i) <;>
  aesop (add simp Finsupp.single_apply)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
v : V
j : n
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) v : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inr j) : R)
    ((((bQ.repr : (a : V ⧸ W) → n →₀ R) ((W.mkQ : (a : V) → V ⧸ W) v) : n →₀ R) : (a : n) → R) j : R)
have simp : Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
  ((bQ.coord j : (a : V ⧸ W) → R) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) : R)
Tactic: simp only [← Module.Basis.coord_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
v : V
j : n
⊢ Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
    ((bQ.coord j : (a : V ⧸ W) → R) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) : R)
have rw : Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
  ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) v : R)
Tactic: rw [← LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
v : V
j : n
⊢ Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) v : R)
have revert : ∀ (v : V),
  Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) v : R)
Tactic: revert v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
j : n
⊢ ∀ (v : V),
    Eq.{u_2 + 1} (α := R) (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) v : R)
      ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) v : R)
have rw : (bW.sumQuot bQ).coord (Sum.inr j) = bQ.coord j ∘ₗ W.mkQ
Tactic: rw [← LinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
j : n
⊢ (bW.sumQuot bQ).coord (Sum.inr j) = bQ.coord j ∘ₗ W.mkQ
have apply : ∀ (i : m ⊕ n),
  Eq.{u_2 + 1} (α := R)
    (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) i : V) : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) i : V) : R)
Tactic: apply (sumQuot bW bQ).ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
j : n
x : m ⊕ n
⊢ Eq.{u_2 + 1} (α := R)
    (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) x : V) : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) x : V) : R)
have inl : ∀ (i : m),
  Eq.{u_2 + 1} (α := R)
    (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) : R)
Tactic: induction x with
  | inl i =>
    simp [sumQuot_inl, LinearMap.comp_apply,
      (Quotient.mk_eq_zero W).mpr (Submodule.coe_mem (bW i))]
  | inr i =>
    classical
    simp [LinearMap.comp_apply, sumQuot_inr, Finsupp.single_apply]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
j : n
x : m ⊕ n
inl :
  ∀ (i : m),
    Eq.{u_2 + 1} (α := R)
      (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) : R)
      ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) x : V) : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) x : V) : R)
have inr : ∀ (i : n),
  Eq.{u_2 + 1} (α := R)
    (((bW.sumQuot bQ).coord (Sum.inr j) : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr i) : V) : R)
    ((bQ.coord j ∘ₗ W.mkQ : (a : V) → R) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr i) : V) : R)
Tactic: induction x with
  | inl i =>
    simp [sumQuot_inl, LinearMap.comp_apply,
      (Quotient.mk_eq_zero W).mpr (Submodule.coe_mem (bW i))]
  | inr i =>
    classical
    simp [LinearMap.comp_apply, sumQuot_inr, Finsupp.single_apply]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis.{u_4, u_2, u_3} m R ↥W
bQ : Basis.{u_5, u_2, u_3} n R (V ⧸ W)
v : V
hv : v ∈ W
j : n
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) v : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inr j) : R) (0 : R)
have suffices : Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) (0 : V ⧸ W)
Tactic: suffices W.mkQ v = 0 by simp [sumQuot_repr_inr, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
have let : ∀ (f : ((V ⧸ p) × ↥p) ≃ₗ[K] V), Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
Tactic: let ⟨f⟩ := quotient_prod_linearEquiv p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
have let : ∀ (f : ((V ⧸ p) × ↥p) ≃ₗ[K] V), Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
Tactic: classical
    let ⟨f⟩ := quotient_prod_linearEquiv p
    exact rank_prod'.symm.trans f.rank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V_1 V₁ V₂ V₃ : Type v
ι : Type w
inst : DivisionRing K
inst_1 : AddCommGroup V_1
inst_2 : Module K V_1
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
V : Type u₀
x : AddCommGroup V
x_1 : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ ∃ (s : Set V), #(↑s : Type u₀) = Module.rank K V ∧ LinearIndepOn K id s
have refine : #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
  Module.rank K V
Tactic: refine ⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V_1 V₁ V₂ V₃ : Type v
ι : Type w
inst : DivisionRing K
inst_1 : AddCommGroup V_1
inst_2 : Module K V_1
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
V : Type u₀
x : AddCommGroup V
x_1 : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    Module.rank K V
have rw : lift.{u₀, u₀}
    #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
  lift.{u₀, u₀} (Module.rank K V)
Tactic: rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
      Module.Free.rank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V_1 V₁ V₂ V₃ : Type v
ι : Type w
inst : DivisionRing K
inst_1 : AddCommGroup V_1
inst_2 : Module K V_1
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
V : Type u₀
x : AddCommGroup V
x_1 : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
rw :
  lift.{u₀, u₀}
      #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    lift.{u₀, u₀} (Module.rank K V)
⊢ #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    Module.rank K V
have rw₁ : lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} (Module.rank K V)
Tactic: rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
      Module.Free.rank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V_1 V₁ V₂ V₃ : Type v
ι : Type w
inst : DivisionRing K
inst_1 : AddCommGroup V_1
inst_2 : Module K V_1
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
V : Type u₀
x : AddCommGroup V
x_1 : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
rw :
  lift.{u₀, u₀}
      #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    lift.{u₀, u₀} (Module.rank K V)
rw₁ : lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} (Module.rank K V)
⊢ #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    Module.rank K V
have rw₂ : lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V)
Tactic: rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
      Module.Free.rank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
⊢ Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
have rwa : (db.coprod eb).range = ⊤
Tactic: rwa [← range_eq_top, range_coprod, eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
rwa : (db.coprod eb).range = ⊤
⊢ Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
have rwa₁ : db.range ⊔ eb.range = ⊤
Tactic: rwa [← range_eq_top, range_coprod, eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (hypothesis)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
have hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
Tactic: have hf : Surjective (coprod db eb) := by
    rwa [← range_eq_top, range_coprod, eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
| Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
have rhs : Module.rank K V₂ + Module.rank K V₃
Tactic: rhs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.DivisionRing (goal)
Goal:
K : Type u
V V₁ V₂ V₃ : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₁
inst_4 : Module K V₁
inst_5 : AddCommGroup V₂
inst_6 : Module K V₂
inst_7 : AddCommGroup V₃
inst_8 : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ :
  ∀ (d : V₂) (e : V₃),
    Eq (α := V) ((db : (a : V₂) → V) d : V) ((eb : (a : V₃) → V) e : V) →
      ∃ (c : V₁), (cd : (a : V₁) → V₂) c = d ∧ (ce : (a : V₁) → V₃) c = e
hf : Surjective (α := V₂ × V₃) (β := V) (⇑(db.coprod eb) : (a : V₂ × V₃) → V)
| Module.rank K V₂ + Module.rank K V₃
have rw : Module.rank K V + Module.rank K ↥(db.coprod eb).ker
Tactic: rw [← rank_prod', rank_eq_of_surjective hf]