Theorem: sq_rel_is_not_function (meetings/ex4.lean)

State before:
⊢ ¬is_function sq_rel
Tactic:
intro is_fn
State after:
is_fn : is_function sq_rel
⊢ False

State before:
is_fn : is_function sq_rel
⊢ False
Tactic:
rw [is_function] at is_fn
State after:
is_fn : sq_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℝ), ∃! y, (x, y) ∈ sq_rel
⊢ False

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
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

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⟩
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

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 *
State after:
case intro
rel_sub : True
rel_uniq : ∀ (x : ℝ), ∃! y, y ^ 2 = x
⊢ False

State before:
case intro
rel_sub : True
rel_uniq : ∀ (x : ℝ), ∃! y, y ^ 2 = x
⊢ False
Tactic:
specialize rel_uniq 4
State after:
case intro
rel_sub : True
rel_uniq : ∃! y, y ^ 2 = 4
⊢ False

State before:
case intro
rel_sub : True
rel_uniq : ∃! y, y ^ 2 = 4
⊢ False
Tactic:
rw [ExistsUnique] at rel_uniq
State after:
case intro
rel_sub : True
rel_uniq : ∃ x, x ^ 2 = 4 ∧ ∀ (y : ℝ), y ^ 2 = 4 → y = x
⊢ False

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⟩⟩
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

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)
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

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)
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals