-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_le_of_surjective_injective
    (i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j)
    (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    lift.{v'} (Module.rank R S) ≤ lift.{v} (Module.rank R' S')

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : ((algebraMap R' S').comp i) r = (j.comp (algebraMap R S)) r
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
simp only [RingHom.coe_comp, comp_apply] at this

Result:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)
⊢ ↑j (r • x✝) = i r • ↑j x✝

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
simp only [smul_def, AddMonoidHom.coe_coe, map_mul, ZeroHom.coe_coe, this]

Result:
no goals

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
have := congr($hc r)

Result:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
this : ((algebraMap R' S').comp i) r = (j.comp (algebraMap R S)) r
⊢ ↑j (r • x✝) = i r • ↑j x✝

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R 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 _ ↦ ?_

Result:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
r : R
x✝ : S
⊢ ↑j (r • x✝) = i r • ↑j x✝