-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_mul_relrank (h1 : A ≤ B) (h2 : B ≤ C) :
    relrank A B * relrank B C = relrank A C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
letI : Algebra A B := (inclusion h1).toAlgebra

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this : Algebra ↥A ↥B := (inclusion h1).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝² : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this✝¹ : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this✝ : Algebra ↥A ↥C := (inclusion h3).toAlgebra
this : IsScalarTower ↥A ↥B ↥C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
exact rank_mul_rank A B C

Result:
no goals

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
have h3 := h1.trans h2

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝¹ : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this✝ : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this : Algebra ↥A ↥C := (inclusion h3).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
haveI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' rfl

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝² : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this✝¹ : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this✝ : Algebra ↥A ↥C := (inclusion h3).toAlgebra
this : IsScalarTower ↥A ↥B ↥C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this : Algebra ↥A ↥B := (inclusion h1).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
letI : Algebra B C := (inclusion h2).toAlgebra

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝ : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this : Algebra ↥B ↥C := (inclusion h2).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝ : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this : Algebra ↥B ↥C := (inclusion h2).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
letI : Algebra A C := (inclusion h3).toAlgebra

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this✝¹ : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this✝ : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this : Algebra ↥A ↥C := (inclusion h3).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
rw [relrank_eq_rank_of_le h1, relrank_eq_rank_of_le h2, relrank_eq_rank_of_le h3]

Result:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)