awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) (sec '' t)
have refine_2 : LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
  ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) '' sec '' t)
Tactic: rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
refine_2 :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) '' sec '' t)
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) (sec '' t)
have refine_2₁ : LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
  ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec '' t)
Tactic: rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
refine_2 :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) '' sec '' t)
refine_2₁ :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec '' t)
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) (sec '' t)
have refine_2₂ : LinearIndepOn R _root_.id (_root_.id '' t)
Tactic: rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht : #(↑t : Type u) = Module.rank R (HasQuotient.Quotient M (B := Submodule R M) (span R s))
ht' :
  LinearIndependent.{u, u_1, u} (ι := (↑t : Type u)) R
    (Subtype.val (p := fun (x : HasQuotient.Quotient M (B := Submodule R M) (span R s)) ↦ x ∈ t))
sec : (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)) → M
hsec :
  ∀ (b : HasQuotient.Quotient M (B := Submodule R M) (span R s)), (mkQ (span R s) : (a : M) → M ⧸ span R s) (sec b) = b
hsec' : (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
refine_2 :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) '' sec '' t)
refine_2₁ :
  LinearIndepOn (ι := HasQuotient.Quotient M (B := Submodule R M) (span R s)) R _root_.id
    ((⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) ∘ sec '' t)
refine_2₂ : LinearIndepOn R _root_.id (_root_.id '' t)
⊢ LinearIndepOn R (M := HasQuotient.Quotient M (B := Submodule R M) (span R s))
    (⇑(mkQ (span R s)) : (a : M) → M ⧸ span R s) (sec '' t)
have refine_2₃ : LinearIndepOn R _root_.id t
Tactic: rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
have obtain : ∀ (t : Set M) (h₁ : Set.range v ⊆ t) (h₂ : #(↑t : Type u) = Module.rank R M) (h₃ : LinearIndepOn R _root_.id t),
  ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
Tactic: obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndepOn_of_lt_rank hv.linearIndepOn_id
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ Set.range v ≠ t
have refine : ∀ (e : Set.range v = t), (↑n : Cardinal.{u}) = Module.rank R M
Tactic: refine fun e ↦ h.ne ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
⊢ (↑n : Cardinal.{u}) = Module.rank R M
have h₄ : lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)
Tactic: rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
Cleared hypotheses: h₂, h₃, e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
have this : Set.range v ≠ t
Tactic: have : range v ≠ t := by
    refine fun e ↦ h.ne ?_
    rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂
    simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #(↑t : Type u) = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
have obtain : ∀ (x : M) (hx : x ∈ t) (hx' : x ∉ Set.range v),
  ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)
Tactic: obtain ⟨x, hx, hx'⟩ := nonempty_of_ssubset (h₁.ssubset_of_ne this)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
⊢ ∃ (x : M), LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M) v x)
have simp : ∃ (x : M),
  LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
    Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
Tactic: simp only [Fin.snoc_eq_cons_rotate]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : (↑n : Cardinal.{u}) < Module.rank R M
⊢ ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
have have : ∀ (x : M)
  (hx : LinearIndependent.{0, u_1, u} (ι := Fin (n + 1)) R (M := M) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M) x v)),
  ∃ (x : M),
    LinearIndependent.{0, u_1, u} R (M := M) fun (i : Fin (n + 1)) ↦
      Fin.cons (α := fun (x : Fin (n + 1)) ↦ M) x v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)
Tactic: have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
⊢ ∃ (y : M), LinearIndependent R ![x, y]
have obtain : ∀ (y : M)
  (hy :
    LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
      (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)),
  ∃ (y : M), LinearIndependent R ![x, y]
Tactic: obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (.of_subsingleton (v := ![x]) 0 hx) h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
⊢ ∃ (y : M), LinearIndependent R ![x, y]
have this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
Tactic: have : Fin.snoc ![x] y = ![x, y] := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
inst_4 : IsDomain R
inst_5 : StrongRankCondition R
inst_6 : IsTorsionFree R M
h : 1 < Module.rank R M
x : M
hx : x ≠ 0
y : M
hy :
  LinearIndependent.{0, u_1, u} (ι := Fin (Nat.succ 0 + 1)) R (M := M)
    (Fin.snoc (α := fun (a : Fin (Nat.succ 0 + 1)) ↦ M) ![x] y)
this : Fin.snoc (α := fun (a : Fin (Nat.succ 0).succ) ↦ M) ![x] y = ![x, y]
⊢ ∃ (y : M), LinearIndependent R ![x, y]
have hy₁ : LinearIndependent R ![x, y]
Tactic: rw [this] at hy
Cleared hypotheses: hy, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
e : Module.rank R (M ⧸ N) = 0
⊢ False
have h₁ : Module.rank R ↥N < Module.rank R ↥N
Tactic: rw [← rank_quotient_add_rank N, e, zero_add] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have this : Module.rank R (M ⧸ N) ≠ 0
Tactic: have : Module.rank R (M ⧸ N) ≠ 0 := by
    intro e
    rw [← rank_quotient_add_rank N, e, zero_add] at h
    exact h.ne rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : Module.rank R (M ⧸ N) ≠ 0
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have this₁ : ¬∀ (x : M), ∃ (a : R), a ≠ 0 ∧ HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) = 0
Tactic: rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ¬∀ (x : M), ∃ (a : R), a ≠ 0 ∧ HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) = 0
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have this₁ : ∃ (x : M), ∀ (a : R) (_ : a ≠ 0), HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) ≠ 0
Tactic: push Not at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (hypothesis)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ∃ (x : M), ∀ (a : R) (_ : a ≠ 0), HSMul.hSMul (β := M ⧸ N) a (Quotient.mk x) ≠ 0
⊢ ∃ (m : M), ∀ (r : R), r ≠ 0 → r • m ∉ N
have this₁ : ∃ (x : M), ∀ (a : R) (_ : ¬a = 0), a • x ∉ N
Tactic: simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
| Module.rank R ↥s + Module.rank R ↥t
have enter : Module.rank R ↥t
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
| Module.rank R ↥t
have rw : Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [show t = (s ⊔ t) ⊓ t by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
| Module.rank R ↥s + Module.rank R ↥t
have enter : Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t
have conv_rhs : Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw : Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₁ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₂ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
    Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₃ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
    Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.RankNullity (goal)
Goal:
R : Type u_1
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : HasRankNullity.{u, u_1} R
s t : Submodule R M
rw :
  Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₁ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype (s ⊓ t)) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₂ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥s ⧸ comap s.subtype s ⊓ comap s.subtype t) +
        Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
rw₃ :
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
⊢ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥((s ⊔ t) ⊓ t)
have rw₄ : Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ t) =
  Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
    Module.rank R ↥((s ⊔ t) ⊓ t)
Tactic: rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype),
    ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype),
    comap_inf, (quotientInfEquivSupQuotient s t).rank_eq, ← comap_inf,
    (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype,
    (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype,
    ← inf_assoc, inf_idem, add_right_comm]