awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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 : Bijective i
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
x : R
x_1 : M'
⊢ i x • x_1 = (j : (a : M) → M') (HSMul.hSMul (β := M) x (((↑j.symm : M' →+ M) : (a : M') → M) x_1 : M))

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M 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 (α := 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₁)
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injectiveₛ i j hi hj hc

Premises used: lift_rank_le_of_injective_injectiveₛ, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M 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 (α := 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₁)
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc

Premises used: lift_rank_le_of_surjective_injective, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M 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 : Bijective i
hc : ∀ (r : R) (m : M), (j : (a : M) → M₁) (r • m) = HSMul.hSMul (β := M₁) (i r) ((j : (a : M) → M₁) m : M₁)
⊢ Module.rank R M = Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc

Premises used: lift_rank_eq_of_equiv_equiv, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
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)
⊢ Module.rank R R = 1

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]

Premises used: Cardinal.two_le_iff_one_lt, Module.le_rank_iff_exists_linearMap, Module.one_le_rank_iff, not_lt, le_antisymm_iff, Nat.cast_two
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)

Tactic:
⟨fun ⟨f, inj⟩ ↦ ?_, _, (LinearEquiv.refl ..).injective⟩

Premises used: False, _private.0.CommSemiring.rank_self.match_1, And.intro, Exists.intro, LinearEquiv.refl, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u_1
inst : CommSemiring R
h : Nontrivial R
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
⊢ (¬∃ (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:
refine ⟨fun ⟨f, inj⟩ ↦ ?_, _, (LinearEquiv.refl ..).injective⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
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)
⊢ 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)

Tactic:
simp_rw [map_smul, smul_eq_mul]

Premises used: smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
⊢ 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:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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]
⊢ Eq (α := R) ((f : (a : Fin 2 → R) → R) ![0, 1] : R) (0 : R)

Tactic:
simpa using congr($this 0)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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]
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
⊢ Eq (α := R) (0 : R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R)

Tactic:
simpa using congr($this 1)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
h₂ : Eq (α := R) (0 : R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R)
⊢ Eq.{u_1 + 1} (α := R) 0 1

Tactic:
simpa using congr($(inj (h₁.trans h₂)) 1)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
h₂ : Eq (α := R) (0 : R) ((f : (a : Fin 2 → R) → R) ![1, 0] : R)
⊢ False

Tactic:
exact zero_ne_one (α := R) (by simpa using congr($(inj (h₁.trans h₂)) 1))

Premises used: zero_ne_one
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')
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'))
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Cardinal.bddAbove_of_small, Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')
x : { s : Set M // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x_1 : M
h_1 : Eq.{v' + 1} (α := M') ((j : (a : M) → M') x_1 : M') (0 : M')
rwa rwa₁ rwa₂ rwa₃ : Eq.{v' + 1} (α := M') ((j : (a : M) → M') x_1 : M') (0 : M')
⊢ Eq.{v' + 1} (α := M') ((j : (a : M) → M') x_1 : M') ((j : (a : M) → M') 0 : M')

Tactic:
rwa [j.map_zero]

Premises used: AddMonoidHom.map_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')
⊢ 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:
exact ciSup_mono_of_forall_exists' bddAbove_of_small fun ⟨s, h⟩ ↦
    ⟨⟨j '' s, LinearIndepOn.id_image <| h.linearIndependent.map_of_injective_injective i j hi
      (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

Premises used: ciSup_mono_of_forall_exists', Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type u
R' : Type u'
M 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 (α := 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₁)
⊢ Module.rank R M ≤ Module.rank R' M₁

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc

Premises used: lift_rank_le_of_injective_injective, Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')

Tactic:
_root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_

Premises used: AddMonoidHomClass.toAddMonoidHom, lift_rank_le_of_injective_injectiveₛ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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'
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')
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_

Premises used: lift_rank_le_of_injective_injectiveₛ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')
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')
⊢ ((↑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:
simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]

Premises used: AddMonoidHom.coe_coe, map_mul, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')

Tactic:
_root_.lift_rank_le_of_surjective_injective i j hi hj fun r _ ↦ ?_

Premises used: AddMonoidHomClass.toAddMonoidHom, lift_rank_le_of_surjective_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
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')
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_le_of_surjective_injective i j hi hj fun r _ ↦ ?_

Premises used: lift_rank_le_of_surjective_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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
this :
  Eq.{v' + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((i : (a : R) → R') r : R') : S')
    ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) r : S) : 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:
simp only [smul_def, AddMonoidHom.coe_coe, map_mul, this]

Premises used: AddMonoidHom.coe_coe, map_mul, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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')

Tactic:
_root_.lift_rank_eq_of_equiv_equiv i j i.bijective fun r _ ↦ ?_

Premises used: lift_rank_eq_of_equiv_equiv, AddEquivClass.toAddEquiv, RingEquiv.bijective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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)
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')
⊢ lift.{v', v} (Module.rank R S) = lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_eq_of_equiv_equiv i j i.bijective fun r _ ↦ ?_

Premises used: lift_rank_eq_of_equiv_equiv, RingEquiv.bijective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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
⊢ 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)
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
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
this :
  Eq.{v' + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((i : (a : R) → R') r : R') : S')
    ((j : (a : S) → S') ((algebraMap R S : (a : R) → S) r : S) : 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:
simp only [smul_def, RingEquiv.coe_toAddEquiv, map_mul, this]

Premises used: RingEquiv.coe_toAddEquiv, map_mul, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.Dimension.Basic
Goal:
R : Type w
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
R' : Type w'
inst_3 : CommSemiring R'
S' : Type v
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 (α := S) (β := S') (⇑j : (a : S) → S')
hc : RingHom.comp (j.comp (algebraMap R S)) i = algebraMap R' S'
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc

Premises used: Algebra.lift_rank_le_of_injective_injective, Cardinal.lift_id