awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
⊢ Module.rank R M = 1
have h₁ : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ 1
Tactic: rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
h₁ : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ 1
⊢ Module.rank R M = 1
have h₂ : ∀ w < 1, ∃ (i : { s : Set M // LinearIndepOn R id s }), w < #(↑(↑i : Set M) : Type v)
Tactic: rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
⊢ ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ 1
have this : Subsingleton M
Tactic: have := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ 1 ≤ Module.rank R M ↔ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
⊢ 1 ≤ Module.rank R M ↔ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
have refine_1 : (∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)) →
  ∀ (f : (Fin 1 → R) →ₗ[R] M) (hf : Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)),
    ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
Tactic: refine le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Nontrivial R
refine_1 :
  (∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)) →
    ∀ (f : (Fin 1 → R) →ₗ[R] M) (hf : Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)),
      ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
⊢ 1 ≤ Module.rank R M ↔ ∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)
have refine_2 : (∃ (f : R →ₗ[R] M), Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)) →
  ∀ (f : R →ₗ[R] M) (hf : Injective.{u + 1, v + 1} (α := R) (β := M) (⇑f : (a : R) → M)),
    ∃ (f : (Fin 1 → R) →ₗ[R] M), Injective.{u + 1, v + 1} (α := Fin 1 → R) (β := M) (⇑f : (a : Fin 1 → R) → M)
Tactic: refine le_rank_iff_exists_linearMap.trans ⟨fun ⟨f, hf⟩ ↦ ?_, fun ⟨f, hf⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
have simp_rw : LE.le (α := Cardinal.{max v v'}) (⨆ (i : { s : Set M // LinearIndepOn R id s }), lift.{v', v} #(↑(↑i : Set M) : Type v))
  (⨆ (i : { s : Set M' // LinearIndepOn R' id s }), lift.{v, v'} #(↑(↑i : Set M') : Type v'))
Tactic: simp_rw [Module.rank, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
have obtain : ∀ (i' : R' → R) (hi' : RightInverse i' i), lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
Tactic: obtain ⟨i', hi'⟩ := hi.hasRightInverse
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
have refine_1 : ∀ (x x_1 : R') (h : i' x = i' x_1), x = x_1
Tactic: refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
refine_1 : ∀ (x x_1 : R') (h : i' x = i' x_1), x = x_1
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
have refine_2 : ∀ (r : R') (m : M), (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i' x = i' x_1
⊢ x = x_1
have h₁ : i (i' x) = i (i' x_1)
Tactic: apply_fun i at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i (i' x) = i (i' x_1)
⊢ x = x_1
have refine_1 : ∀ (h : x = i (i' x_1)), x = x_1
Tactic: rwa [hi', hi'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i (i' x) = i (i' x_1)
refine_1 : ∀ (h : x = i (i' x_1)), x = x_1
⊢ x = x_1
have refine_1₁ : ∀ (h : x = x_1), x = x_1
Tactic: rwa [hi', hi'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
have refine_2 : HSMul.hSMul (β := M') (i (i' r)) ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: rw [hc (i' r) m, hi']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
refine_2 :
  HSMul.hSMul (β := M') (i (i' r)) ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
have refine_2₁ : HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: rw [hc (i' r) m, hi']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Module.rank R R = 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
⊢ Module.rank R R = 1
have rw : (¬∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)) ∧
  ∃ (f : R →ₗ[R] R), Injective (α := R) (β := R) (⇑f : (a : R) → R)
Tactic: rw [le_antisymm_iff, ← not_lt, ← two_le_iff_one_lt, ← Nat.cast_two,
    Module.le_rank_iff_exists_linearMap, Module.one_le_rank_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
⊢ (¬∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)) ∧
    ∃ (f : R →ₗ[R] R), Injective (α := R) (β := R) (⇑f : (a : R) → R)
have refine : (∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)) →
  ∀ (f : (Fin 2 → R) →ₗ[R] R) (inj : Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)), False
Tactic: refine ⟨fun ⟨f, inj⟩ ↦ ?_, _, (LinearEquiv.refl ..).injective⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
h_1 : ∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
f : (Fin 2 → R) →ₗ[R] R
inj : Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
⊢ Eq (α := R)
    ((f : (a : Fin 2 → R) → R)
        (HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) ![1, 0]) :
      R)
    ((f : (a : Fin 2 → R) → R)
        (HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) ![0, 1]) :
      R)
have simp_rw : HMul.hMul (α := R) (β := R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) =
  HMul.hMul (α := R) (β := R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R)
Tactic: simp_rw [map_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
h_1 : ∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
f : (Fin 2 → R) →ₗ[R] R
inj : Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
⊢ False
have this : HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) ![1, 0] =
  HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) ![0, 1]
Tactic: have := inj (a₁ := f ![0, 1] • ![1, 0]) (a₂ := f ![1, 0] • ![0, 1]) <| by
    simp_rw [map_smul, smul_eq_mul]; apply mul_comm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
h_1 : ∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
f : (Fin 2 → R) →ₗ[R] R
inj : Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
this :
  HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) ![1, 0] =
    HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) ![0, 1]
⊢ False
have h₁ : Eq (α := R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) (0 : R)
Tactic: have h₁ : f ![0, 1] = 0 := by simpa using congr($this 0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
h_1 : ∃ (f : (Fin 2 → R) →ₗ[R] R), Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
f : (Fin 2 → R) →ₗ[R] R
inj : Injective (α := Fin 2 → R) (β := R) (⇑f : (a : Fin 2 → R) → R)
this :
  HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) ![1, 0] =
    HSMul.hSMul (α := R) (β := Fin (Nat.succ 0).succ → R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R) ![0, 1]
h₁ : Eq (α := R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) (0 : R)
⊢ False
have h₂ : Eq (α := R) (0 : R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R)
Tactic: have h₂ : 0 = f ![1, 0] := by simpa using congr($this 1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Ring R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective.{v + 1, v' + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
have simp_rw : LE.le (α := Cardinal.{max v v'}) (⨆ (i : { s : Set M // LinearIndepOn R id s }), lift.{v', v} #(↑(↑i : Set M) : Type v))
  (⨆ (i : { s : Set M' // LinearIndepOn R' id s }), lift.{v, v'} #(↑(↑i : Set M') : Type v'))
Tactic: simp_rw [Module.rank, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective.{w' + 1, w + 1} (α := R') (β := R) (⇑i : (a : R') → R)
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')
have refine : ∀ (r : R') (x : S),
  ((↑j : S →+ S') : (a : S) → S') (HSMul.hSMul.{w, v, v} (α := R) ((i : (a : R') → R) r : R) x) =
    HSMul.hSMul (β := S') r (((↑j : S →+ S') : (a : S) → S') x : S')
Tactic: refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective.{w' + 1, w + 1} (α := R') (β := R) (⇑i : (a : R') → R)
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
r : R'
x : S
⊢ ((↑j : S →+ S') : (a : S) → S') (HSMul.hSMul.{w, v, v} (α := R) ((i : (a : R') → R) r : R) x) =
    HSMul.hSMul (β := S') r (((↑j : S →+ S') : (a : S) → S') x : S')
have this : Eq.{v' + 1} (α := S') ((RingHom.comp (j.comp (algebraMap R S)) i : (a : R') → S') r : S')
  ((algebraMap R' S' : (a : R') → S') r : S')
Tactic: have := congr($hc r)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective.{w' + 1, w + 1} (α := R') (β := R) (⇑i : (a : R') → R)
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
r : R'
x : S
this :
  Eq.{v' + 1} (α := S') ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) : S')
    ((algebraMap R' S' : (a : R') → S') r : S')
⊢ ((↑j : S →+ S') : (a : S) → S') (HSMul.hSMul.{w, v, v} (α := R) ((i : (a : R') → R) r : R) x) =
    HSMul.hSMul (β := S') r (((↑j : S →+ S') : (a : S) → S') x : S')
have simp_rw : ((↑j : S →+ S') : (a : S) → S') (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) x) =
  HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') (((↑j : S →+ S') : (a : S) → S') x : S')
Tactic: simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective.{w' + 1, w + 1} (α := R') (β := R) (⇑i : (a : R') → R)
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
r : R'
x : S
this :
  Eq.{v' + 1} (α := S') ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) : S')
    ((algebraMap R' S' : (a : R') → S') r : S')
simp_rw :
  ((↑j : S →+ S') : (a : S) → S')
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) x) =
    HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') (((↑j : S →+ S') : (a : S) → S') x : S')
⊢ ((↑j : S →+ S') : (a : S) → S') (HSMul.hSMul.{w, v, v} (α := R) ((i : (a : R') → R) r : R) x) =
    HSMul.hSMul (β := S') r (((↑j : S →+ S') : (a : S) → S') x : S')
have simp_rw₁ : (j : (a : S) → S') (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) x) =
  HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') ((j : (a : S) → S') x : S')
Tactic: simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective.{w' + 1, w + 1} (α := R') (β := R) (⇑i : (a : R') → R)
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
r : R'
x : S
this :
  Eq.{v' + 1} (α := S') ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) : S')
    ((algebraMap R' S' : (a : R') → S') r : S')
simp_rw :
  ((↑j : S →+ S') : (a : S) → S')
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) x) =
    HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') (((↑j : S →+ S') : (a : S) → S') x : S')
simp_rw₁ :
  (j : (a : S) → S') (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) x) =
    HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') ((j : (a : S) → S') x : S')
⊢ ((↑j : S →+ S') : (a : S) → S') (HSMul.hSMul.{w, v, v} (α := R) ((i : (a : R') → R) r : R) x) =
    HSMul.hSMul (β := S') r (((↑j : S →+ S') : (a : S) → S') x : S')
have simp_rw₂ : HMul.hMul (α := S') (β := S') ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) ((i : (a : R') → R) r : R) : S) : S')
    ((j : (a : S) → S') x : S') =
  HMul.hMul (α := S') (β := S') ((algebraMap R' S' : (a : R') → S') r : S') ((j : (a : S) → S') x : S')
Tactic: simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective.{w + 1, w' + 1} (α := R) (β := R') (⇑i : (a : R) → R')
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (algebraMap R' S') i = j.comp (algebraMap R S)
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')
have refine : ∀ (r : R) (x : S),
  ((↑j : S →+ S') : (a : S) → S') (r • x) =
    HSMul.hSMul.{w', v', v'} (α := R') (β := S') ((i : (a : R) → R') r : R') (((↑j : S →+ S') : (a : S) → S') x : S')
Tactic: refine _root_.lift_rank_le_of_surjective_injective i j hi hj fun r _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective.{w + 1, w' + 1} (α := R) (β := R') (⇑i : (a : R) → R')
hj : Injective.{v + 1, v' + 1} (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (algebraMap R' S') i = j.comp (algebraMap R S)
r : R
x : S
⊢ ((↑j : S →+ S') : (a : S) → S') (r • x) =
    HSMul.hSMul.{w', v', v'} (α := R') (β := S') ((i : (a : R) → R') r : R') (((↑j : S →+ S') : (a : S) → S') x : S')
have this : Eq.{v' + 1} (α := S') ((RingHom.comp (algebraMap R' S') i : (a : R) → S') r : S')
  ((j.comp (algebraMap R S) : (a : R) → S') r : S')
Tactic: have := congr($hc r)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (goal)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : RingHom.comp (algebraMap R' S') i.toRingHom = j.toRingHom.comp (algebraMap R S)
⊢ lift.{v', v} (Module.rank R S) = lift.{v, v'} (Module.rank R' S')
have refine : ∀ (r : R) (x : S),
  ((↑j : S ≃+ S') : (a : S) → S') (r • x) =
    HSMul.hSMul.{w', v', v'} (α := R') (β := S') ((i : (a : R) → R') r : R') (((↑j : S ≃+ S') : (a : S) → S') x : S')
Tactic: refine _root_.lift_rank_eq_of_equiv_equiv i j i.bijective fun r _ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Basic (hypothesis)
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
S' : Type v'
inst_3 : CommSemiring R'
inst_4 : Semiring S'
inst_5 : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : RingHom.comp (algebraMap R' S') i.toRingHom = j.toRingHom.comp (algebraMap R S)
r : R
x : S
⊢ ((↑j : S ≃+ S') : (a : S) → S') (r • x) =
    HSMul.hSMul.{w', v', v'} (α := R') (β := S') ((i : (a : R) → R') r : R') (((↑j : S ≃+ S') : (a : S) → S') x : S')
have this : Eq.{v' + 1} (α := S') ((RingHom.comp (algebraMap R' S') i.toRingHom : (a : R) → S') r : S')
  ((j.toRingHom.comp (algebraMap R S) : (a : R) → S') r : S')
Tactic: have := congr($hc r)