awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
pos : ∀ (h : P.LiesOver p), p.inertiaDeg (comap e P) = p.inertiaDeg P
neg : ∀ (h : ¬P.LiesOver p), p.inertiaDeg (comap e P) = p.inertiaDeg P
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
by_cases h : P.LiesOver p

Premises used: Ideal.LiesOver
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : P.LiesOver p
pos : finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (comap e P)) = finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P)
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (comap e P)) = finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P)

Tactic:
(Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq

Premises used: LinearEquiv.finrank_eq, AlgEquiv.toLinearEquiv, Ideal.Quotient.algEquivOfEqComap, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (comap e P)) = finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P)

Tactic:
exact (Quotient.algEquivOfEqComap p e rfl).toLinearEquiv.finrank_eq

Premises used: LinearEquiv.finrank_eq, AlgEquiv.toLinearEquiv, Ideal.Quotient.algEquivOfEqComap, rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : ¬P.LiesOver p
neg : 0 = p.inertiaDeg P
⊢ p.inertiaDeg (comap e P) = p.inertiaDeg P

Tactic:
rw [inertiaDeg, dif_neg (fun eq => h ⟨(he.mp eq).symm⟩)]

Premises used: Ideal.inertiaDeg, Ideal.LiesOver.mk, dif_neg, Iff.mp, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap (F := R →+* S) f (comap e P) = p ↔ comap (F := R →+* S₁) (algebraMap R S₁) P = p
h : ¬P.LiesOver p
neg :
  Eq (α := ℕ) 0 (if hPp : comap (F := R →+* S₁) (algebraMap R S₁) P = p then finrank.{u, u_1} (R ⧸ p) (S₁ ⧸ P) else 0)
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ 0 = p.inertiaDeg P

Tactic:
rw [inertiaDeg, dif_neg (fun eq => h ⟨eq.symm⟩)]

Premises used: Ideal.inertiaDeg, Ideal.LiesOver.mk, dif_neg
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
P : Ideal S
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
e : E
rw : p.inertiaDeg (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.inertiaDeg P
⊢ inertiaDeg.{u, u_1} (S := S₁) p (map e P) = p.inertiaDeg P

Tactic:
rw [show P.map e = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]

Premises used: RingEquivClass.toRingEquiv, Ideal.map_comap_of_equiv
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
P : Ideal S
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.inertiaDeg P

Tactic:
p.inertiaDeg_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Premises used: Ideal.inertiaDeg_comap_eq, AlgEquiv.symm, AlgEquivClass.toAlgEquiv, Ideal.comap, RingEquiv.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
S₁ : Type u_1
inst_3 : CommRing S₁
inst_4 : Algebra R S₁
P : Ideal S
E : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
e : E
⊢ p.inertiaDeg (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.inertiaDeg P

Tactic:
exact p.inertiaDeg_comap_eq (AlgEquivClass.toAlgEquiv e).symm P

Premises used: Ideal.inertiaDeg_comap_eq, AlgEquiv.symm, AlgEquivClass.toAlgEquiv
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP : LiesOver.{u, v} (A := R) P ⊥
rw : finrank.{u, v} (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P) = finrank R S
⊢ inertiaDeg.{u, v} (R := R) ⊥ P = finrank R S

Tactic:
rw [inertiaDeg, dif_pos (over_def P (⊥ : Ideal R)).symm]

Premises used: Ideal.inertiaDeg, dif_pos, Bot.bot, Ideal.over_def, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP : LiesOver.{u, v} (A := R) P ⊥
⊢ P = ⊥

Tactic:
replace hP : P = ⊥ := eq_bot_of_liesOver_bot R P
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP_1 : LiesOver.{u, v} (A := R) P ⊥
hP : P = ⊥
rw :
  Eq (α := RingHom.{u, v} R (S ⧸ P))
    (RingHom.comp (algebraMap (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P))
      (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.quotientBot R))))
    ((RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.trans (quotEquivOfEq hP) (RingEquiv.quotientBot S)))).comp f)
⊢ finrank.{u, v} (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P) = finrank R S

Tactic:
rw [Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot R).symm
    ((quotEquivOfEq hP).trans (RingEquiv.quotientBot S)).symm]

Premises used: Ideal.quotEquivOfEq, Algebra.finrank_eq_of_equiv_equiv, RingEquiv.trans, RingEquiv.symm, RingEquiv.quotientBot
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hP_1 : LiesOver.{u, v} (A := R) P ⊥
hP : P = ⊥
⊢ Eq (α := RingHom.{u, v} R (S ⧸ P))
    (RingHom.comp (algebraMap (HasQuotient.Quotient R (B := Ideal R) ⊥) (S ⧸ P))
      (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.quotientBot R))))
    ((RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.trans (quotEquivOfEq hP) (RingEquiv.quotientBot S)))).comp f)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := LiesOver.trans Q P p
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this : Q.LiesOver p
rw : finrank.{v, u_2} (S ⧸ P) (T ⧸ Q) ≤ finrank.{u, u_2} (R ⧸ p) (T ⧸ Q)
⊢ P.inertiaDeg Q ≤ p.inertiaDeg Q

Tactic:
rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this : Q.LiesOver p
x_1 : R ⧸ p
x : R
⊢ Eq.{u_2 + 1} (α := T ⧸ Q)
    ((algebraMap (R ⧸ p) (T ⧸ Q) : (a : R ⧸ p) → T ⧸ Q) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x) : T ⧸ Q)
    ((algebraMap (S ⧸ P) (T ⧸ Q) : (a : S ⧸ P) → T ⧸ Q)
        ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x)) :
      T ⧸ Q)

Tactic:
simp [Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply R (S ⧸ P) (T ⧸ Q)]

Premises used: HasQuotient.Quotient, Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this : Q.LiesOver p
⊢ IsScalarTower.{u, v, u_2} (R ⧸ p) (S ⧸ P) (T ⧸ Q)

Tactic:
have : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ Q) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩
    simp [Submodule.Quotient.quot_mk_eq_mk, IsScalarTower.algebraMap_apply R (S ⧸ P) (T ⧸ Q)]
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this_1 : Q.LiesOver p
this : IsScalarTower.{u, v, u_2} (R ⧸ p) (S ⧸ P) (T ⧸ Q)
⊢ finrank.{v, u_2} (S ⧸ P) (T ⧸ Q) ≤ finrank.{u, u_2} (R ⧸ p) (T ⧸ Q)

Tactic:
finrank_top_le_finrank_of_isScalarTower ..

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Module.Finite R T
Q : Ideal T
inst_8 : P.LiesOver p
inst_9 : Q.LiesOver P
inst_10 : p.IsPrime
this_1 : Q.LiesOver p
this : IsScalarTower.{u, v, u_2} (R ⧸ p) (S ⧸ P) (T ⧸ Q)
⊢ finrank.{v, u_2} (S ⧸ P) (T ⧸ Q) ≤ finrank.{u, u_2} (R ⧸ p) (T ⧸ Q)

Tactic:
exact finrank_top_le_finrank_of_isScalarTower ..

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : IsDedekindDomain R
inst_5 : Free ℤ R
inst_6 : Algebra S R
inst_7 : Module.Finite S R
P : Ideal R
p : Ideal S
inst_8 : P.LiesOver p
hp : p.IsPrime
hp_ne_bot : p ≠ ⊥
⊢ p.IsMaximal

Tactic:
have : p.IsMaximal := hp.isMaximal hp_ne_bot
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
S : Type u_1
inst_1 : CommRing S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : IsDedekindDomain R
inst_5 : Free ℤ R
inst_6 : Algebra S R
inst_7 : Module.Finite S R
P : Ideal R
p : Ideal S
inst_8 : P.LiesOver p
hp : p.IsPrime
hp_ne_bot : p ≠ ⊥
this : p.IsMaximal
x : Field (S ⧸ p) := Quotient.field p
⊢ (absNorm : (a : Ideal R) → ℕ) P = HPow.hPow (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) p : ℕ) (p.inertiaDeg P)

Tactic:
simpa [absNorm_apply, Submodule.cardQuot_apply] using Module.natCard_eq_pow_finrank (K := S ⧸ p)

Premises used: Module.natCard_eq_pow_finrank, Ideal.absNorm_apply, Submodule.cardQuot_apply
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst_4 : P.LiesOver (A := ℤ) (span {p})
hp rwa rwa₁ rwa₂ rwa₃ : Prime p
⊢ IsPrime (α := ℤ) (span {p})

Tactic:
rwa [span_singleton_prime hp.ne_zero]

Premises used: Prime.ne_zero, Ideal.span_singleton_prime
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst_4 : P.LiesOver (A := ℤ) (span {p})
hp : Prime p
⊢ Ne (α := Ideal ℤ) (span {p}) ⊥

Tactic:
simpa using hp.ne_zero

Premises used: Prime.ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
p : ℤ
P : Ideal R
inst_4 : P.LiesOver (A := ℤ) (span {p})
hp : Prime p
⊢ (absNorm : (a : Ideal R) → ℕ) P = p.natAbs ^ inertiaDeg (R := ℤ) (span {p}) P

Tactic:
simpa using absNorm_eq_pow_inertiaDeg_of_liesOver P (span {p})
    (by rwa [span_singleton_prime hp.ne_zero]) (by simpa using hp.ne_zero)

Premises used: Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, Ideal.span, Singleton.singleton
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Free ℤ R
inst_3 : Module.Finite ℤ R
p : ℕ
P : Ideal R
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hp : Nat.Prime p
⊢ (absNorm : (a : Ideal R) → ℕ) P = p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P

Tactic:
absNorm_eq_pow_inertiaDeg P (Nat.prime_iff_prime_int.mp hp)

Premises used: Nat.prime_iff_prime_int, Int.natAbs, Iff.mp, Ideal.absNorm_eq_pow_inertiaDeg
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
⊢ p = under R P

Tactic:
have h₁ := P.over_def p
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
⊢ P = under S I

Tactic:
have h₂ := I.over_def P
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
⊢ p = under R I

Tactic:
have h₃ := (LiesOver.trans I P p).over
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
simp : finrank.{u_1, u_3} (R ⧸ p) (T ⧸ I) = finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) * finrank.{u_2, u_3} (S ⧸ P) (T ⧸ 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]

Premises used: Ideal.inertiaDeg, dif_pos, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this_1 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this_2 : Algebra.{u_2, u_3} (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra.{u_1, u_3} (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x_1 : R ⧸ p
x : R
⊢ Eq.{u_3 + 1} (α := T ⧸ I)
    ((algebraMap (R ⧸ p) (T ⧸ I) : (a : R ⧸ p) → T ⧸ I) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x) : T ⧸ I)
    ((algebraMap (S ⧸ P) (T ⧸ I) : (a : S ⧸ P) → T ⧸ I)
        ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x)) :
      T ⧸ I)

Tactic:
congr_arg _ (IsScalarTower.algebraMap_apply R S T x)

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, congr_arg, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this_1 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this_2 : Algebra.{u_2, u_3} (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : Algebra.{u_1, u_3} (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
x_1 : R ⧸ p
x : R
⊢ Eq.{u_3 + 1} (α := T ⧸ I)
    ((algebraMap (R ⧸ p) (T ⧸ I) : (a : R ⧸ p) → T ⧸ I) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x) : T ⧸ I)
    ((algebraMap (S ⧸ P) (T ⧸ I) : (a : S ⧸ P) → T ⧸ I)
        ((algebraMap (R ⧸ p) (S ⧸ P) : (a : R ⧸ p) → S ⧸ P) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) x)) :
      T ⧸ I)

Tactic:
exact congr_arg _ (IsScalarTower.algebraMap_apply R S T x)

Premises used: congr_arg, IsScalarTower.algebraMap_apply
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this_1 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this_2 : Algebra.{u_2, u_3} (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this_3 : Algebra.{u_1, u_3} (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : IsScalarTower.{u_1, u_2, u_3} (R ⧸ p) (S ⧸ P) (T ⧸ I) := ⋯
⊢ finrank.{u_1, u_3} (R ⧸ p) (T ⧸ I) = finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) * finrank.{u_2, u_3} (S ⧸ P) (T ⧸ I)

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

Premises used: HasQuotient.Quotient, Module.finrank_mul_finrank, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Inertia
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst_7 : p.IsMaximal
inst_8 : P.IsMaximal
inst_9 : P.LiesOver p
inst_10 : I.LiesOver P
h₁ : p = under R P
h₂ : P = under S I
h₃ : p = under R I
this_1 : Algebra.{u_1, u_2} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfLEComap ⋯
this_2 : Algebra.{u_2, u_3} (S ⧸ P) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this_3 : Algebra.{u_1, u_3} (R ⧸ p) (T ⧸ I) := Quotient.algebraQuotientOfLEComap ⋯
this : IsScalarTower.{u_1, u_2, u_3} (R ⧸ p) (S ⧸ P) (T ⧸ I) := ⋯
⊢ finrank.{u_1, u_3} (R ⧸ p) (T ⧸ I) = finrank.{u_1, u_2} (R ⧸ p) (S ⧸ P) * finrank.{u_2, u_3} (S ⧸ P) (T ⧸ I)

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

Premises used: HasQuotient.Quotient, Module.finrank_mul_finrank, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : DecidablePred fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
h : ∃ (n : ℕ), ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
⊢ (sSup fun (a : ℕ) ↦ ∀ ⦃x : S⦄, Membership.mem (γ := Submodule S S) (map (F := R →+* S) f p) x → x ∈ P ^ a) =
    Nat.find (p := fun (n : ℕ) ↦
      ∀ (a : ℕ),
        Membership.mem (γ := Set ℕ)
            (fun (a : ℕ) ↦ ∀ ⦃x : S⦄, Membership.mem (γ := Submodule S S) (map (F := R →+* S) f p) x → x ∈ P ^ a) a →
          a ≤ n)
      h

Tactic:
Nat.sSup_def h

Premises used: Nat.sSup_def
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
inst_3 : DecidablePred fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
h : ∃ (n : ℕ), ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx P = Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) h

Tactic:
convert! Nat.sSup_def h

Premises used: Nat.sSup_def
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
push : ∀ (n : ℕ), ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a ∧ n < a
⊢ ¬∃ (n : ℕ), ∀ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a → a ≤ n

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a ∧ n < a

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | map (F := R →+* S) f p ≤ P ^ n} a ∧ n < a

Tactic:
exact h
-- Module: Mathlib.NumberTheory.RamificationInertia.Ramification
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
n : ℕ
hle : map (F := R →+* S) f p ≤ P ^ n
hgt : ¬map (F := R →+* S) f p ≤ P ^ (n + 1)
Q : ℕ → Prop := fun (m : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ m
k : ℕ
hk : map (F := R →+* S) f p ≤ P ^ k
⊢ k ≤ n

Tactic:
le_of_not_gt fun hnk => ?_

Premises used: le_of_not_gt