lemma proved tactic proof

`lcm_9_5_eq_45`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  38lemma lcm_9_5_eq_45 : Nat.lcm 9 5 = 45 := by

proof body

Tactic-mode proof.

  39  have hg : Nat.gcd 9 5 = 1 := by decide
  40  have h := Nat.gcd_mul_lcm 9 5
  41  have h' : Nat.lcm 9 5 = 9 * 5 := by simpa [hg, Nat.one_mul] using h
  42  have hmul : 9 * 5 = 45 := by decide
  43  simpa [hmul] using h'
  44
  45/-- 9 ∣ 45. -/

depends on (2)

Lean names referenced from this declaration's body.

one_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
gcd_mul_lcm in IndisputableMonolith.NumberTheory.Primes.GCDLCM decl_use