awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : 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)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
hsp :
  Eq (α := Submodule R (V ⧸ W))
    (span R (range.{u_3, u_5 + 1} (ι := n) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))))
    (span R (range.{u_3, u_5 + 1} (ι := n) (⇑bQ : (a : n) → V ⧸ W)))
⊢ LE.le (α := Submodule R V) ⊤
    (span R
      (range (ι := m ⊕ n)
        (Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W)))))

Tactic:
rw [Set.Sum.elim_range, Submodule.span_union,
      show Set.range (fun i ↦ (bW i : V)) = W.subtype '' (Set.range (fun i ↦ bW i)) by aesop,
      ← Submodule.map_span, bW.span_eq, Submodule.map_top, Submodule.range_subtype, top_le_iff,
      ← Submodule.map_mkQ_eq_top, Submodule.map_span, ← Set.range_comp, ← bQ.span_eq]

Premises used: Set.range_comp, Set.Sum.elim_range, Submodule.map_top, Submodule.map_mkQ_eq_top, Submodule.span_union, top_le_iff, Submodule.map_span, Module.Basis.span_eq, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R_1 : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R_1 M
R : Type u_2
V : Type u_3
inst_6 : CommRing R
inst_7 : AddCommGroup V
inst_8 : 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)
b : m ⊕ n → V := Sum.elim (fun (i : m) ↦ (↑((bW : (a : m) → ↥W) i) : V)) (surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))
br : Eq (α := n → V ⧸ W) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ b ∘ Sum.inr) (⇑bQ : (a : n) → V ⧸ W)
⊢ Eq (α := Submodule R (V ⧸ W))
    (span R (range.{u_3, u_5 + 1} (ι := n) ((⇑W.mkQ : (a : V) → V ⧸ W) ∘ surjInv ⋯ ∘ (⇑bQ : (a : n) → V ⧸ W))))
    (span R (range.{u_3, u_5 + 1} (ι := n) (⇑bQ : (a : n) → V ⧸ W)))

Tactic:
congr 2
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
i : m
⊢ Eq.{u_3 + 1} (α := V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) ((↑((bW : (a : m) → ↥W) i) : V) : V)

Tactic:
simp [sumQuot]

Premises used: Module.Basis.sumQuot
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ Eq.{u_3 + 1} (α := V ⧸ W) (Submodule.Quotient.mk ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr j)) : V ⧸ W)
    ((bQ : (a : n) → V ⧸ W) j : V ⧸ W)

Tactic:
simpa only [sumQuot, Basis.coe_mk, Sum.elim_inr, Function.comp_apply, ← W.mkQ_apply]
    using Function.rightInverse_surjInv W.mkQ_surjective _

Premises used: Module.Basis.sumQuot, Submodule.mkQ_apply, Sum.elim_inr, Module.Basis.coe_mk, Function.rightInverse_surjInv, Function.comp_apply, Submodule.mkQ_surjective
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
i : m
rw : Eq.{u_3 + 1} (α := V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inl i) : V) ((↑((bW : (a : m) → ↥W) i) : V) : V)
rw₁ rw₂ : Eq.{u_3 + 1} (α := V) (↑((bW : (a : m) → ↥W) i) : V) (↑((bW : (a : m) → ↥W) i) : V)
⊢ Eq (α := m ⊕ n →₀ R) (((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) (↑((bW : (a : m) → ↥W) i) : V))
    (Finsupp.single (Sum.inl i) 1)

Tactic:
rw [← Module.Basis.apply_eq_iff, sumQuot_inl]

Premises used: Module.Basis.apply_eq_iff, Module.Basis.sumQuot_inl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)

Tactic:
Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i)

Premises used: Module.Basis.sumQuot, Sum.inl, Module.Basis.repr, Module.Basis.repr_apply_eq, Submodule.subtype, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
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)
⊢ 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)

Tactic:
refine Eq.symm <| (bW.repr_apply_eq
      (fun w i => (sumQuot bW bQ).repr (W.subtype w) (Sum.inl i)) ?_ ?_ ?_ w i)

Premises used: Module.Basis.sumQuot, Sum.inl, Module.Basis.repr, Module.Basis.repr_apply_eq, Submodule.subtype, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ ∀ (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:
aesop (add simp Finsupp.single_apply)

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ ∀ (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:
aesop (add simp Finsupp.single_apply)

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
⊢ ∀ (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:
aesop (add simp Finsupp.single_apply)

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
i : m
⊢ Eq.{u_2 + 1} (α := R)
    (((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R) v : m ⊕ n →₀ R) : (a : m ⊕ n) → R) (Sum.inl i) : R)
    ((((bW.repr : (a : ↥W) → m →₀ R) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) v hv) : m →₀ R) : (a : m) → R) i : R)

Tactic:
sumQuot_repr_inl bW bQ ⟨v, hv⟩ i

Premises used: Module.Basis.sumQuot_repr_inl, Subtype.mk
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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)

Tactic:
simp only [← Module.Basis.coord_apply]

Premises used: Module.Basis.coord_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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:
rw [← LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
rw : (bW.sumQuot bQ).coord (Sum.inr j) = bQ.coord j ∘ₗ W.mkQ
⊢ ∀ (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:
rw [← LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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)
⊢ (bW.sumQuot bQ).coord (Sum.inr j) = bQ.coord j ∘ₗ W.mkQ

Tactic:
apply (sumQuot bW bQ).ext

Premises used: Module.Basis.sumQuot, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
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:
simp [sumQuot_inl, LinearMap.comp_apply,
      (Quotient.mk_eq_zero W).mpr (Submodule.coe_mem (bW i))]

Premises used: Iff.mpr, LinearMap.comp_apply, Submodule.coe_mem, Module.Basis.sumQuot_inl, DFunLike.coe, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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 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:
simp [LinearMap.comp_apply, sumQuot_inr, Finsupp.single_apply]

Premises used: LinearMap.comp_apply, Module.Basis.sumQuot_inr, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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 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:
classical
    simp [LinearMap.comp_apply, sumQuot_inr, Finsupp.single_apply]

Premises used: LinearMap.comp_apply, Module.Basis.sumQuot_inr, Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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)
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)
⊢ 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)

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]

Premises used: LinearMap.comp_apply, Module.Basis.sumQuot_inr, Finsupp.single_apply, Module.Basis.sumQuot_inl
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
this : Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) (0 : V ⧸ W)
⊢ 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)

Tactic:
simp [sumQuot_repr_inr, this]

Premises used: Module.Basis.sumQuot_repr_inr
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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
suffices : Eq (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) (0 : V ⧸ W)
⊢ 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)

Tactic:
suffices W.mkQ v = 0 by simp [sumQuot_repr_inr, this]
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
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 (α := V ⧸ W) ((W.mkQ : (a : V) → V ⧸ W) v : V ⧸ W) (0 : V ⧸ W)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Module.rank K V < ℵ₀
⊢ (ofVectorSpaceIndex K V).Finite

Tactic:
Set.finite_def.2 <| (Basis.ofVectorSpace K V).nonempty_fintype_index_of_rank_lt_aleph0 h

Premises used: Iff.mpr, Module.Basis.ofVectorSpace, Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0, Set.finite_def
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
let : ∀ (f : ((V ⧸ p) × ↥p) ≃ₗ[K] V), Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
let ⟨f⟩ := quotient_prod_linearEquiv p
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : ((V ⧸ p) × ↥p) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
rank_prod'.symm.trans f.rank_eq

Premises used: LinearEquiv.rank_eq, rank_prod', Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : ((V ⧸ p) × ↥p) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
exact rank_prod'.symm.trans f.rank_eq

Premises used: LinearEquiv.rank_eq, rank_prod', Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
let let₁ let₂ : ∀ (f : ((V ⧸ p) × ↥p) ≃ₗ[K] V), Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank 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
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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

Tactic:
⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent, And.intro, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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
refine :
  #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    Module.rank K V
⊢ ∃ (s : Set V), #(↑s : Type u₀) = Module.rank K V ∧ LinearIndepOn K id s

Tactic:
refine ⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩
-- Module: Mathlib.LinearAlgebra.Dimension.DivisionRing
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)
rw₂ rw₃ : lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V)
⊢ #(↑(range (ι := Module.Free.ChooseBasisIndex K V) (⇑b : (a : Module.Free.ChooseBasisIndex K V) → V)) : Type u₀) =
    Module.rank K V

Tactic:
rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
      Module.Free.rank_eq_card_chooseBasisIndex]

Premises used: Cardinal.mk_range_eq_of_injective, Function.Injective.eq_iff, Module.Basis.injective, Module.Free.rank_eq_card_chooseBasisIndex, Cardinal.lift_injective