awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
refine_1 :
  LinearMap.{u, u, v, v} (R := R ⧸ p) (RingHom.id (R ⧸ p)) (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)))
refine_2 :
  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)
⊢ 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)) ≃ₗ[R ⧸ p]
    S ⧸ P
have refine_3 : 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: refine (LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩).symm
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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) (S ⧸ P) +
      Module.rank.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
have 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))
Tactic: rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective p P i),
    (quotientRangePowQuotSuccInclusionEquiv p P hP0 hi).symm.rank_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
have refine_1 : ∀ (j : ℕ) (lt_e : j < e) (_le_j : i ≤ j) (ih : Q (j + 1)), Q j
Tactic: refine Nat.decreasingInduction' (P := Q) (fun j lt_e _le_j ih => ?_) hi ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
⊢ 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)
have refine_2 : Q e
Tactic: refine Nat.decreasingInduction' (P := Q) (fun j lt_e _le_j ih => ?_) hi ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 ^ e)) =
    (e - e) • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
have refine_2 : Module.rank.{u, v} (R ⧸ p) ↥⊥ = 0
Tactic: rw [Nat.sub_self, zero_nsmul, map_quotient_self]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
have 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)
Tactic: have := rank_pow_quot p P hP0 0 (Nat.zero_le e)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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) (S ⧸ P ^ e) = e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have hdim : 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
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have 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)
Tactic: by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have 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)
Tactic: by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have this₁ : FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)
Tactic: have := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have 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})
Tactic: apply @Nat.cast_injective Cardinal
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ 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})
have pos : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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})
⊢ 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})
have 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})
Tactic: rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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})
⊢ 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})
have pos₂ : Module.rank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
Tactic: rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ 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})
have pos₃ : e • Module.rank.{u, v} (R ⧸ p) (S ⧸ P) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
Tactic: rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ 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})
have pos₄ : (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P) = (↑e : Cardinal.{v}) * Module.rank.{u, v} (R ⧸ p) (S ⧸ P)
Tactic: rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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)
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ P ^ e) = e * finrank.{u, v} (R ⧸ p) (S ⧸ P)
have hPe : ¬FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ P ^ e)
Tactic: have hPe := mt (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mp hP
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)))
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) =
    p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S)
have hP0 : (↑P : Ideal S) ≠ ⊥
Tactic: rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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) ≠ ⊥
⊢ finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)) =
    p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S)
have he : p.ramificationIdx (↑P : Ideal S) ≠ 0
Tactic: rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ FiniteDimensional.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
have refine : 0 < finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
Tactic: refine .of_finrank_pos ?_
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 : Module.Finite R S
inst_5 : p.IsMaximal
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ 0 < finrank.{u, v} (R ⧸ p) (S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
have rw : p.ramificationIdx (↑P : Ideal S) * p.inertiaDeg (↑P : Ideal S) ≠ 0
Tactic: rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
P_1 : Ideal S
inst_3 : IsDedekindDomain S
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))
⊢ (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p)) =
    (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S)
have rw : (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p)) =
  (↑P : Ideal S) ^ Multiset.count (↑P : Ideal S) (factors (map (F := R →+* S) f p))
Tactic: rw [IsDedekindDomain.ramificationIdx_eq_factors_count hp (Factors.isPrime p P)
            (Factors.ne_bot p P)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p_1 : Ideal R
P : Ideal S
inst_3 : IsDedekindDomain S
p : Ideal R
hp : Ne.{v + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
m : R ⧸ p
c : R
x_1 : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)
x : S
⊢ Equiv.toFun
      (RingEquiv.toEquiv
        (piQuotientEquiv p hp :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
            ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
              S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
      (HSMul.hSMul (α := R ⧸ p) (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c)
        (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x)) =
    HSMul.hSMul (α := R ⧸ p) (β :=
      (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c) : R ⧸ p)
      (Equiv.toFun
          (RingEquiv.toEquiv
            (piQuotientEquiv p hp :
              HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
                ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                  S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
          (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x) :
        (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
          S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
have mk : ∀ (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))),
  Equiv.toFun
      (RingEquiv.toEquiv
        (piQuotientEquiv p hp :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
            ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
              S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
      (HSMul.hSMul (α := R ⧸ p) (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c)
        (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x))
      P =
    HSMul.hSMul (α := R ⧸ p) (β :=
      (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
        S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      ((RingHom.id (R ⧸ p) : (a : R ⧸ p) → R ⧸ p) (Quot.mk (⇑(Submodule.quotientRel p) : R → R → Prop) c) : R ⧸ p)
      (Equiv.toFun
          (RingEquiv.toEquiv
            (piQuotientEquiv p hp :
              HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p) ≃+*
                ((P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
                  S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))))
          (Quot.mk (⇑(Submodule.quotientRel (map f p)) : S → S → Prop) x) :
        (P : ↥(Multiset.toFinset (factors (map (F := R →+* S) f p)))) →
          S ⧸ (↑P : Ideal S) ^ p.ramificationIdx (↑P : Ideal S))
      P
Tactic: ext P