awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i_1 : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
i : ι
hf :
  HSMul.hSMul (β := (↑Y : Type (max u v))) r
      ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → (↑Y : Type (max u v)))
      ((algebraMap R₀ (Matrix ι ι R) : (a : R₀) → Matrix ι ι R) r : Matrix ι ι R)
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i
⊢ HSMul.hSMul (β := (↑Y : Type (max u v))) r
      ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i

Tactic:
change _ = ((algebraMap R₀ (Matrix ι ι R) r) • ((ModuleCat.Hom.hom f).mapMatrixModule ι v)) i

Premises used: Algebra.algebraMap, Matrix, LinearMap.mapMatrixModule, HSMul.hSMul, ModuleCat.Hom.hom, DFunLike.coe
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i_1 : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
i : ι
⊢ HSMul.hSMul (β := (↑Y : Type (max u v))) r
      ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → (↑Y : Type (max u v)))
      ((algebraMap R₀ (Matrix ι ι R) : (a : R₀) → Matrix ι ι R) r : Matrix ι ι R)
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i

Tactic:
simp [Matrix.algebraMap_matrix_apply]

Premises used: Matrix.algebraMap_matrix_apply
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Nonempty ι
⊢ IsMoritaEquivalent R₀ R (Matrix ι ι R)

Tactic:
⟨Nonempty.map (moritaEquivalenceMatrix R R₀) inferInstance⟩

Premises used: moritaEquivalenceMatrix, inferInstance, IsMoritaEquivalent.mk, Nonempty.map
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b

Tactic:
simp [emultiplicity]

Premises used: emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ emultiplicity a b < ⊤ ↔ FiniteMultiplicity a b

Tactic:
simp [lt_top_iff_ne_top, emultiplicity_eq_top]

Premises used: emultiplicity_eq_top, lt_top_iff_ne_top
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
by_contra : ∀ (nh : ¬FiniteMultiplicity a b), False
⊢ FiniteMultiplicity a b

Tactic:
by_contra nh
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
nh : ¬FiniteMultiplicity a b
⊢ Eq (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
rw [← emultiplicity_eq_top, h] at nh

Premises used: emultiplicity_eq_top
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
nh : Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ False

Tactic:
trivial
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
simp : WithTop.untopD 1 (↑n : ℕ∞) = n
⊢ multiplicity a b = n

Tactic:
simp [multiplicity, h]

Premises used: multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
⊢ WithTop.untopD 1 (↑n : ℕ∞) = n

Tactic:
rfl
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
⊢ multiplicity a b ≠ n → emultiplicity a b ≠ (↑n : ℕ∞)

Tactic:
mt multiplicity_eq_of_emultiplicity_eq_some

Premises used: mt, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
top : ∀ (hm : emultiplicity a b = ⊤), Eq (α := ℕ∞) ⊤ (↑(multiplicity a b) : ℕ∞)
coe : ∀ (a_1 : ℕ) (hm : emultiplicity a b = (↑a_1 : ℕ∞)), Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑(multiplicity a b) : ℕ∞)
⊢ emultiplicity a b = (↑(multiplicity a b) : ℕ∞)

Tactic:
cases hm : emultiplicity a b

Premises used: emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
hm : emultiplicity a b = ⊤
⊢ Eq (α := ℕ∞) ⊤ (↑(multiplicity a b) : ℕ∞)

Tactic:
simp [h] at hm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
a_1 : ℕ
hm : emultiplicity a b = (↑a_1 : ℕ∞)
coe coe₁ : Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑a_1 : ℕ∞)
⊢ Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑(multiplicity a b) : ℕ∞)

Tactic:
rw [multiplicity_eq_of_emultiplicity_eq_some hm]

Premises used: multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
⊢ emultiplicity a b = (↑n : ℕ∞) ↔ multiplicity a b = n

Tactic:
simp [h.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
mp : emultiplicity a b = (↑n : ℕ∞) → multiplicity a b = n
mpr : multiplicity a b = n → emultiplicity a b = (↑n : ℕ∞)
⊢ emultiplicity a b = (↑n : ℕ∞) ↔ multiplicity a b = n

Tactic:
constructor
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = (↑n : ℕ∞) → multiplicity a b = n

Tactic:
multiplicity_eq_of_emultiplicity_eq_some

Premises used: multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = (↑n : ℕ∞) → multiplicity a b = n

Tactic:
exact multiplicity_eq_of_emultiplicity_eq_some

Premises used: multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
h₂ : multiplicity a b = n
⊢ emultiplicity a b = (↑n : ℕ∞)

Tactic:
simpa [multiplicity, WithTop.untopD_eq_iff, h] using h₂

Premises used: multiplicity, WithTop.untopD_eq_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ emultiplicity a b = 0 ↔ multiplicity a b = 0

Tactic:
emultiplicity_eq_iff_multiplicity_eq_of_ne_one zero_ne_one

Premises used: zero_ne_one, WithTop.some, emultiplicity_eq_iff_multiplicity_eq_of_ne_one
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
simp [multiplicity, emultiplicity_eq_top.2 h]

Premises used: Iff.mpr, emultiplicity_eq_top, multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
pos : ∀ (hf : FiniteMultiplicity a b), (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
neg : ∀ (hf : ¬FiniteMultiplicity a b), (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
⊢ (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b

Tactic:
by_cases hf : FiniteMultiplicity a b

Premises used: FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b

Tactic:
simp [hf.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b

Tactic:
simp [hf, emultiplicity_eq_top.2]

Premises used: Iff.mpr, emultiplicity_eq_top
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
rw rw₁ : WithTop.untopD 1 (emultiplicity c d) = WithTop.untopD 1 (emultiplicity c d)
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b ≤ (↑n : ℕ∞)
⊢ multiplicity a b ≤ n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans h

Premises used: LE.le.trans, multiplicity_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
rw : LE.le (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)
⊢ emultiplicity a b ≤ (↑n : ℕ∞)

Tactic:
rw [emultiplicity_eq_multiplicity hfin]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : multiplicity a b ≤ n
⊢ LE.le (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)

Tactic:
assumption_mod_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≤ multiplicity a b
⊢ (↑n : ℕ∞) ≤ emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

Premises used: WithTop.coe_mono, LE.le.trans, multiplicity_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : (↑n : ℕ∞) ≤ emultiplicity a b
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (h : n ≤ multiplicity a b), n ≤ multiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
assumption_mod_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b < (↑n : ℕ∞)
⊢ multiplicity a b < n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

Premises used: LE.le.trans_lt, multiplicity_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
rw : LT.lt (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)
⊢ emultiplicity a b < (↑n : ℕ∞)

Tactic:
rw [emultiplicity_eq_multiplicity hfin]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : multiplicity a b < n
⊢ LT.lt (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)

Tactic:
assumption_mod_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n < multiplicity a b
⊢ (↑n : ℕ∞) < emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

Premises used: LT.lt.trans_le, WithTop.coe_strictMono, multiplicity_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : (↑n : ℕ∞) < emultiplicity a b
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (h : n < multiplicity a b), n < multiplicity a b
⊢ n < multiplicity a b

Tactic:
assumption_mod_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ 0 < multiplicity a b

Tactic:
simp [pos_iff_ne_zero, pos_iff_ne_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero]

Premises used: emultiplicity_eq_zero_iff_multiplicity_eq_zero, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ FiniteMultiplicity a b ↔ ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a : α
⊢ FiniteMultiplicity a 1 → ¬a ∣ 1

Tactic:
fun ⟨n, hn⟩ ⟨d, hd⟩ => hn ⟨d ^ (n + 1), (pow_mul_pow_eq_one (n + 1) hd.symm).symm⟩

Premises used: False, HPow.hPow, HAdd.hAdd, _private.0.FiniteMultiplicity.not_dvd_of_one_right.match_1, Exists.intro, pow_mul_pow_eq_one, OfNat.ofNat, Eq.symm, Not, _private.0.FiniteMultiplicity.not_dvd_of_one_right.match_2
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h₂ :
  (∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
      (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v) →
    (∃ (n : ℕ), ¬a ^ (n + 1) ∣ b) → ∀ (x : ℕ), HPow.hPow (α := ℤ) (↑a : ℤ) (x + 1) ∣ (↑b : ℤ) ↔ a ^ (x + 1) ∣ b
h₁ : ∀ (x : ℕ), HPow.hPow (α := ℤ) (↑a : ℤ) (x + 1) ∣ (↑b : ℤ) ↔ a ^ (x + 1) ∣ b
⊢ Eq (α := ℕ∞)
    (if h : ∃ (n : ℕ), ¬HPow.hPow (α := ℤ) (↑a : ℤ) (n + 1) ∣ (↑b : ℤ) then
      (↑(Nat.find (p := fun (n : ℕ) ↦ ¬HPow.hPow (α := ℤ) (↑a : ℤ) (n + 1) ∣ (↑b : ℤ)) h) : ℕ∞)
    else ⊤)
    (if h : ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) else ⊤)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
h_congr_thm :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v
h : ∃ (n : ℕ), ¬a ^ (n + 1) ∣ b
x : ℕ
h₂ h₃ h₄ h₅ : a ^ (x + 1) ∣ b ↔ a ^ (x + 1) ∣ b
⊢ HPow.hPow (α := ℤ) (↑a : ℤ) (x + 1) ∣ (↑b : ℤ) ↔ a ^ (x + 1) ∣ b

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b x : ℕ
h₁ h₂ h₃ h₄ : a ^ (x + 1) ∣ b ↔ a ^ (x + 1) ∣ b
⊢ HPow.hPow (α := ℤ) (↑a : ℤ) (x + 1) ∣ (↑b : ℤ) ↔ a ^ (x + 1) ∣ b

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℕ
⊢ multiplicity (α := ℤ) (↑a : ℤ) (↑b : ℤ) = multiplicity a b

Tactic:
multiplicity_eq_of_emultiplicity_eq (natCast_emultiplicity a b)

Premises used: multiplicity_eq_of_emultiplicity_eq, Int.natCast_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
rw : 1 ∣ b
⊢ a ^ zero ∣ b

Tactic:
rw [_root_.pow_zero]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b

Tactic:
one_dvd _

Premises used: one_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b

Tactic:
exact one_dvd _

Premises used: one_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ n.succ ∣ b

Tactic:
simpa [FiniteMultiplicity] using h

Premises used: FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
simp : (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ¬FiniteMultiplicity a b

Tactic:
simp [FiniteMultiplicity]

Premises used: FiniteMultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b

Tactic:
tauto
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ ¬IsUnit a

Tactic:
let ⟨n, hn⟩ := h
  hn ∘ IsUnit.dvd ∘ IsUnit.pow (n + 1)

Premises used: IsUnit, Function.comp, IsUnit.pow, IsUnit.dvd, HAdd.hAdd, _private.0.FiniteMultiplicity.not_unit.match_1, OfNat.ofNat, Not
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b c : α
⊢ FiniteMultiplicity a (b * c) → FiniteMultiplicity a b

Tactic:
fun ⟨n, hn⟩ =>
  ⟨n, fun h => hn (h.trans (dvd_mul_right _ _))⟩

Premises used: _private.0.FiniteMultiplicity.mul_left.match_1, FiniteMultiplicity, Exists.intro, dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : (↑k : ℕ∞) ≤ emultiplicity a b
zero : ∀ (hk : (↑0 : ℕ∞) ≤ emultiplicity a b), HPow.hPow (β := ℕ) a 0 ∣ b
succ : ∀ (n : ℕ) (hk : (↑(n + 1) : ℕ∞) ≤ emultiplicity a b), a ^ (n + 1) ∣ b
⊢ a ^ k ∣ b

Tactic:
cases k
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hk : (↑0 : ℕ∞) ≤ emultiplicity a b
⊢ HPow.hPow (β := ℕ) a 0 ∣ b

Tactic:
simp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
hk :
  LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
    (if h : FiniteMultiplicity a b then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) else ⊤)
succ :
  ∀ (h : FiniteMultiplicity a b)
    (hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞)), a ^ (n + 1) ∣ b
succ₁ : ¬FiniteMultiplicity a b → ∀ (hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤), a ^ (n + 1) ∣ b
⊢ a ^ (n + 1) ∣ b

Tactic:
split at hk
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞)
⊢ n + 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h

Tactic:
norm_cast at hk
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
hk : n + 1 ≤ Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h
⊢ a ^ (n + 1) ∣ b

Tactic:
simpa using (Nat.find_min _ (lt_of_succ_le hk))

Premises used: Nat.lt_of_succ_le, Nat.find_min
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : ¬FiniteMultiplicity a b
hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤
⊢ a ^ (n + 1) ∣ b

Tactic:
apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Premises used: FiniteMultiplicity.not_iff_forall, Iff.mp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : (↑k : ℕ∞) ≤ emultiplicity a b
zero : ∀ (hk : (↑0 : ℕ∞) ≤ emultiplicity a b), HPow.hPow (β := ℕ) a 0 ∣ b
succ succ₁ : ∀ (n : ℕ) (hk : (↑(n + 1) : ℕ∞) ≤ emultiplicity a b), a ^ (n + 1) ∣ b
succ₂ :
  ∀ (n : ℕ)
    (hk :
      LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞)
        (if h : FiniteMultiplicity a b then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) else ⊤)),
    a ^ (n + 1) ∣ b
succ₃ :
  ∀ (n : ℕ) (h : FiniteMultiplicity a b)
    (hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞)), a ^ (n + 1) ∣ b
succ₄ succ₅ : ∀ (n : ℕ), ¬FiniteMultiplicity a b → ∀ (hk : LE.le (α := ℕ∞) (↑(n + 1) : ℕ∞) ⊤), a ^ (n + 1) ∣ b
⊢ a ^ k ∣ b

Tactic:
classical
  cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Premises used: FiniteMultiplicity.not_iff_forall, Iff.mp, emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
k : ℕ
hk : k ≤ multiplicity a b
⊢ a ^ k ∣ b

Tactic:
pow_dvd_of_le_emultiplicity (le_emultiplicity_of_le_multiplicity hk)

Premises used: le_emultiplicity_of_le_multiplicity, pow_dvd_of_le_emultiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ a ^ multiplicity a b ∣ b

Tactic:
pow_dvd_of_le_multiplicity le_rfl

Premises used: le_rfl, pow_dvd_of_le_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
hm :
  LT.lt (α := ℕ∞) (if h : FiniteMultiplicity a b then (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) else ⊤)
    (↑m : ℕ∞)
nh : a ^ m ∣ b
isTrue :
  ∀ (h : FiniteMultiplicity a b)
    (hm : LT.lt (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) (↑m : ℕ∞)), False
isFalse : ¬FiniteMultiplicity a b → ∀ (hm : LT.lt (α := ℕ∞) ⊤ (↑m : ℕ∞)), False
⊢ False

Tactic:
split at hm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h : FiniteMultiplicity a b
hm : LT.lt (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ ¬a ^ (n + 1) ∣ b) h) : ℕ∞) (↑m : ℕ∞)
⊢ ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b

Tactic:
simp only [cast_lt, find_lt_iff] at hm

Premises used: Nat.find_lt_iff, Nat.cast_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h : FiniteMultiplicity a b
hm : ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b
isTrue : ∀ (n : ℕ) (hn1 : n < m) (hn2 : ¬a ^ (n + 1) ∣ b), False
⊢ False

Tactic:
obtain ⟨n, hn1, hn2⟩ := hm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False

Tactic:
hn2 ((pow_dvd_pow _ hn1).trans nh)

Premises used: pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False

Tactic:
exact hn2 ((pow_dvd_pow _ hn1).trans nh)

Premises used: pow_dvd_pow, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h : ¬FiniteMultiplicity a b
hm : LT.lt (α := ℕ∞) ⊤ (↑m : ℕ∞)
⊢ False

Tactic:
simp at hm
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
hm₁ : emultiplicity a b < (↑m : ℕ∞)
⊢ ¬a ^ m ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt

Premises used: not_pow_dvd_of_emultiplicity_lt
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
hm₁ : LT.lt (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑m : ℕ∞)
⊢ emultiplicity a b < (↑m : ℕ∞)

Tactic:
rw [hf.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm hm₁ hm₂ hm₃ hm₄ : multiplicity a b < m
⊢ LT.lt (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑m : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
⊢ 0 < multiplicity a b

Tactic:
Nat.pos_iff_ne_zero.2 fun h => ?_

Premises used: Iff.mpr, Nat.pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
refine : ∀ (h : multiplicity a b = 0), False
⊢ 0 < multiplicity a b

Tactic:
refine Nat.pos_iff_ne_zero.2 fun h => ?_

Premises used: Iff.mpr, Nat.pos_iff_ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
by_contra! : ∀ (nh : ∀ (n : ℕ), a ^ (n + 1) ∣ b), False
⊢ FiniteMultiplicity a b

Tactic:
by_contra! nh
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ∀ (n : ℕ), a ^ (n + 1) ∣ b
⊢ False

Tactic:
simp [nh] at h