awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₅ : p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₆ : p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔ p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₇ : p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₈ : p ≤
    comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f)
      (P ^ n) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₈ :
  p ≤
      comap (F := R →+* S₁)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₉ : p ≤ comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv : S →+* S₁) f) (P ^ n) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₈ :
  p ≤
      comap (F := R →+* S₁)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₉ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₁₀ : p ≤ comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) (P ^ n) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₈ :
  p ≤
      comap (F := R →+* S₁)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₉ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₀ :
  p ≤ comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₁₁ : p ≤
    comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑e : S →ₐ[R] S₁) : S →+* S₁) f)
      (P ^ n) ↔
  p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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₁
n : ℕ
e_a :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap (F := S →+* S₁) (↑e.toRingEquiv : S →+* S₁) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₂ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₃ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e.toRingEquiv.symm.symm P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₄ :
  p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₅ :
  p ≤ comap (F := R →+* S) f (map (F := S₁ →+* S) (↑e.toRingEquiv.symm : S₁ →+* S) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₆ :
  p ≤ comap (F := R →+* S) f (comap e.toRingEquiv.symm.symm (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₇ :
  p ≤ comap (F := R →+* S) f (comap (F := S →+* S₁) (↑e.toRingEquiv.symm.symm : S →+* S₁) (P ^ n)) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₈ :
  p ≤
      comap (F := R →+* S₁)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv.symm.symm : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₉ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.toRingEquiv : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₀ :
  p ≤ comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e : S →+* S₁) f) (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
e_a₁₁ :
  p ≤
      comap (F := R →+* S₁) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(↑e : S →ₐ[R] S₁) : S →+* S₁) f)
        (P ^ n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
⊢ p ≤ comap (F := R →+* S) f (HPow.hPow (α := Ideal S) (comap e P) n) ↔
    p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
have e_a₁₂ : p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n) ↔ p ≤ comap (F := R →+* S₁) (algebraMap R S₁) (P ^ n)
Tactic: rw [← comap_coe e, ← e.toRingEquiv_toRingHom, comap_coe, ← RingEquiv.symm_symm (e : S ≃+* S₁),
    ← map_comap_of_equiv, ← Ideal.map_pow, map_comap_of_equiv, ← comap_coe (RingEquiv.symm _),
    comap_comap, RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom,
    AlgHom.comp_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
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 : Type u_2
inst_5 : EquivLike E S S₁
inst_6 : AlgEquivClass E R S S₁
P : Ideal S
e : E
⊢ ramificationIdx.{u, u_1} (S := S₁) p (map e P) = p.ramificationIdx P
have rw : p.ramificationIdx (comap (F := S₁ ≃+* S) (RingEquiv.symm (↑e : S ≃+* S₁)) P) = p.ramificationIdx P
Tactic: rw [show P.map e = _ from P.map_comap_of_equiv (RingEquivClass.toRingEquiv e : S ≃+* S₁)]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have pos : ∀ (H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
  p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: by_cases! H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
pos :
  ∀ (H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k),
    p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have neg : ∀ (H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n),
  p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: by_cases! H : ∀ n : ℕ, ∃ k, p.map f ≤ P ^ k ∧ n < k
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∀ (n : ℕ), ∃ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k ∧ n < k
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have pos : ∀ (k : ℕ) (hk : map (F := R →+* S) f p ≤ P ^ k) (h2k : 2 < k),
  p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: obtain ⟨k, hk, h2k⟩ := H 2
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
⊢ p.ramificationIdx P ≠ 1 ↔ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have neg : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
  map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: rw [Ideal.ramificationIdx_eq_find H]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have neg : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 →
  map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
neg :
  Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 →
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
⊢ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1 ↔
    map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have neg₁ : map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2 →
  Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
Tactic: have : 1 ≤ Nat.find H := Nat.find_spec H 1 (by simpa)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (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
hp : map (F := R →+* S) f p ≤ P
H : ∃ (n : ℕ), ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n
he : Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ), map (F := R →+* S) f p ≤ P ^ k → k ≤ n) H ≠ 1
this : 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ n) H
⊢ map (F := R →+* S) f p ≤ HPow.hPow (β := ℕ) P 2
have this₁ : ¬∀ (k : ℕ) (_ : map (F := R →+* S) f p ≤ P ^ k), k ≤ 1
Tactic: have := Nat.find_min H (m := 1) (by lia)