Theorem: bijective_fn (meetings/ex4.lean)

State before:
⊢ Function.Bijective bij_fun
Tactic:
rw [Function.Bijective, Function.Injective, Function.Surjective]
State after:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧ ∀ (b : { x // x > Real.sqrt 2 }), ∃ a, bij_fun a = b

State before:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧ ∀ (b : { x // x > Real.sqrt 2 }), ∃ a, bij_fun a = b
Tactic:
simp only [Subtype.forall, ge_iff_le]
State after:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧
    ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }

State before:
⊢ (∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂) ∧
    ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Tactic:
constructor
State after:
case left

⊢ ∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂

case right

⊢ ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }

State before:
case left

⊢ ∀ ⦃a₁ a₂ : ℝ⦄, bij_fun a₁ = bij_fun a₂ → a₁ = a₂
Tactic:
intros a b heq
State after:
case left
a b : ℝ
heq : bij_fun a = bij_fun b
⊢ a = b

State before:
case left
a b : ℝ
heq : bij_fun a = bij_fun b
⊢ a = b
Tactic:
simp_rw [bij_fun] at heq
State after:
case left
a b : ℝ
heq :
  { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
    { val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) }
⊢ a = b

State before:
case left
a b : ℝ
heq :
  { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
    { val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) }
⊢ a = b
Tactic:
apply_fun(λ e => Real.log (e - Real.sqrt 2)) at heq
State after:
case left
a b : ℝ
heq :
  Real.log
      (↑{ val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2) =
    Real.log
      (↑{ val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2)
⊢ a = b

State before:
case left
a b : ℝ
heq :
  Real.log
      (↑{ val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2) =
    Real.log
      (↑{ val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2)
⊢ a = b
Tactic:
simp only [add_sub_cancel, Real.log_exp] at heq
State after:
case left
a b : ℝ
heq : a = b
⊢ a = b

State before:
case left
a b : ℝ
heq : a = b
⊢ a = b
Tactic:
exact heq
State after:
no goals

State before:
case right

⊢ ∀ (a : ℝ) (b : a > Real.sqrt 2), ∃ a_1, bij_fun a_1 = { val := a, property := b }
Tactic:
intros x hle
State after:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a, bij_fun a = { val := x, property := hle }

State before:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a, bij_fun a = { val := x, property := hle }
Tactic:
simp_rw [bij_fun]
State after:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a,
    { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
      { val := x, property := hle }

State before:
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a,
    { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
      { val := x, property := hle }
Tactic:
use (Real.log (x - Real.sqrt 2))
State after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ { val := Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2,
      property := (_ : Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 > Real.sqrt 2) } =
    { val := x, property := hle }

State before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ { val := Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2,
      property := (_ : Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 > Real.sqrt 2) } =
    { val := x, property := hle }
Tactic:
simp only [Subtype.mk.injEq]
State after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 = x

State before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 = x
Tactic:
rw [Real.exp_log (by linarith)]
State after:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ x - Real.sqrt 2 + Real.sqrt 2 = x

State before:
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ x - Real.sqrt 2 + Real.sqrt 2 = x
Tactic:
ring_nf
State after:
no goals

State before:
x : ℝ
hle : x > Real.sqrt 2
⊢ 0 < x - Real.sqrt 2
Tactic:
linarith
State after:
no goals