-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_self {a : α} : multiplicity a a = 1

Proof state:
case pos.intro.inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False

Tactic:
have : IsUnit a := isUnit_of_mul_eq_one a v hv.symm

Result:
case pos.intro.inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
this : IsUnit a
⊢ False

Proof state:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
⊢ False

Tactic:
obtain hv | rfl := hv

Result:
case pos.intro.inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False

case pos.intro.inr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a

Tactic:
simp only [pow_one, dvd_refl, reduceAdd, true_and]

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ ¬a ^ 2 ∣ a

Proof state:
case pos.intro.inr
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
simpa using ha.ne_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
⊢ multiplicity a a = 1

Tactic:
by_cases ha : FiniteMultiplicity a a

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Proof state:
case pos.intro.inl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
this : IsUnit a
⊢ False

Tactic:
simpa [this] using ha.not_unit

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
simp [ha]

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a = a ^ 2 * v
⊢ False

Tactic:
nth_rw 1 [← mul_one a] at hv

Result:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False

Proof state:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False

Tactic:
simp only [sq, mul_assoc, mul_eq_mul_left_iff] at hv

Result:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
⊢ False

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
rw [ha.multiplicity_eq_iff]

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a

Proof state:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
⊢ ¬a ^ 2 ∣ a

Tactic:
rintro ⟨v, hv⟩

Result:
case pos.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a = a ^ 2 * v
⊢ False