awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
u v : m ⊕ n
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e u v = fromBlocks A B 0 D u v
have a : ∀ (i : m),
  (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) v = fromBlocks A B 0 D (Sum.inl i) v
Tactic: cases u with
  | inl i =>
    cases v with
    | inl k =>
      simp only [b, sumQuot_inl, Matrix.fromBlocks_apply₁₁, A, LinearMap.toMatrix_apply]
      apply sumQuot_repr_inl_of_mem
    | inr l => simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]
  | inr j =>
    cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
R : Type u_6
V : Type u_7
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Finite R V
W : Submodule R V
inst_4 : Free.{u_6, u_7} R ↥W
inst_5 : Module.Finite.{u_6, u_7} R ↥W
inst_6 : Free.{u_6, u_7} R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW : (a : ↥W →ₗ[R] ↥W) → Matrix m m R) (e.restrict he)
B : Matrix m n R :=
  (of : (a : m → n → R) → Matrix m n R) fun (i : m) (l : n) ↦
    ((((bW.sumQuot bQ).repr : (a : V) → m ⊕ n →₀ R)
            ((e : (a : V) → V) ((bW.sumQuot bQ : (a : m ⊕ n) → V) (Sum.inr l) : V)) :
          Finsupp.{u_7, u_6} (m ⊕ n) R) :
        (a : m ⊕ n) → R)
      (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ : (a : V ⧸ W →ₗ[R] V ⧸ W) → Matrix n n R) (W.mapQ W e he)
u v : m ⊕ n
a :
  ∀ (i : m),
    (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inl i) v = fromBlocks A B 0 D (Sum.inl i) v
⊢ (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e u v = fromBlocks A B 0 D u v
have a₁ : ∀ (j : n),
  (toMatrix b b : (a : V →ₗ[R] V) → Matrix (m ⊕ n) (m ⊕ n) R) e (Sum.inr j) v = fromBlocks A B 0 D (Sum.inr j) v
Tactic: cases u with
  | inl i =>
    cases v with
    | inl k =>
      simp only [b, sumQuot_inl, Matrix.fromBlocks_apply₁₁, A, LinearMap.toMatrix_apply]
      apply sumQuot_repr_inl_of_mem
    | inr l => simp [b, LinearMap.toMatrix_apply, Matrix.fromBlocks_apply₁₂, B]
  | inr j =>
    cases v with
    | inl k =>
      suffices W.mkQ (e (bW k)) = 0 by simp [LinearMap.toMatrix_apply, b, this]
      rw [← LinearMap.mem_ker, Submodule.ker_mkQ]
      exact he (Submodule.coe_mem (bW k))
    | inr l =>
      simp only [LinearMap.toMatrix_apply, sumQuot_repr_inr,
        Matrix.fromBlocks_apply₂₂, b, D]
      rw [← sumQuot_inr bW bQ l, W.mapQ_apply]
      simp
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
⊢ LinearIndependent (ι := ι₁ ⊕ ι₂) R (Sum.elim (fun (x : ι₁) ↦ (↑(f x) : M)) g)
have refine : Disjoint (α := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) (span R (range g))
Tactic: refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
⊢ Disjoint (α := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) (span R (range g))
have refine : ∀ (x : M) (h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x)
  (h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x), x = 0
Tactic: refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
x : M
h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x
⊢ x = 0
have this : x ∈ M'
Tactic: have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
x : M
h₁ : Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M))) x
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) x
this : x ∈ M'
⊢ x = 0
have obtain : ∀ (c : ι₂ →₀ R)
  (h₁ :
    Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
      (c.sum fun (i : ι₂) (a : R) ↦ a • g i))
  (h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i))
  (this : (c.sum fun (i : ι₂) (a : R) ↦ a • g i) ∈ M'), Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0
Tactic: obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
Cleared hypotheses: x, h₁, h₂, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (hypothesis)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ :
  Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
    (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
this : (c.sum fun (i : ι₂) (a : R) ↦ a • g i) ∈ M'
⊢ Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0
have this₁ : Eq.{v + 1} (α := M ⧸ M') (c.sum fun (a : ι₂) (b : R) ↦ HSMul.hSMul (β := M ⧸ M') b (Submodule.Quotient.mk (g a))) 0
Tactic: simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ :
  Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
    (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
this :
  Eq.{v + 1} (α := M ⧸ M') (c.sum fun (a : ι₂) (b : R) ↦ HSMul.hSMul (β := M ⧸ M') b (Submodule.Quotient.mk (g a))) 0
⊢ Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0
have rw : Eq.{v + 1} (α := M) (Finsupp.sum 0 fun (i : ι₂) (a : R) ↦ a • g i) 0
Tactic: rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (M := M ⧸ M') (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ :
  Membership.mem (γ := Submodule R M) (span R (range fun (x : ι₁) ↦ (↑(f x) : M)))
    (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
h₂ : Membership.mem (γ := Submodule R M) (span R (range g)) (c.sum fun (i : ι₂) (a : R) ↦ a • g i)
this :
  Eq.{v + 1} (α := M ⧸ M') (c.sum fun (a : ι₂) (b : R) ↦ HSMul.hSMul (β := M ⧸ M') b (Submodule.Quotient.mk (g a))) 0
rw : Eq.{v + 1} (α := M) (Finsupp.sum 0 fun (i : ι₂) (a : R) ↦ a • g i) 0
⊢ Eq.{v + 1} (α := M) (c.sum fun (i : ι₂) (a : R) ↦ a • g i) 0
have rw₁ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ LinearIndepOn R f (s ∪ t)
have apply : Disjoint (α := Submodule R M) (span R (f '' s)) (span R (f '' t))
Tactic: apply hs.union ht.of_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ Disjoint (α := Submodule R M) (span R (f '' s)) (span R (f '' t))
have h : Eq (α := Submodule R M) (span R (f '' s))
  (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
Tactic: convert! (Submodule.range_ker_disjoint ht).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
ht :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
h :
  Eq (α := Submodule R M) (span R (f '' s))
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
⊢ Disjoint (α := Submodule R M) (span R (f '' s)) (span R (f '' t))
have h₁ : f '' t = range fun (x : (↑t : Type w)) ↦ f (↑x : ι)
Tactic: convert! (Submodule.range_ker_disjoint ht).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ (↑M' : Set M)
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (M := M ⧸ M') (⇑M'.mkQ : (a : M) → M ⧸ M') t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (id '' s)))
    ((⇑(mkQ (span R (id '' s))) : (a : M) → M ⧸ span R (id '' s)) ∘ id) t
have rw : LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
  ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ id) t
Tactic: rw [image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
⊢ LinearIndepOn R f (s ∪ t) ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
have refine_1 : ∀ (h : LinearIndepOn R f (s ∪ t)), LinearIndepOn R f s
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
refine_1 : ∀ (h : LinearIndepOn R f (s ∪ t)), LinearIndepOn R f s
⊢ LinearIndepOn R f (s ∪ t) ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
have refine_2 : ∀ (h : LinearIndepOn R f (s ∪ t)),
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
have refine_2 : Disjoint (α := Submodule R M) (span R (range fun (x : (↑t : Type w)) ↦ f (↑x : ι)))
  (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s))) (mkQ (span R (f '' s))))
Tactic: apply (h.mono subset_union_right).map
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R f (s ∪ t)
have rw : LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
  LinearIndepOn R f s ∧
    LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
Tactic: rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
rw :
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R f s ∧
      LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
        ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
      ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
    LinearIndepOn R f (s ∪ t)
have rw₁ : LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t ↔
  LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R (f '' s)))
    ((⇑(mkQ (span R (f '' s))) : (a : M) → M ⧸ span R (f '' s)) ∘ f) t
Tactic: rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
| Module.rank R (M ⧸ M') + Module.rank R ↥M'
have simp : HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
  (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v))
Tactic: simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M
have conv_lhs : HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
    (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v)) ≤
  Module.rank R M
Tactic: conv_lhs => simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
⊢ HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set (M ⧸ M') // LinearIndepOn R id s }), #(↑(↑ι : Set (M ⧸ M')) : Type v))
      (⨆ (ι : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑ι : Set ↥M') : Type v)) ≤
    Module.rank R M
have rw : ⨆ (i : { s : Set (M ⧸ M') // LinearIndepOn R id s }),
    ⨆ (j : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑i : Set (M ⧸ M')) : Type v) + #(↑(↑j : Set ↥M') : Type v) ≤
  Module.rank R M
Tactic: rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
⊢ ⨆ (i : { s : Set (M ⧸ M') // LinearIndepOn R id s }),
      ⨆ (j : { s : Set ↥M' // LinearIndepOn R id s }), #(↑(↑i : Set (M ⧸ M')) : Type v) + #(↑(↑j : Set ↥M') : Type v) ≤
    Module.rank R M
have refine : ∀ (x : { s : Set (M ⧸ M') // LinearIndepOn R id s }) (s : Set (M ⧸ M')) (hs : LinearIndepOn R id s)
  (x : { s : Set ↥M' // LinearIndepOn R id s }) (t : Set ↥M') (ht : LinearIndepOn R id t),
  #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
      #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
    Module.rank R M
Tactic: refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
M' : Submodule R M
x : { s : Set (M ⧸ M') // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x_1 : { s : Set ↥M' // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
      #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
    Module.rank R M
have choose : ∀ (f : (b : M ⧸ M') → M) (hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b),
  #(↑(↑(Subtype.mk (p := fun (s : Set (M ⧸ M')) ↦ LinearIndepOn R id s) s hs) : Set (M ⧸ M')) : Type v) +
      #(↑(↑(Subtype.mk (p := fun (s : Set ↥M') ↦ LinearIndepOn R id s) t ht) : Set ↥M') : Type v) ≤
    Module.rank R M
Tactic: choose f hf using Submodule.Quotient.mk_surjective M'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ finrank R (ULift.{u_2, v} M) = finrank R M
have simp_rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u_2}) → ℕ) (Module.rank R (ULift.{u_2, v} M)) : ℕ)
  ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: simp_rw [finrank, rank_ulift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u_2}) → ℕ) (Module.rank R (ULift.{u_2, v} M)) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
⊢ finrank R (ULift.{u_2, v} M) = finrank R M
have simp_rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u_2}) → ℕ) (lift.{u_2, v} (Module.rank R M)) : ℕ)
  ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ)
Tactic: simp_rw [finrank, rank_ulift, toNat_lift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
| Module.rank R M + Module.rank R M₁
have simp : HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
  (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v))
Tactic: simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
⊢ Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)
have conv_lhs : HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
    (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v)) ≤
  Module.rank R (M × M₁)
Tactic: conv_lhs => simp only [Module.rank_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M M₁ : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Nontrivial R
⊢ HAdd.hAdd (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
      (⨆ (ι : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑ι : Set M₁) : Type v)) ≤
    Module.rank R (M × M₁)
have rw : ⨆ (i : { s : Set M // LinearIndepOn R id s }),
    ⨆ (j : { s : Set M₁ // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) + #(↑(↑j : Set M₁) : Type v) ≤
  Module.rank R (M × M₁)
Tactic: rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
inst_5 : Nontrivial R
⊢ lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
have rw : Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')
Tactic: rw [← rank_ulift, ← rank_ulift]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type w
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
have obtain : ∀ (fst : Type v) (bs : Basis fst R M), Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
Tactic: obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Constructions (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
ι : Type w
fst : Type v
bs : Basis fst R M
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)
have rw : Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} #fst
Tactic: rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]