-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem inertiaDeg_algebra_tower (p : Ideal R) (P : Ideal S) (I : Ideal T) [p.IsMaximal]
    [P.IsMaximal] [P.LiesOver p] [I.LiesOver P] : inertiaDeg p I =
    inertiaDeg p P * inertiaDeg P I

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Tactic:
letI : Algebra (S ⧸ P) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₂.le

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Tactic:
have h₁ := P.over_def p

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Tactic:
letI : Algebra (R ⧸ p) (S ⧸ P) := Ideal.Quotient.algebraQuotientOfLEComap h₁.le

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Tactic:
have h₃ := (LiesOver.trans I P p).over

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝² : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ I) :=
  IsScalarTower.of_algebraMap_eq fun x =>
    Quot.ind (fun x => congr_arg (Quot.mk ⇑(Submodule.quotientRel I)) (IsScalarTower.algebraMap_apply R S T x)) x
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Tactic:
exact (finrank_mul_finrank (R ⧸ p) (S ⧸ P) (T ⧸ I)).symm

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

Tactic:
simp only [inertiaDeg, dif_pos h₁.symm, dif_pos h₂.symm, dif_pos h₃.symm]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
⊢ finrank (R ⧸ p) (T ⧸ I) = finrank (R ⧸ p) (S ⧸ P) * finrank (S ⧸ P) (T ⧸ I)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
⊢ ∀ (x : R ⧸ p), (algebraMap (R ⧸ p) (T ⧸ I)) x = (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) x)

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this✝ : Algebra (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x✝ : R ⧸ p
x : R
⊢ (algebraMap (R ⧸ p) (T ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel p)) x) =
    (algebraMap (S ⧸ P) (T ⧸ I)) ((algebraMap (R ⧸ p) (S ⧸ P)) (Quot.mk (⇑(Submodule.quotientRel p)) x))