Elementary math

Stream: new members

[Iocta]

Are there tactics that can solve these holes? What is recommended here?

import Mathlib
import Mathlib.Tactic
import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Algebra.Order.Sub.Canonical

open BigOperators Nat Finset

open Real

example (a : ℝ → ℝ) (ha : ∃ s r, a = (fun i => s * r ^ i)) (h1 : a 1 = 2) (h2 : a 2 = 3) : a 3 = 9/2 := by
  cases ha with
  | intro s hs =>
    cases hs with
    | intro r hr =>
      rw [hr]
      rw [hr] at h1 h2
      dsimp only
      dsimp at h1 h2
      have r_eq_three_div_two : r = 3/2 := sorry
      have s_eq_four_div_three : s = 4/3 := by
        rw [r_eq_three_div_two, rpow_one] at h1
        linarith
      rw [r_eq_three_div_two, s_eq_four_div_three]
      sorry
      /-
      case intro.intro
      a : ℝ → ℝ
      s r : ℝ
      h2 : s * r ^ 2 = 3
      h1 : s * r ^ 1 = 2
      hr : a = fun i ↦ s * r ^ i
      r_eq_three_div_two : r = 3 / 2
      s_eq_four_div_three : s = 4 / 3
      ⊢ 4 / 3 * (3 / 2) ^ 3 = 9 / 2
      -/

[Eric Wieser]

norm_num is the tactic you want

[Iocta]

What about the other sorry?

[Iocta]

basically

      s r : ℝ
      h2 : s * r ^ 2 = 3
      h1 : s * r ^ 1 = 2
      ⊢ r = 3 / 2

[Eric Wieser]

Another tip would be to start your proof with

  obtain ⟨s, r, rfl⟩ := ha
  dsimp only at *

[Eric Wieser]

For your goal state above, have := congr($h2 / $h1) is helpful

[Julian Berman]

A lazy way (found partially via hint) seems to be have r_eq_three_div_two : r = 3/2 := by simp_all [rpow_two, rpow_one]; nlinarith

[Iocta]

I see, that's

have r_eq_three_div_two : r = 3/2 := by
    rw [rpow_one] at h1
    rw [rpow_two] at h2
    nlinarith

[Iocta]

rpow_two is a little strange.

[Matt Diamond]

do you mean the fact that it looks like x ^ 2 = x ^ 2?

[Matt Diamond]

if you look at the source, it's actually x ^ (2 : ℝ) = x ^ (2 : ℕ)

[Eric Wieser]

The general case is docs#Real.rpow_ofNat, which looks even stranger!

[Matt Diamond]

hmm... @Eric Wieser is it missing?