internlm/Lean-Github huggingface dataset:
Theorem: lin_rel_is_not_function
Proof state before:
is_fn : is_function lin_rel
⊢ False
Tactic:
rw [is_function] at is_fn
Proof state after:
is_fn : lin_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ lin_rel
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
is_fn : lin_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ lin_rel
⊢ False
Tactic:
rw [lin_rel, Set.subset_def] at is_fn
Proof state after:
is_fn : (∀ x ∈ {p | p.1 + 3 * p.2 = 4}, x ∈ Set.univ ×ˢ Set.univ) ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ {p | p.1 + 3 * p.2 = 4}
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
is_fn : (∀ x ∈ {p | p.1 + 3 * p.2 = 4}, x ∈ Set.univ ×ˢ Set.univ) ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ {p | p.1 + 3 * p.2 = 4}
⊢ False
Tactic:
rcases is_fn with ⟨rel_sub, rel_uniq⟩
Proof state after:
case intro
rel_sub : ∀ x ∈ {p | p.1 + 3 * p.2 = 4}, x ∈ Set.univ ×ˢ Set.univ
rel_uniq : ∀ (x : ℤ), ∃! y, (x, y) ∈ {p | p.1 + 3 * p.2 = 4}
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro
rel_sub : ∀ x ∈ {p | p.1 + 3 * p.2 = 4}, x ∈ Set.univ ×ˢ Set.univ
rel_uniq : ∀ (x : ℤ), ∃! y, (x, y) ∈ {p | p.1 + 3 * p.2 = 4}
⊢ False
Tactic:
simp at *
Proof state after:
case intro
rel_uniq : ∀ (x : ℤ), ∃! y, x + 3 * y = 4
rel_sub : True
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro
rel_uniq : ∀ (x : ℤ), ∃! y, x + 3 * y = 4
rel_sub : True
⊢ False
Tactic:
specialize rel_uniq 3
Proof state after:
case intro
rel_sub : True
rel_uniq : ∃! y, 3 + 3 * y = 4
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro
rel_sub : True
rel_uniq : ∃! y, 3 + 3 * y = 4
⊢ False
Tactic:
rw [ExistsUnique] at rel_uniq
Proof state after:
case intro
rel_sub : True
rel_uniq : ∃ x, 3 + 3 * x = 4 ∧ ∀ (y : ℤ), 3 + 3 * y = 4 → y = x
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro
rel_sub : True
rel_uniq : ∃ x, 3 + 3 * x = 4 ∧ ∀ (y : ℤ), 3 + 3 * y = 4 → y = x
⊢ False
Tactic:
rcases rel_uniq with ⟨y, ⟨hl, _⟩⟩
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℤ
hl : 3 + 3 * y = 4
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℤ
hl : 3 + 3 * y = 4
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
⊢ False
Tactic:
apply_fun (λ e => e - 3) at hl
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : 3 + 3 * y - 3 = 4 - 3
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : 3 + 3 * y - 3 = 4 - 3
⊢ False
Tactic:
ring_nf at hl
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y * 3 = 1
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y * 3 = 1
⊢ False
Tactic:
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at hl
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y = 1 ∧ 3 = 1 ∨ y = -1 ∧ 3 = -1
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y = 1 ∧ 3 = 1 ∨ y = -1 ∧ 3 = -1
⊢ False
Tactic:
rcases hl with (hl | hr)
Proof state after:
case intro.intro.intro.inl
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y = 1 ∧ 3 = 1
⊢ False

case intro.intro.intro.inr
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hr : y = -1 ∧ 3 = -1
⊢ False
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro.inl
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hl : y = 1 ∧ 3 = 1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: lin_rel_is_not_function
Proof state before:
case intro.intro.intro.inr
rel_sub : True
y : ℤ
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
hr : y = -1 ∧ 3 = -1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: sq_rel_is_not_function
Proof state before:
⊢ ¬is_function sq_rel
Tactic:
intro is_fn
Proof state after:
is_fn : is_function sq_rel
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
is_fn : is_function sq_rel
⊢ False
Tactic:
rw [is_function] at is_fn
Proof state after:
is_fn : sq_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℝ), ∃! y, (x, y) ∈ sq_rel
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
is_fn : sq_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℝ), ∃! y, (x, y) ∈ sq_rel
⊢ False
Tactic:
rw [sq_rel, Set.subset_def] at is_fn
Proof state after:
is_fn :
  (∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ) ∧
    ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
is_fn :
  (∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ) ∧
    ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False
Tactic:
rcases is_fn with ⟨rel_sub, rel_uniq⟩
Proof state after:
case intro
rel_sub : ∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ
rel_uniq : ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro
rel_sub : ∀ x ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}, x ∈ Set.univ ×ˢ Set.univ
rel_uniq : ∀ (x : ℝ), ∃! y, (x, y) ∈ {x | ∃ x_1, (x_1 ^ 2, x_1) = x}
⊢ False
Tactic:
simp at *
Proof state after:
case intro
rel_sub : True
rel_uniq : ∀ (x : ℝ), ∃! y, y ^ 2 = x
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro
rel_sub : True
rel_uniq : ∀ (x : ℝ), ∃! y, y ^ 2 = x
⊢ False
Tactic:
specialize rel_uniq 4
Proof state after:
case intro
rel_sub : True
rel_uniq : ∃! y, y ^ 2 = 4
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro
rel_sub : True
rel_uniq : ∃! y, y ^ 2 = 4
⊢ False
Tactic:
rw [ExistsUnique] at rel_uniq
Proof state after:
case intro
rel_sub : True
rel_uniq : ∃ x, x ^ 2 = 4 ∧ ∀ (y : ℝ), y ^ 2 = 4 → y = x
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro
rel_sub : True
rel_uniq : ∃ x, x ^ 2 = 4 ∧ ∀ (y : ℝ), y ^ 2 = 4 → y = x
⊢ False
Tactic:
rcases rel_uniq with ⟨y, ⟨_, hrel⟩⟩
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
⊢ False
Tactic:
have htwo := hrel (2) (by ring_nf)
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
⊢ False
Tactic:
have hmtwo := hrel (-2) (by ring_nf)
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
hmtwo : -2 = y
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
hmtwo : -2 = y
⊢ False
Tactic:
rw [←htwo] at hmtwo
Proof state after:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
hmtwo : -2 = 2
⊢ False
Theorem: sq_rel_is_not_function
Proof state before:
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
hmtwo : -2 = 2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: sq_rel_is_not_function
Proof state before:
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
⊢ 2 ^ 2 = 4
Tactic:
ring_nf
Proof state after:
no goals
Theorem: sq_rel_is_not_function
Proof state before:
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
⊢ (-2) ^ 2 = 4
Tactic:
ring_nf
Proof state after:
no goals
Theorem: pair_fn_injective
Proof state before:
⊢ Function.Injective pair_fn
Tactic:
intros p q eq
Proof state after:
p q : ℤ × ℤ
eq : pair_fn p = pair_fn q
⊢ p = q
Theorem: pair_fn_injective
Proof state before:
p q : ℤ × ℤ
eq : pair_fn p = pair_fn q
⊢ p = q
Tactic:
simp [pair_fn] at eq
Proof state after:
p q : ℤ × ℤ
eq : p.1 + p.2 = q.1 + q.2 ∧ 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Theorem: pair_fn_injective
Proof state before:
p q : ℤ × ℤ
eq : p.1 + p.2 = q.1 + q.2 ∧ 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Tactic:
rcases eq with ⟨hl, hr⟩
Proof state after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p = q
Tactic:
rw [Prod.eq_iff_fst_eq_snd_eq]
Proof state after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 = 2 * q.1 + q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
apply_fun (λ e => e - (p.1 + p.2)) at hr
Proof state after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (p.1 + p.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (p.1 + p.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
nth_rewrite 2 [hl] at hr
Proof state after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (q.1 + q.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : 2 * p.1 + p.2 - (p.1 + p.2) = 2 * q.1 + q.2 - (q.1 + q.2)
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
ring_nf at hr
Proof state after:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : p.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
rw [hr] at hl
Proof state after:
case intro
p q : ℤ × ℤ
hl : q.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hl : q.1 + p.2 = q.1 + q.2
hr : p.1 = q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
apply_fun (λ e => e - q.1) at hl
Proof state after:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : q.1 + p.2 - q.1 = q.1 + q.2 - q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : q.1 + p.2 - q.1 = q.1 + q.2 - q.1
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
ring_nf at hl
Proof state after:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : p.2 = q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Theorem: pair_fn_injective
Proof state before:
case intro
p q : ℤ × ℤ
hr : p.1 = q.1
hl : p.2 = q.2
⊢ p.1 = q.1 ∧ p.2 = q.2
Tactic:
exact ⟨hr, hl⟩
Proof state after:
no goals
Theorem: pair_fn_surjective
Proof state before:
⊢ Function.Surjective pair_fn
Tactic:
intro p
Proof state after:
p : ℤ × ℤ
⊢ ∃ a, pair_fn a = p
Theorem: pair_fn_surjective
Proof state before:
p : ℤ × ℤ
⊢ ∃ a, pair_fn a = p
Tactic:
simp [pair_fn]
Proof state after:
p : ℤ × ℤ
⊢ ∃ a b, (a + b, 2 * a + b) = p
Theorem: pair_fn_surjective
Proof state before:
p : ℤ × ℤ
⊢ ∃ a b, (a + b, 2 * a + b) = p
Tactic:
use (-p.1 + p.2)
Proof state after:
case h
p : ℤ × ℤ
⊢ ∃ b, (-p.1 + p.2 + b, 2 * (-p.1 + p.2) + b) = p
Theorem: pair_fn_surjective
Proof state before:
case h
p : ℤ × ℤ
⊢ ∃ b, (-p.1 + p.2 + b, 2 * (-p.1 + p.2) + b) = p
Tactic:
use (2 * p.1 - p.2)
Proof state after:
case h
p : ℤ × ℤ
⊢ (-p.1 + p.2 + (2 * p.1 - p.2), 2 * (-p.1 + p.2) + (2 * p.1 - p.2)) = p
Theorem: pair_fn_surjective
Proof state before:
case h
p : ℤ × ℤ
⊢ (-p.1 + p.2 + (2 * p.1 - p.2), 2 * (-p.1 + p.2) + (2 * p.1 - p.2)) = p
Tactic:
ring_nf
Proof state after:
no goals
Theorem: image_fn
Proof state before:
⊢ fn '' Set.Icc 3 5 = Set.Icc 12 28
Tactic:
ext x
Proof state after:
case h
x : ℝ
⊢ x ∈ fn '' Set.Icc 3 5 ↔ x ∈ Set.Icc 12 28
Theorem: image_fn
Proof state before:
case h
x : ℝ
⊢ x ∈ fn '' Set.Icc 3 5 ↔ x ∈ Set.Icc 12 28
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_image, Set.mem_Icc, fn]
Proof state after:
case h
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) ↔ 12 ≤ x ∧ x ≤ 28
Theorem: image_fn
Proof state before:
case h
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) ↔ 12 ≤ x ∧ x ≤ 28
Tactic:
constructor
Proof state after:
case h.mp
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) → 12 ≤ x ∧ x ≤ 28

case h.mpr
x : ℝ
⊢ 12 ≤ x ∧ x ≤ 28 → ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Theorem: image_fn
Proof state before:
case h.mp
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) → 12 ≤ x ∧ x ≤ 28
Tactic:
intro hex
Proof state after:
case h.mp
x : ℝ
hex : ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
⊢ 12 ≤ x ∧ x ≤ 28
Theorem: image_fn
Proof state before:
case h.mp
x : ℝ
hex : ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
⊢ 12 ≤ x ∧ x ≤ 28
Tactic:
rcases hex with ⟨y, ⟨⟨h3le, h5ge⟩ , hfy⟩⟩
Proof state after:
case h.mp.intro.intro.intro
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x ∧ x ≤ 28
Theorem: image_fn
Proof state before:
case h.mp.intro.intro.intro
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x ∧ x ≤ 28
Tactic:
constructor
Proof state after:
case h.mp.intro.intro.intro.left
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x

case h.mp.intro.intro.intro.right
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ x ≤ 28
Theorem: image_fn
Proof state before:
case h.mp.intro.intro.intro.left
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x
Tactic:
nlinarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.mp.intro.intro.intro.right
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ x ≤ 28
Tactic:
nlinarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.mpr
x : ℝ
⊢ 12 ≤ x ∧ x ≤ 28 → ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
intro hlege
Proof state after:
case h.mpr
x : ℝ
hlege : 12 ≤ x ∧ x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Theorem: image_fn
Proof state before:
case h.mpr
x : ℝ
hlege : 12 ≤ x ∧ x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
rcases hlege with ⟨h12ge, h28le⟩
Proof state after:
case h.mpr.intro
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Theorem: image_fn
Proof state before:
case h.mpr.intro
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
Tactic:
use (Real.sqrt (x - 3))
Proof state after:
case h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ (3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5) ∧ Real.sqrt (x - 3) ^ 2 + 3 = x
Theorem: image_fn
Proof state before:
case h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ (3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5) ∧ Real.sqrt (x - 3) ^ 2 + 3 = x
Tactic:
constructor
Proof state after:
case h.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x
Theorem: image_fn
Proof state before:
case h.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5
Tactic:
constructor
Proof state after:
case h.left.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3)

case h.left.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ≤ 5
Theorem: image_fn
Proof state before:
case h.left.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ≤ Real.sqrt (x - 3)
Tactic:
refine Real.le_sqrt_of_sq_le ?h.left.left.h
Proof state after:
case h.left.left.h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ^ 2 ≤ x - 3
Theorem: image_fn
Proof state before:
case h.left.left.h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 3 ^ 2 ≤ x - 3
Tactic:
linarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.left.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ≤ 5
Tactic:
refine Real.sqrt_le_iff.mpr ?h.left.right.a
Proof state after:
case h.left.right.a
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5 ∧ x - 3 ≤ 5 ^ 2
Theorem: image_fn
Proof state before:
case h.left.right.a
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5 ∧ x - 3 ≤ 5 ^ 2
Tactic:
constructor
Proof state after:
case h.left.right.a.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5

case h.left.right.a.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 ≤ 5 ^ 2
Theorem: image_fn
Proof state before:
case h.left.right.a.left
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ 5
Tactic:
nlinarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.left.right.a.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 ≤ 5 ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x
Tactic:
rw [Real.sq_sqrt]
Proof state after:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 + 3 = x

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ x - 3
Theorem: image_fn
Proof state before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 + 3 = x
Tactic:
nlinarith
Proof state after:
no goals
Theorem: image_fn
Proof state before:
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ x - 3
Tactic:
nlinarith
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
⊢ fn ⁻¹' Set.Icc 12 19 = Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
Tactic:
ext x
Proof state after:
case h
x : ℝ
⊢ x ∈ fn ⁻¹' Set.Icc 12 19 ↔ x ∈ Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
Theorem: preimage_fn
Proof state before:
case h
x : ℝ
⊢ x ∈ fn ⁻¹' Set.Icc 12 19 ↔ x ∈ Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
Tactic:
simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_preimage, Set.mem_Icc, neg_le_neg_iff,
  neg_lt_neg_iff, Set.mem_union, fn]
Proof state after:
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
constructor
Proof state after:
case h.mp
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 → 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

case h.mpr
x : ℝ
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3 → 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Theorem: preimage_fn
Proof state before:
case h.mp
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 → 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
intro hlege
Proof state after:
case h.mp
x : ℝ
hlege : 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp
x : ℝ
hlege : 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rcases hlege with ⟨h12le, h19ge⟩
Proof state after:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have heq12 : (12 : ℝ) = (3^2) + 3 := by ring
Proof state after:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rw [heq12, add_le_add_iff_right, sq_le_sq, abs_of_pos (by simp), le_abs, le_neg] at h12le
Proof state after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have heq19 : (19 : ℝ) = (4^2) + 3 := by ring
Proof state after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
have lt04 : (0 : ℝ) < 4 := by simp
Proof state after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rw [heq19, add_le_add_iff_right, sq_le_sq, abs_of_pos lt04, abs_le] at h19ge
Proof state after:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
rcases h12le with (h3le | hm3ge)
Proof state after:
case h.mp.intro.inl
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3

case h.mp.intro.inr
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 12 = 3 ^ 2 + 3
Tactic:
ring
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
x : ℝ
h12le : |3| ≤ |x|
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 0 < 3
Tactic:
simp
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 19 = 4 ^ 2 + 3
Tactic:
ring
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 0 < 4
Tactic:
simp
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mp.intro.inl
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
left
Proof state after:
case h.mp.intro.inl.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4
Theorem: preimage_fn
Proof state before:
case h.mp.intro.inl.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
h3le : 3 ≤ x
⊢ 3 ≤ x ∧ x ≤ 4
Tactic:
exact ⟨h3le, h19ge.2⟩
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mp.intro.inr
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
Tactic:
right
Proof state after:
case h.mp.intro.inr.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ -4 ≤ x ∧ x ≤ -3
Theorem: preimage_fn
Proof state before:
case h.mp.intro.inr.h
x : ℝ
h19ge : -4 ≤ x ∧ x ≤ 4
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
lt04 : 0 < 4
hm3ge : x ≤ -3
⊢ -4 ≤ x ∧ x ≤ -3
Tactic:
exact ⟨h19ge.1, hm3ge⟩
Proof state after:
no goals
Theorem: preimage_fn
Proof state before:
case h.mpr
x : ℝ
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3 → 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
intro hlege
Proof state after:
case h.mpr
x : ℝ
hlege : 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Theorem: preimage_fn
Proof state before:
case h.mpr
x : ℝ
hlege : 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
rcases hlege with (⟨h3le, h4ge⟩ | ⟨hm4le, hm3ge⟩)
Proof state after:
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Theorem: preimage_fn
Proof state before:
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
Tactic:
constructor
Proof state after:
case h.mpr.inl.intro.left
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3

case h.mpr.inl.intro.right
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ x ^ 2 + 3 ≤ 19