Theorem: lin_rel_is_not_function (meetings/ex4.lean)

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

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

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

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

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

State before:
case intro
rel_uniq : ∀ (x : ℤ), ∃! y, x + 3 * y = 4
rel_sub : True
⊢ False
Tactic:
specialize rel_uniq 3
State after:
case intro
rel_sub : True
rel_uniq : ∃! y, 3 + 3 * y = 4
⊢ False

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

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

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

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

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

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

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

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