Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.add_preserves_nonzero_denominators (Lean4Axiomatic/Rational/Impl/Fraction/Naive.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, Nonzero p.denominator → Nonzero q.denominator → Nonzero (p + q).denominator
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
pn pd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, Nonzero (pn//pd).denominator → Nonzero q.denominator → Nonzero (pn//pd + q).denominator
Tactic:
intro (qn//qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero (qn//qd).denominator → Nonzero (pn//pd + qn//qd).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ Nonzero (pn//pd).denominator → Nonzero (qn//qd).denominator → Nonzero (pn//pd + qn//qd).denominator
Tactic:
intro (_ : Nonzero pd) (_ : Nonzero qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pn//pd + qn//qd).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pn//pd + qn//qd).denominator
Tactic:
show Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero ((pn * qd + pd * qn)//(pd * qd)).denominator
Tactic:
show Nonzero (pd * qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pd * qd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
x✝¹ : Nonzero pd
x✝ : Nonzero qd
⊢ Nonzero (pd * qd)
Tactic:
exact Integer.mul_preserves_nonzero ‹Nonzero pd› ‹Nonzero qd›
State after:
no goals