awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
mp : emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
have mpr : (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d
Tactic: classical
  constructor
  · exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)
  · intro h
    unfold emultiplicity
    -- aesop? says
    split
    next h_1 =>
      obtain ⟨w, h_1⟩ := h_1
      split
      next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]
      next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]
    next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.coe_ne_top, imp_false, not_false_eq_true, implies_true]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
have rw : emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
Tactic: rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hab.emultiplicity_eq_multiplicity,
    ← hcd.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
F : Type u_3
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → HPow.hPow (α := β) ((f : (a : α) → β) a : β) n ∣ (f : (a : α) → β) b
have rw : a ^ n ∣ b → Dvd.dvd.{u_2} (α := β) ((f : (a : α) → β) (a ^ n) : β) ((f : (a : α) → β) b : β)
Tactic: rw [← map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℕ
⊢ FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b
have rw : (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
Tactic: rw [← not_iff_not, FiniteMultiplicity.not_iff_forall, not_and_or, not_ne_iff, not_lt,
    Nat.le_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
have h₁ : ∀ (n : ℕ), HPow.hPow (α := ℕ) 0 n ∣ b
Tactic: rw [ha] at h
Cleared hypotheses: h, hb, ha
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
have inl : a = 1 → ∀ (n : ℕ), a ^ n ∣ b
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℕ
h : a = 1 ∨ b = 0
inl : a = 1 → ∀ (n : ℕ), a ^ n ∣ b
⊢ ∀ (n : ℕ), a ^ n ∣ b
have inr : b = 0 → ∀ (n : ℕ), a ^ n ∣ b
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b
have by_contra! : ∀ (nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b), False
Tactic: by_contra! nh
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
nh : (∀ (n : ℕ), p ^ (n + 1) ∣ a) ∧ ∀ (n : ℕ), p ^ (n + 1) ∣ b
⊢ False
have obtain : ∀ (c : ℕ) (hc : ¬p ^ (c + 1) ∣ a + b), False
Tactic: obtain ⟨c, hc⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)
have top : ∀ (hm : min (emultiplicity p a) (emultiplicity p b) = ⊤), ⊤ ≤ emultiplicity p (a + b)
Tactic: cases hm : min (emultiplicity p a) (emultiplicity p b)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
top : ∀ (hm : min (emultiplicity p a) (emultiplicity p b) = ⊤), ⊤ ≤ emultiplicity p (a + b)
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)
have coe : ∀ (a_1 : ℕ) (hm : min (emultiplicity p a) (emultiplicity p b) = (↑a_1 : ℕ∞)), (↑a_1 : ℕ∞) ≤ emultiplicity p (a + b)
Tactic: cases hm : min (emultiplicity p a) (emultiplicity p b)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)
have top : ∀ (hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b), ¬FiniteMultiplicity p (a + b)
Tactic: simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ ¬FiniteMultiplicity p (a + b)
have top : ∀ (hm : FiniteMultiplicity p (a + b)), ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)
Tactic: contrapose hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)
have top : FiniteMultiplicity p a ∨ FiniteMultiplicity p b
Tactic: simp only [not_and_or, not_not] at hm ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Semiring α
p a b : α
a_1 : ℕ
hm : min (emultiplicity p a) (emultiplicity p b) = (↑a_1 : ℕ∞)
⊢ (↑a_1 : ℕ∞) ≤ emultiplicity p (a + b)
have coe : p ^ a_1 ∣ a + b
Tactic: apply le_emultiplicity_of_pow_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ (∃ (n : ℕ), ¬a ^ (n + 1) ∣ -b) ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b
have a₁ : ∀ (x : ℕ), a ^ (x + 1) ∣ -b ↔ a ^ (x + 1) ∣ b
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
a b : α
⊢ emultiplicity a (-b) = emultiplicity a b
have rw : ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b
Tactic: rw [emultiplicity_eq_emultiplicity_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
have inl : ∀ (h : b = (↑b.natAbs : ℤ)), emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
Tactic: rcases Int.natAbs_eq b with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
inl : ∀ (h : b = (↑b.natAbs : ℤ)), emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
have inr : ∀ (h : b = -(↑b.natAbs : ℤ)), emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
Tactic: rcases Int.natAbs_eq b with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
| emultiplicity (↑a : ℤ) b
have rw : emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
have inl : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
Tactic: conv_rhs => rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
| emultiplicity (↑a : ℤ) b
have rw : emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (↑a : ℤ) b
have inr : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
Tactic: conv_rhs => rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = (↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
have inl : emultiplicity a b.natAbs = emultiplicity a b.natAbs
Tactic: rw [Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
have inr : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
Tactic: rw [emultiplicity_neg, Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a : ℕ
b : ℤ
h : b = -(↑b.natAbs : ℤ)
inr : emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (↑b.natAbs : ℤ)
⊢ emultiplicity a b.natAbs = emultiplicity (α := ℤ) (↑a : ℤ) (-(↑b.natAbs : ℤ))
have inr₁ : emultiplicity a b.natAbs = emultiplicity a b.natAbs
Tactic: rw [emultiplicity_neg, Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p b
have this : FiniteMultiplicity p b
Tactic: have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p b
have rw : ∀ (h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a) (this : FiniteMultiplicity p b),
  emultiplicity p (a + b) = (↑(multiplicity p b) : ℕ∞)
Tactic: rw [this.emultiplicity_eq_multiplicity] at *
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = (↑(multiplicity p b) : ℕ∞)
have hk : p ^ multiplicity p b ∣ a + b
Tactic: apply emultiplicity_eq_of_dvd_of_not_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hk : p ^ multiplicity p b ∣ a + b
⊢ emultiplicity p (a + b) = (↑(multiplicity p b) : ℕ∞)
have hsucc : ¬p ^ (multiplicity p b + 1) ∣ a + b
Tactic: apply emultiplicity_eq_of_dvd_of_not_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a + b
have hk : p ^ multiplicity p b ∣ a
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hk : p ^ multiplicity p b ∣ a
⊢ p ^ multiplicity p b ∣ a + b
have hk₁ : p ^ multiplicity p b ∣ b
Tactic: apply dvd_add
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a
have hk : (↑(multiplicity p b) : ℕ∞) ≤ emultiplicity p a
Tactic: apply pow_dvd_of_le_emultiplicity
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b
have hsucc : ¬p ^ (multiplicity p b + 1) ∣ b
Tactic: rw [dvd_add_right]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
hsucc : ¬p ^ (multiplicity p b + 1) ∣ b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b
have hsucc₁ : p ^ (multiplicity p b + 1) ∣ a
Tactic: rw [dvd_add_right]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ b
have hsucc : multiplicity p b < multiplicity p b + 1
Tactic: apply this.not_pow_dvd_of_multiplicity_lt
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : (↑(multiplicity p b) : ℕ∞) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a
have hsucc : (↑(multiplicity p b + 1) : ℕ∞) ≤ emultiplicity p a
Tactic: apply pow_dvd_of_le_emultiplicity
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b
have rw : emultiplicity p (-b) = emultiplicity p b
Tactic: rw [sub_eq_add_neg, emultiplicity_add_of_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
rw : emultiplicity p (-b) = emultiplicity p b
⊢ emultiplicity p (a - b) = emultiplicity p b
have rw₁ : emultiplicity p (-b) < emultiplicity p a
Tactic: rw [sub_eq_add_neg, emultiplicity_add_of_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) = emultiplicity p b
have rw : emultiplicity p b = emultiplicity p b
Tactic: rw [emultiplicity_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (a - b) = multiplicity p b
have rw : multiplicity p (-b) = multiplicity p b
Tactic: rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
rw : multiplicity p (-b) = multiplicity p b
⊢ multiplicity p (a - b) = multiplicity p b
have rw₁ : multiplicity p (-b) < multiplicity p a
Tactic: rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (-b) = multiplicity p b
have rw : multiplicity p b = multiplicity p b
Tactic: rw [multiplicity_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
have inl : ∀ (hab : emultiplicity p a < emultiplicity p b), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Tactic: rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
inl :
  ∀ (hab : emultiplicity p a < emultiplicity p b), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
have inr : emultiplicity p a = emultiplicity p b → emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Tactic: rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
inl :
  ∀ (hab : emultiplicity p a < emultiplicity p b), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
inr : emultiplicity p a = emultiplicity p b → emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
have inr₁ : ∀ (hab : emultiplicity p b < emultiplicity p a), emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Tactic: rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
have inl : emultiplicity p a ≤ emultiplicity p b
Tactic: rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
have inr : emultiplicity p b ≤ emultiplicity p a
Tactic: rw [emultiplicity_add_of_gt hab, min_eq_right]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
have inl : ∀ (hab : multiplicity p a < multiplicity p b), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Tactic: rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
inl : ∀ (hab : multiplicity p a < multiplicity p b), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
have inr : multiplicity p a = multiplicity p b → multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Tactic: rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
inl : ∀ (hab : multiplicity p a < multiplicity p b), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
inr : multiplicity p a = multiplicity p b → multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
have inr₁ : ∀ (hab : multiplicity p b < multiplicity p a), multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Tactic: rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
have inl : multiplicity p a ≤ multiplicity p b
Tactic: rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
have inr : multiplicity p b ≤ multiplicity p a
Tactic: rw [hb.multiplicity_add_of_gt hab, min_eq_right]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
h_2 : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p
have hy₁ : x = p ^ n * y
Tactic: rw [tsub_add_cancel_of_le (succ_le_of_lt hn0)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this_1 : p ∣ a * b
h_1 : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p
have rw : x * b * p = p ^ (n + m) * s * p
Tactic: rw [tsub_add_eq_add_tsub (succ_le_of_lt hn0), tsub_add_cancel_of_le this]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
h_2 : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p
have hy₁ : x = p ^ m * y
Tactic: rw [tsub_add_cancel_of_le (succ_le_of_lt hm0)] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
h : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
h_1 : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p
have rw : a * x * p = p ^ (n + m) * s * p
Tactic: rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k_1 k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))
have rw : FiniteMultiplicity p (a * a ^ k)
Tactic: rw [_root_.pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
⊢ multiplicity a a = 1
have pos : ∀ (ha : FiniteMultiplicity a a), multiplicity a a = 1
Tactic: by_cases ha : FiniteMultiplicity a a
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
pos : ∀ (ha : FiniteMultiplicity a a), multiplicity a a = 1
⊢ multiplicity a a = 1
have neg : ∀ (ha : ¬FiniteMultiplicity a a), multiplicity a a = 1
Tactic: by_cases ha : FiniteMultiplicity a a
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1
have pos : HPow.hPow (β := ℕ) a 1 ∣ a ∧ ¬a ^ HAdd.hAdd (α := ℕ) 1 1 ∣ a
Tactic: rw [ha.multiplicity_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ HPow.hPow (β := ℕ) a 1 ∣ a ∧ ¬a ^ HAdd.hAdd (α := ℕ) 1 1 ∣ a
have pos : ¬HPow.hPow (β := ℕ) a 2 ∣ a
Tactic: simp only [pow_one, dvd_refl, reduceAdd, true_and]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a = HPow.hPow (β := ℕ) a 2 * v
⊢ False
have hv₁ : a * 1 = HPow.hPow (β := ℕ) a 2 * v
Tactic: nth_rw 1 [← mul_one a] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = HPow.hPow (β := ℕ) a 2 * v
⊢ False
have hv₁ : 1 = a * v ∨ a = 0
Tactic: simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
⊢ False
have pos : ∀ (hv : 1 = a * v), False
Tactic: obtain hv | rfl := hv
Cleared hypotheses: hv