-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_le_emultiplicity_iff {c d : β} :
    emultiplicity a b ≤ emultiplicity c d ↔ ∀ n : ℕ, a ^ n ∣ b → c ^ n ∣ d

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ emultiplicity a b ≤ emultiplicity c d

Tactic:
unfold emultiplicity

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h_2)

Tactic:
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]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : FiniteMultiplicity a b
⊢ ↑(Nat.find h_1) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
obtain ⟨w, h_1⟩ := h_1

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
⊢ ↑(Nat.find ⋯) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Proof state:
case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
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]

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
exact fun h n hab ↦ pow_dvd_of_le_emultiplicity (le_trans (le_emultiplicity_of_pow_dvd hab) h)

Result:
no goals

Proof state:
case mpr.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : FiniteMultiplicity a b
⊢ ↑(Nat.find h✝) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
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]

Result:
case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
split

Result:
case mpr.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : FiniteMultiplicity a b
⊢ ↑(Nat.find h✝) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h_1 : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
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]

Result:
no goals

Proof state:
case intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Tactic:
intro h

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ emultiplicity a b ≤ emultiplicity c d

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d → ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) → emultiplicity a b ≤ emultiplicity c d

Proof state:
case intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h✝)

case intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
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]

Result:
case intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
⊢ ↑(Nat.find ⋯) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
split

Result:
case intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h✝)

case intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
simp_all only [not_exists, Decidable.not_not, le_top]

Result:
no goals