awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
⊢ x ∈ HSMul.hSMul (β := Submodule A V) a ⊤ ↔ Membership.mem (γ := Submodule A V) ⊤ x
have h : Membership.mem (γ := Submodule A V) ⊤ x → x ∈ HSMul.hSMul (β := Submodule A V) a ⊤
Tactic: refine ⟨fun _ ↦ trivial, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M : Submodule R V
inst_7 : IsLattice A M
a : Aˣ
x : V
h : Membership.mem (γ := Submodule A V) ⊤ x
⊢ x ∈ HSMul.hSMul (β := Submodule A V) a ⊤
have h : a • a⁻¹ • x ∈ HSMul.hSMul (β := Submodule A V) a ⊤
Tactic: rw [show x = a • a⁻¹ • x by simp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Module A V
inst_6 : IsScalarTower R A V
M N : Submodule R V
hle : M ≤ N
inst_7 : IsLattice A M
hfg : N.FG
⊢ LE.le (α := Submodule A V) ⊤ (span A (↑M : Set V))
have rw : LE.le.{u_3} (α := Submodule A V) ⊤ ⊤
Tactic: rw [IsLattice.span_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have obtain : ∀ (s : Set M) (hs : Cardinal.mk (↑s : Type u) = Module.rank R M)
  (hli : LinearIndependent.{u, u_1, u} (ι := (↑s : Type u)) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))),
  Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
Tactic: obtain ⟨s, hs, hli⟩ := exists_set_linearIndependent R M
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent.{u, u_1, u} (ι := (↑s : Type u)) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have hli₁ : LinearIndependent (ι := (↑s : Type u)) R (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: replace hli := hli.map' f (LinearMap.ker_eq_bot.mpr hf)
Cleared hypotheses: hli
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent (ι := (↑s : Type u)) R (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have hli₁ : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
Tactic: rw [LinearIndependent.iff_fractionRing (R := R) (K := K)] at hli
Cleared hypotheses: hli
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hs : Cardinal.mk (↑s : Type u) = Module.rank R M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have hs₁ : Cardinal.mk (↑s : Type u) = Module.rank K N
Tactic: replace hs : Cardinal.mk s = Module.rank K N :=
    le_antisymm (LinearIndependent.cardinal_le_rank hli) (hs ▸ h)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hs : Cardinal.mk (↑s : Type u) = Module.rank K N
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have hs₁ : ∃ (h : Fintype (↑s : Type u)), Fintype.card.{u} (↑s : Type u) = finrank K N
Tactic: rw [← Module.finrank_eq_rank, Cardinal.mk_eq_nat_iff_fintype] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hs : ∃ (h : Fintype (↑s : Type u)), Fintype.card.{u} (↑s : Type u) = finrank K N
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have obtain : ∀ (hfin : Fintype (↑s : Type u)) (hcard : Fintype.card.{u} (↑s : Type u) = finrank K N),
  Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
Tactic: obtain ⟨hfin, hcard⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have hsubset : (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)
Tactic: have hsubset : Set.range (fun x : s ↦ f x.val) ⊆ (LinearMap.range f : Set N) := by
    rintro x ⟨a, rfl⟩
    simp
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
M N : Type u
inst_3 : IsDomain R
inst_4 : IsFractionRing R K
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module K N
inst_10 : IsScalarTower R K N
inst_11 : Module.Finite K N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
h : Module.rank K N ≤ Module.rank R M
s : Set M
hli : LinearIndependent (ι := (↑s : Type u)) K (M := N) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))
hfin : Fintype (↑s : Type u)
hcard : Fintype.card.{u} (↑s : Type u) = finrank K N
hsubset : (Set.range fun (x : (↑s : Type u)) ↦ (f : (a : M) → N) (↑x : M)) ⊆ (↑f.range : Set N)
⊢ Eq (α := Submodule K N) (span K (↑f.range : Set N)) ⊤
have rw : LE.le (α := Submodule K N)
  (span K (Set.range (ι := (↑s : Type u)) ((⇑f : (a : M) → N) ∘ Subtype.val (p := fun (x : M) ↦ x ∈ s))))
  (span K (↑f.range : Set N))
Tactic: rw [eq_top_iff, ← LinearIndependent.span_eq_top_of_card_eq_finrank' hli hcard]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
⊢ LinearIndependent.{u_4, u_2, u_3} K (M := V) fun (i : κ) ↦ (↑((b : (a : κ) → ↥M) i) : V)
have rw : ∀ (s : Finset κ) (g : κ → R),
  Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (↑((b : (a : κ) → ↥M) i) : V)) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [← LinearIndependent.iff_fractionRing (R := R), linearIndependent_iff']
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
s : Finset κ
g : κ → R
hs : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (↑((b : (a : κ) → ↥M) i) : V)) 0
⊢ ∀ i ∈ s, g i = 0
have hs₁ : Eq.{u_3 + 1} (α := ↥M) (∑ i ∈ s, HSMul.hSMul (β := ↥M) (g i) ((b : (a : κ) → ↥M) i : ↥M)) 0
Tactic: simp_rw [← Submodule.coe_smul_of_tower, ← Submodule.coe_sum, Submodule.coe_eq_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
hli : LinearIndependent.{u_4, u_2, u_3} K (M := V) fun (i : κ) ↦ (↑((b : (a : κ) → ↥M) i) : V)
⊢ LE.le.{u_3} (α := Submodule K V) ⊤
    (span K (Set.range fun (i : κ) ↦ Function.comp (β := ↥M) (⇑M.subtype : (a : ↥M) → V) (⇑b : (a : κ) → ↥M) i))
have rw : LE.le (α := Submodule K V) ⊤
  (span K (↑(map M.subtype (span R (Set.range.{u_3, u_4 + 1} (ι := κ) (⇑b : (a : κ) → ↥M)))) : Set V))
Tactic: rw [← Submodule.span_span_of_tower R, Set.range_comp, ← Submodule.map_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsTorsionFree R K
M : Submodule R V
inst_10 : IsLattice K M
⊢ Free.{u_1, u_3} R ↥M
have this : IsTorsionFree R V
Tactic: have := Module.IsTorsionFree.trans_faithfulSMul R K V
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsFractionRing R K
M : Submodule R V
inst_10 : IsLattice K M
b : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R ↥M) R ↥M := Free.chooseBasis R ↥M
⊢ Module.rank R ↥M = Module.rank K V
have rw : (↑(Fintype.card.{u_3} (Free.ChooseBasisIndex R ↥M)) : Cardinal.{u_3}) = Module.rank K V
Tactic: rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsFractionRing R K
M : Submodule R V
inst_10 : IsLattice K M
b : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R ↥M) R ↥M := Free.chooseBasis R ↥M
rw : (↑(Fintype.card.{u_3} (Free.ChooseBasisIndex R ↥M)) : Cardinal.{u_3}) = Module.rank K V
⊢ Module.rank R ↥M = Module.rank K V
have rw₁ : Module.rank K V = Module.rank K V
Tactic: rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
ι : Type u_4
inst_5 : Fintype ι
inst_6 : IsFractionRing R K
M : Submodule R (ι → K)
inst_7 : IsLattice K M
⊢ Module.rank R ↥M = (↑(Fintype.card ι) : Cardinal.{max u_2 u_4})
have rw : Module.rank K (ι → K) = (↑(Fintype.card ι) : Cardinal.{max u_2 u_4})
Tactic: rw [IsLattice.rank' K M]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ (M ⊓ N).FG
have this : IsNoetherian.{u_1, u_3} R ↥(M ⊓ N)
Tactic: have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le inf_le_left
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
this : IsNoetherian.{u_1, u_3} R ↥(M ⊓ N)
⊢ (M ⊓ N).FG
have rw : Module.Finite.{u_1, u_3} R ↥(M ⊓ N)
Tactic: rw [← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ Eq (α := Submodule K V) (span K (↑(M ⊓ N) : Set V)) ⊤
have rw : Eq (α := Submodule K V) (span K (↑(M ⊓ N).subtype.range : Set V)) ⊤
Tactic: rw [← range_subtype (M ⊓ N)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ Eq (α := Submodule K V) (span K (↑(M ⊓ N).subtype.range : Set V)) ⊤
have apply : Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
Tactic: apply Submodule.span_range_eq_top_of_injective_of_rank_le (M ⊓ N).injective_subtype
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
have h : Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank R ↥M + Module.rank R ↥N
Tactic: have h := Submodule.rank_sup_add_rank_inf_eq M N
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
h : Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank R ↥M + Module.rank R ↥N
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
have h₁ : Module.rank K V + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank K V
Tactic: rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Lattice (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
h : Module.rank K V + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank K V
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
have rw : Module.rank K V ≤ Module.rank K V
Tactic: rw [Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
⊢ HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') (c • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') ((σ₁₂ : (a : R) → R') c : R')
      (HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') x)
have simp_rw : (f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') (c • x)) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := R') (β := M') ((σ₁₂ : (a : R) → R') c : R')
    ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')
Tactic: simp_rw [DomMulAct.smul_apply, ← smul_comm, f.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
simp_rw :
  (f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') (c • x)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') (β := M') ((σ₁₂ : (a : R) → R') c : R')
      ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')
⊢ HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') (c • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') ((σ₁₂ : (a : R) → R') c : R')
      (HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') x)
have simp_rw₁ : (f : (a : M) → M') (c • HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) =
  HSMul.hSMul.{u_2, u_5, u_5} (α := R') (β := M') ((σ₁₂ : (a : R) → R') c : R')
    ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')
Tactic: simp_rw [DomMulAct.smul_apply, ← smul_comm, f.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
inst_12 : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ Eq.{u_5 + 1} (α := M') ((s • t • f : (a : M) → M') m : M') ((t • s • f : (a : M) → M') m : M')
have simp_rw : Eq.{u_5 + 1} (α := M')
  ((f : (a : M) → M')
      (HSMul.hSMul (α := T') ((Equiv.symm DomMulAct.mk : (a : T'ᵈᵐᵃ) → T') t : T')
        (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') s : S') m)) :
    M')
  ((f : (a : M) → M')
      (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') s : S')
        (HSMul.hSMul (α := T') ((Equiv.symm DomMulAct.mk : (a : T'ᵈᵐᵃ) → T') t : T') m)) :
    M')
Tactic: simp_rw [DomMulAct.smul_linearMap_apply, smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
inst_6 : Semiring S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : SMulCommClass R' S M'
inst_10 : SMulCommClass R S M
x x_1 : Sᵈᵐᵃ
x_2 : M →ₛₗ[σ₁₂] M'
x_3 : M
⊢ Eq.{u_5 + 1} (α := M') (((x + x_1) • x_2 : (a : M) → M') x_3 : M') ((x • x_2 + x_1 • x_2 : (a : M) → M') x_3 : M')
have simp_rw : Eq.{u_5 + 1} (α := M')
  ((x_2 : (a : M) → M') (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (x + x_1) : S) x_3) : M')
  ((x_2 : (a : M) → M')
      (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x : S)
          ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x_1 : S) •
        x_3) :
    M')
Tactic: simp_rw [add_apply, DomMulAct.smul_linearMap_apply, ← map_add, ← add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b : A
⊢ Eq (α := A →ₗ[R] A) (mulLeft R (a * b)) (mulLeft R a ∘ₗ mulLeft R b)
have h : ∀ (x : A), Eq (α := A) ((mulLeft R (a * b) : (a : A) → A) x : A) ((mulLeft R a ∘ₗ mulLeft R b : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : A
⊢ Eq (α := A →ₗ[R] A) (mulRight R (a * b)) (mulRight R b ∘ₗ mulRight R a)
have h : ∀ (x : A), Eq (α := A) ((mulRight R (a * b) : (a : A) → A) x : A) ((mulRight R b ∘ₗ mulRight R a : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Basic (goal)
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
⊢ Sum.elim 0 (f + g) = HAdd.hAdd (α := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g)
have h : ∀ (i : κ),
  Sum.elim 0 (f + g) (inl i) = HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inl i)
Tactic: ext (i | i)