awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
⊢ Function.Injective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)

Tactic:
exact quotientToQuotientRangePowQuotSucc_injective p P hi a_mem a_notMem

Premises used: Ideal.quotientToQuotientRangePowQuotSucc_injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
⊢ Function.Surjective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)

Tactic:
quotientToQuotientRangePowQuotSucc_surjective p P hP hi a_mem a_notMem

Premises used: Ideal.quotientToQuotientRangePowQuotSucc_surjective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : i < e
a : S
a_mem : Membership.mem (γ := Ideal S) ((fun (x : ℕ) ↦ P ^ x) i) a
a_notMem : a ∉ (fun (x : ℕ) ↦ P ^ x) i.succ
⊢ Function.Surjective (α := S ⧸ P) (β :=
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
    (⇑(p.quotientToQuotientRangePowQuotSucc P a_mem) :
      (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)

Tactic:
exact quotientToQuotientRangePowQuotSucc_surjective p P hP hi a_mem a_notMem

Premises used: Ideal.quotientToQuotientRangePowQuotSucc_surjective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
rw :
  Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank.{u, v} (R ⧸ p)
        (HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i))) +
      Module.rank.{u, v} (R ⧸ p) ↥(LinearMap.range (p.powQuotSuccInclusion P i))
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank.{u, v} (R ⧸ p) (S ⧸ P) +
      Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))

Tactic:
rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective p P i),
    (quotientRangePowQuotSuccInclusionEquiv p P hP0 hi).symm.rank_eq]

Premises used: LinearEquiv.symm, Ideal.quotientRangePowQuotSuccInclusionEquiv, LinearEquiv.rank_eq, Ideal.powQuotSuccInclusion_injective, rank_range_of_injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank.{u, v} (R ⧸ p)
        (HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i))) +
      Module.rank.{u, v} (R ⧸ p) ↥(LinearMap.range (p.powQuotSuccInclusion P i))

Tactic:
(Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion p P i))).symm

Premises used: Set.Mem, Submodule.rank_quotient_add_rank, LinearMap.range, Ideal.powQuotSuccInclusion, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank.{u, v} (R ⧸ p)
        (HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i))) +
      Module.rank.{u, v} (R ⧸ p) ↥(LinearMap.range (p.powQuotSuccInclusion P i))

Tactic:
exact (Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion p P i))).symm

Premises used: Submodule.rank_quotient_add_rank, LinearMap.range, Ideal.powQuotSuccInclusion, Eq.symm
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
Nat.decreasingInduction' (P := Q) (fun j lt_e _le_j ih => ?_) hi ?_

Premises used: Nat.decreasingInduction'
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
refine_1 : ∀ (j : ℕ) (lt_e : j < e) (_le_j : i ≤ j) (ih : Q (j + 1)), Q j
refine_2 : Q e
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
    (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
refine Nat.decreasingInduction' (P := Q) (fun j lt_e _le_j ih => ?_) hi ?_

Premises used: Nat.decreasingInduction'
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
refine_1 :
  Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ j)) =
    (e - j) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Q j

Tactic:
dsimp only [Q]
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
rw : P ≠ ⊥
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ j)) =
    (e - j) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
rw [rank_pow_quot_aux p P _ lt_e, ih, ← succ_nsmul', Nat.sub_succ, ← Nat.succ_eq_add_one,
      Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt lt_e)]

Premises used: Nat.succ_eq_add_one, Nat.succ_pred_eq_of_pos, Nat.sub_pos_of_lt, Nat.sub_succ, Ideal.rank_pow_quot_aux, succ_nsmul'
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥

Tactic:
assumption
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
refine_2 :
  Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ e)) =
    (e - e) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Q e

Tactic:
dsimp only [Q]
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
refine_2 : Module.rank.{u, v} (R ⧸ p) ↥⊥ = 0
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ e)) =
    (e - e) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
rw [Nat.sub_self, zero_nsmul, map_quotient_self]

Premises used: Ideal.map_quotient_self, Nat.sub_self, zero_nsmul
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Module.rank.{u, v} (R ⧸ p) ↥⊥ = 0

Tactic:
rank_bot (R ⧸ p) (S ⧸ P ^ e)

Premises used: rank_bot, Set.Mem, AddOpposite, HasQuotient.Quotient, HPow.hPow, Quotient, Submodule.quotientRel, AddAction.orbitRel, Ideal.ramificationIdx
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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
hfp : NeZero e
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop :=
  fun (i : ℕ) ↦
    Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) =
      (e - i) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Module.rank.{u, v} (R ⧸ p) ↥⊥ = 0

Tactic:
exact rank_bot (R ⧸ p) (S ⧸ P ^ e)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this : NeZero e := ⋯
⊢ Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (HPow.hPow (β := ℕ) P 0)) =
    (e - 0) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
have := rank_pow_quot p P hP0 0 (Nat.zero_le e)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this_1 : NeZero e := ⋯
this :
  Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (HPow.hPow (β := ℕ) P 0)) =
    (e - 0) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Module.rank.{u, v} (R ⧸ p) ↥⊤ = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
rw [pow_zero, Nat.sub_zero, Ideal.one_eq_top, Ideal.map_top] at this

Premises used: Ideal.one_eq_top, pow_zero, Nat.sub_zero, Ideal.map_top
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Module.rank.{u, v} (R ⧸ p) ↥⊤ = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
exact (rank_top (R ⧸ p) _).symm.trans this

Premises used: HasQuotient.Quotient, rank_top, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
⊢ Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
have hdim := rank_prime_pow_ramificationIdx _ _ hP0 he
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
pos :
  ∀ (hP : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)),
    finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
neg :
  ∀ (hP : ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)),
    finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)

Premises used: HasQuotient.Quotient, FiniteDimensional
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)
⊢ FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)

Tactic:
have := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this_2 : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)
this : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)
pos :
  Eq.{v + 2} (α := Cardinal.{v}) (↑(finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e)) : Cardinal.{v})
    (↑(e * finrank.{u, v} (R ⧸ p) (S ⧸ P)) : Cardinal.{v})
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
apply @Nat.cast_injective Cardinal

Premises used: Nat.cast_injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this_2 : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)
this : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)
pos : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = (↑(e * finrank.{u, v} (R ⧸ p) (S ⧸ P)) : Cardinal.{v})
pos₁ :
  Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) =
    HMul.hMul (α := Cardinal.{v}) (↑e : Cardinal.{v}) (↑(finrank.{u, v} (R ⧸ p) (S ⧸ P)) : Cardinal.{v})
pos₂ : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
pos₃ : e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
pos₄ pos₅ :
  (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
⊢ Eq.{v + 2} (α := Cardinal.{v}) (↑(finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e)) : Cardinal.{v})
    (↑(e * finrank.{u, v} (R ⧸ p) (S ⧸ P)) : Cardinal.{v})

Tactic:
rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]

Premises used: Nat.cast_mul, Module.finrank_eq_rank', nsmul_eq_mul
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)
⊢ ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)

Tactic:
have hPe := mt (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mp hP
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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 : IsDedekindDomain S
hP0 : P ≠ ⊥
inst_4 : p.IsMaximal
inst_5 : P.IsPrime
he : e ≠ 0
this_1 : NeZero e := ⋯
this : Algebra.{u, v} (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)

Tactic:
simp only [finrank_of_infinite_dimensional hP, finrank_of_infinite_dimensional hPe,
    mul_zero]

Premises used: MulZeroClass.mul_zero, Module.finrank_of_infinite_dimensional
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S) ≠ ⊥

Tactic:
(prime_of_factor _ (Multiset.mem_toFinset.mp P.2)).ne_zero

Premises used: UniqueFactorizationMonoid.prime_of_factor, Prime.ne_zero, Iff.mp, Multiset.mem_toFinset, Subtype.property
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S).IsPrime

Tactic:
Ideal.isPrime_of_prime (prime_of_factor _ (Multiset.mem_toFinset.mp P.2))

Premises used: UniqueFactorizationMonoid.prime_of_factor, Iff.mp, Ideal.isPrime_of_prime, Multiset.mem_toFinset, Subtype.property
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ p.ramificationIdx (↑P : Ideal S) ≠ 0

Tactic:
IsDedekindDomain.ramificationIdx_ne_zero (ne_zero_of_mem_factors (Multiset.mem_toFinset.mp P.2))
    (Factors.isPrime p P) (Ideal.le_of_dvd (dvd_of_mem_factors (Multiset.mem_toFinset.mp P.2)))

Premises used: Ideal.le_of_dvd, UniqueFactorizationMonoid.ne_zero_of_mem_factors, Ideal.IsDedekindDomain.ramificationIdx_ne_zero, Iff.mp, Ideal.Factors.isPrime, UniqueFactorizationMonoid.dvd_of_mem_factors, Multiset.mem_toFinset, Subtype.property
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ NeZero (p.ramificationIdx (↑P : Ideal S))

Tactic:
⟨Factors.ramificationIdx_ne_zero p P⟩

Premises used: NeZero.mk, Ideal.Factors.ramificationIdx_ne_zero
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ IsScalarTower.{u, u, v} R (R ⧸ p) (S ⧸ (↑P : Ideal S))

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S).LiesOver p

Tactic:
⟨(comap_eq_of_scalar_tower_quotient (algebraMap (R ⧸ p) (S ⧸ P.1)).injective).symm⟩

Premises used: Algebra.algebraMap, Ideal.LiesOver.mk, RingHom.injective, HasQuotient.Quotient, Eq.symm, Subtype.val, Ideal.comap_eq_of_scalar_tower_quotient
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
hP0 : (↑P : Ideal S) ≠ ⊥
he : p.ramificationIdx (↑P : Ideal S) ≠ 0
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) =
    p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S)

Tactic:
rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]

Premises used: Ideal.inertiaDeg_algebraMap, Ideal.finrank_prime_pow_ramificationIdx
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S) ≠ ⊥

Tactic:
Factors.ne_bot p P

Premises used: Ideal.Factors.ne_bot
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : IsDedekindDomain S
inst_4 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ p.ramificationIdx (↑P : Ideal S) ≠ 0

Tactic:
NeZero.ne _

Premises used: NeZero.ne