/-- The ratio `a : b` is *equivalent* to `c : d` if `c : d` is a scaled copy of it:`c = k · a` and `d = k · b` for one scale factor `k > 0`. -/def Equivalent (a b c d : Rat) : Prop := ∃ k : Rat, 0 < k ∧ c = k * a ∧ d = k * b
equivalent_iff_cross_multheoremProved here from basic factspropext, Classical.choice, Quot.sound
equivalent_iff_cross_mulLean 4Proved here from basic factsFormally verified
/-- **Cross-multiplication.** For positive quantities, `a : b` is equivalent to `c : d` exactlywhen `a · d = b · c`. One way: `a·(k·b) = b·(k·a)`. The other way: the scale factor is`k = c / a`, and `a·d = b·c` gives `d = k·b`. (Only `a > 0` and `c > 0` are needed.) -/theorem equivalent_iff_cross_mul {a b c d : Rat} (ha : 0 < a) (hc : 0 < c) : Equivalent a b c d ↔ a * d = b * c := by constructor · intro ⟨k, _, hck, hdk⟩ rw [hck, hdk] grind · intro h have ha0 : a ≠ 0 := Rat.ne_of_gt ha refine ⟨c / a, ?_, ?_, ?_⟩ · rw [Rat.lt_div_iff ha] simpa using hc · grind · -- From `a · d = b · c`: `d = (b · c) / a = (c / a) · b`. grind
lemonadetheoremProved here from basic factspropext, Classical.choice, Quot.sound
lemonadeLean 4Proved here from basic factsFormally verified
/-- The lemonade puzzle: `2 : 3` (concentrate to water) and `3 : 5` are **not** equivalent,because `2 · 5 = 10` but `3 · 3 = 9`. Adding one cup of each is not scaling. -/theorem lemonade : ¬ Equivalent 2 3 3 5 := by rw [equivalent_iff_cross_mul (by decide) (by decide)] decide +kernel
/-- A relationship `y = f x` is *proportional* if there is one constant `k` (the constant ofproportionality) with `f x = k · x` for every `x`. -/def IsProportional (f : Rat → Rat) : Prop := ∃ k : Rat, ∀ x, f x = k * x
affine_not_proportionaltheoremProved here from basic factspropext, Classical.choice, Quot.sound
affine_not_proportionalLean 4Proved here from basic factsFormally verified
/-- `y = 2x + 1` is a straight line but **not** proportional: it gives `1`, not `0`, at `x = 0`. -/theorem affine_not_proportional : ¬ IsProportional (fun x => 2 * x + 1) := by intro hf have h0 := proportional_zero hf grind
proportional_iff_ratio_consttheoremProved here from basic factspropext, Classical.choice, Quot.sound
proportional_iff_ratio_constLean 4Proved here from basic factsFormally verified
/-- **Spotting proportionality in a table.** `f` is proportional exactly when `f 0 = 0` and theratio `f x / x` is the same for every `x ≠ 0`. Then `k = f 1`, and `f x / x = f 1` gives`f x = f 1 · x`. -/theorem proportional_iff_ratio_const (f : Rat → Rat) : IsProportional f ↔ f 0 = 0 ∧ ∀ x, x ≠ 0 → f x / x = f 1 := by constructor · intro hf refine ⟨proportional_zero hf, ?_⟩ obtain ⟨k, hk⟩ := hf intro x hx rw [hk x, hk 1] grind · intro ⟨h0, hratio⟩ refine ⟨f 1, ?_⟩ intro x by_cases hx : x = 0 · rw [hx, h0, Rat.mul_zero] · have h := hratio x hx grind
slope_consttheoremProved here from basic factspropext, Classical.choice, Quot.sound
slope_constLean 4Proved here from basic factsFormally verified
/-- **The graph is a straight line through the origin.** Between any two different points ofthe graph of `y = k · x`, the slope `(y₂ - y₁)/(x₂ - x₁)` is the same number `k`. -/theorem slope_const (k x₁ x₂ : Rat) (h : x₁ ≠ x₂) : (k * x₂ - k * x₁) / (x₂ - x₁) = k := by have hne : x₂ - x₁ ≠ 0 := by intro h0 apply h grind grind
proportional_addtheoremProved here from basic factspropext, Classical.choice, Quot.sound
proportional_addLean 4Proved here from basic factsFormally verified
/-- **Adding rows of a ratio table.** If `f` is proportional, then`f (x + y) = k·(x + y) = k·x + k·y = f x + f y`. -/theorem proportional_add {f : Rat → Rat} (hf : IsProportional f) (x y : Rat) : f (x + y) = f x + f y := by obtain ⟨k, hk⟩ := hf rw [hk, hk x, hk y, Rat.mul_add]
proportional_scaletheoremProved here from basic factspropext, Classical.choice, Quot.sound
proportional_scaleLean 4Proved here from basic factsFormally verified
/-- **Scaling a row of a ratio table.** If `f` is proportional, then `f (c · x) = c · f x`. -/theorem proportional_scale {f : Rat → Rat} (hf : IsProportional f) (c x : Rat) : f (c * x) = c * f x := by obtain ⟨k, hk⟩ := hf rw [hk, hk x] grind
additive_nattheoremProved here from basic factspropext, Classical.choice, Quot.sound
additive_natLean 4Proved here from basic factsFormally verified
/-- **Additive implies proportional (for whole numbers).** If the price of `m + n` items isalways the price of `m` items plus the price of `n` items, then the price of `n` items is`n` times the price of one: `f n = n · f 1`. Proof by induction on `n`. -/theorem additive_nat (f : Nat → Rat) (hadd : ∀ m n, f (m + n) = f m + f n) : ∀ n : Nat, f n = n * f 1 := by have h0 : f 0 = 0 := by have h := hadd 0 0 simp at h grind intro n induction n with | zero => simp [h0] | succ n ih => rw [hadd n 1, ih] push_cast grind
increase_by_percenttheoremProved here from basic factspropext, Classical.choice, Quot.sound
increase_by_percentLean 4Proved here from basic factsFormally verified
/-- Increasing `x` by `p` percent multiplies it by `1 + p/100`:`x + (p/100)·x = (1 + p/100)·x`. -/theorem increase_by_percent (p x : Rat) : x + percentOf p x = (1 + p / 100) * x := by unfold percentOf grind
successive_changes_commutetheoremProved here from basic factspropext, Classical.choice, Quot.sound
successive_changes_commuteLean 4Proved here from basic factsFormally verified
/-- Successive percentage changes **multiply**, so their order does not matter: a rise of `p`%then a rise of `q`% gives the same result as `q`% then `p`%. -/theorem successive_changes_commute (x p q : Rat) : x * (1 + p / 100) * (1 + q / 100) = x * (1 + q / 100) * (1 + p / 100) := by grind
ten_up_ten_downtheoremProved here from basic factspropext, Classical.choice, Quot.sound
ten_up_ten_downLean 4Proved here from basic factsFormally verified
/-- A 10% rise followed by a 10% fall multiplies by `1.1 × 0.9 = 0.99`: you end 1% lower. -/theorem ten_up_ten_down (x : Rat) : x * (110 / 100) * (90 / 100) = 99 / 100 * x := by grind
up_down_factortheoremProved here from basic factspropext, Classical.choice, Quot.sound
up_down_factorLean 4Proved here from basic factsFormally verified
/-- Up by a fraction `r`, then down by the same fraction `r`: the overall factor is`(1 + r)(1 - r) = 1 - r²`. -/theorem up_down_factor (x r : Rat) : x * (1 + r) * (1 - r) = x * (1 - r * r) := by grind
sq_postheoremProved here from basic factspropext, Classical.choice, Quot.sound
sq_posLean 4Proved here from basic factsFormally verified
/-- The square of a non-zero rational number is positive (a positive times a positive, or anegative times a negative). -/theorem sq_pos {r : Rat} (hr : r ≠ 0) : 0 < r * r := by rcases Rat.le_total (a := r) (b := 0) with hle | hge · -- `r < 0`, so `-r > 0` and `r · r = (-r) · (-r) > 0`. have hneg : r < 0 := Rat.lt_of_le_of_ne hle hr have h : 0 < -r := by have := Rat.neg_lt_neg hneg simpa using this have := Rat.mul_pos h h grind · -- `r > 0`, so `r · r > 0`. exact Rat.mul_pos (Rat.lt_of_le_of_ne hge (Ne.symm hr)) (Rat.lt_of_le_of_ne hge (Ne.symm hr))
up_down_lttheoremProved here from basic factspropext, Classical.choice, Quot.sound
up_down_ltLean 4Proved here from basic factsFormally verified
/-- **Up and down by the same percentage never gets you back.** For a positive amount `x` andany non-zero change `r`, rising by `r` and then falling by `r` leaves less than `x`:`x · (1 - r²) = x - x·r² < x`. -/theorem up_down_lt {x r : Rat} (hx : 0 < x) (hr : r ≠ 0) : x * (1 + r) * (1 - r) < x := by rw [up_down_factor] have hxr : 0 < x * (r * r) := Rat.mul_pos hx (sq_pos hr) grind
undo_increasetheoremProved here from basic factspropext, Classical.choice, Quot.sound
undo_increaseLean 4Proved here from basic factsFormally verified
/-- **Undoing a percentage rise.** A rise of `p`% is undone by a fall of `100p/(100 + p)`%, notof `p`%: `(1 + p/100) · (1 - p/(100 + p)) = 1`. For `p = 25` the fall is `20`%. -/theorem undo_increase (p : Rat) (hp : 0 ≤ p) : (1 + p / 100) * (1 - p / (100 + p)) = 1 := by have hpos : (0 : Rat) < 100 + p := by have : (0 : Rat) < 100 := by decide grind have hne : (100 : Rat) + p ≠ 0 := Rat.ne_of_gt hpos grind
/-- The graph of a proportional relationship passes through the origin.Hint: `obtain ⟨k, hk⟩ := hf`, then rewrite with `hk` and `Rat.mul_zero`. -/theorem proportional_zero {f : Rat → Rat} (hf : IsProportional f) : f 0 = 0 := by sorry
Show the compiled solution
proportional_zeroLean 4Proved here from basic factsFormally verified
/-- A proportional relationship sends `0` to `0`: `f 0 = k · 0 = 0`. Its graph passes throughthe origin. -/theorem proportional_zero {f : Rat → Rat} (hf : IsProportional f) : f 0 = 0 := by obtain ⟨k, hk⟩ := hf rw [hk, Rat.mul_zero]
/-- Adding two rows of a ratio table gives another row.Hint: after `obtain ⟨k, hk⟩ := hf`, rewrite `f (x + y)`, `f x` and `f y` with `hk`, then usethe distributive law `Rat.mul_add`. -/theorem proportional_add {f : Rat → Rat} (hf : IsProportional f) (x y : Rat) : f (x + y) = f x + f y := by sorry
Show the compiled solution
proportional_addLean 4Proved here from basic factsFormally verified
/-- **Adding rows of a ratio table.** If `f` is proportional, then`f (x + y) = k·(x + y) = k·x + k·y = f x + f y`. -/theorem proportional_add {f : Rat → Rat} (hf : IsProportional f) (x y : Rat) : f (x + y) = f x + f y := by obtain ⟨k, hk⟩ := hf rw [hk, hk x, hk y, Rat.mul_add]