-- Mathlib/RingTheory/Localization/NumDen.lean
@[simp]
lemma num_zero : IsFractionRing.num A (0 : K) = 0

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ num A 0 = 0

Tactic:
have := mk'_num_den' A (0 : K)

Result:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : (algebraMap A K) (num A 0) / (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Proof state:
case h.e'_3
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) (num A 0) = 0
⊢ (algebraMap A K) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : (algebraMap A K) (num A 0) = 0 ∨ (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Tactic:
rcases this with h | h

Result:
case inl
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) (num A 0) = 0
⊢ num A 0 = 0

case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : (algebraMap A K) (num A 0) / (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Tactic:
simp only [div_eq_zero_iff] at this

Result:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
this : (algebraMap A K) (num A 0) = 0 ∨ (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Proof state:
case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = (algebraMap A K) 0
⊢ num A 0 = 0

Tactic:
absurd FaithfulSMul.algebraMap_injective A K h

Result:
case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = (algebraMap A K) 0
⊢ ¬↑(den A 0) = 0

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = 0
⊢ (algebraMap A K) ↑(den A 0) = (algebraMap A K) 0

Tactic:
convert h

Result:
case h.e'_3
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = 0
⊢ (algebraMap A K) 0 = 0

Proof state:
case h.e'_3
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = 0
⊢ (algebraMap A K) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = 0
⊢ num A 0 = 0

Tactic:
replace h : algebraMap A K (den A (0 : K)) = algebraMap A K 0 := by convert h; simp

Result:
case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = (algebraMap A K) 0
⊢ num A 0 = 0

Proof state:
case inr
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) ↑(den A 0) = (algebraMap A K) 0
⊢ ¬↑(den A 0) = 0

Tactic:
apply nonZeroDivisors.coe_ne_zero

Result:
no goals

Proof state:
case inl
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) (num A 0) = 0
⊢ num A 0 = 0

Tactic:
exact FaithfulSMul.algebraMap_injective A K (by convert h; simp)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) (num A 0) = 0
⊢ (algebraMap A K) (num A 0) = (algebraMap A K) 0

Tactic:
convert h

Result:
case h.e'_3
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : (algebraMap A K) (num A 0) = 0
⊢ (algebraMap A K) 0 = 0