Theorem: inter_image_fun_inter_not_eq (meetings/ex4.lean)

State before:
⊢ ∃ α β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (ℤ)
State after:
case h

⊢ ∃ β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y

State before:
case h

⊢ ∃ β f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (ℤ)
State after:
case h

⊢ ∃ f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y

State before:
case h

⊢ ∃ f X Y, f '' (X ∩ Y) ≠ f '' X ∩ f '' Y
Tactic:
use (λ _ => 0)
State after:
case h

⊢ ∃ X Y, (fun x => 0) '' (X ∩ Y) ≠ (fun x => 0) '' X ∩ (fun x => 0) '' Y

State before:
case h

⊢ ∃ X Y, (fun x => 0) '' (X ∩ Y) ≠ (fun x => 0) '' X ∩ (fun x => 0) '' Y
Tactic:
use ({1} : Set ℤ)
State after:
case h

⊢ ∃ Y, (fun x => 0) '' ({1} ∩ Y) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' Y

State before:
case h

⊢ ∃ Y, (fun x => 0) '' ({1} ∩ Y) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' Y
Tactic:
use ({2} : Set ℤ)
State after:
case h

⊢ (fun x => 0) '' ({1} ∩ {2}) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' {2}

State before:
case h

⊢ (fun x => 0) '' ({1} ∩ {2}) ≠ (fun x => 0) '' {1} ∩ (fun x => 0) '' {2}
Tactic:
simp only [Set.inter_singleton_nonempty, Set.image_singleton, Set.inter_self, ne_eq]
State after:
case h

⊢ ¬(fun x => 0) '' ({1} ∩ {2}) = {0}

State before:
case h

⊢ ¬(fun x => 0) '' ({1} ∩ {2}) = {0}
Tactic:
intro heq
State after:
case h
heq : (fun x => 0) '' ({1} ∩ {2}) = {0}
⊢ False

State before:
case h
heq : (fun x => 0) '' ({1} ∩ {2}) = {0}
⊢ False
Tactic:
rw [Set.inter_def] at heq
State after:
case h
heq : (fun x => 0) '' {a | a ∈ {1} ∧ a ∈ {2}} = {0}
⊢ False

State before:
case h
heq : (fun x => 0) '' {a | a ∈ {1} ∧ a ∈ {2}} = {0}
⊢ False
Tactic:
simp at heq
State after:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
⊢ False

State before:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
⊢ False
Tactic:
have hf {a : ℤ} : (a = 1 ∧ a = 2) = False := by
  simp_all only [eq_iff_iff, iff_false, not_and, OfNat.one_ne_ofNat, not_false_eq_true, implies_true]
State after:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False

State before:
case h
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
⊢ False
Tactic:
simp_rw [hf] at heq
State after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : (fun x => 0) '' {a | False} = {0}
⊢ False

State before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : (fun x => 0) '' {a | False} = {0}
⊢ False
Tactic:
simp at heq
State after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : ∅ = {0}
⊢ False

State before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : ∅ = {0}
⊢ False
Tactic:
symm at heq
State after:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : {0} = ∅
⊢ False

State before:
case h
hf : ∀ {a : ℤ}, (a = 1 ∧ a = 2) = False
heq : {0} = ∅
⊢ False
Tactic:
exact Set.singleton_ne_empty 0 heq
State after:
no goals

State before:
heq : (fun x => 0) '' {a | a = 1 ∧ a = 2} = {0}
a : ℤ
⊢ (a = 1 ∧ a = 2) = False
Tactic:
simp_all only [eq_iff_iff, iff_false, not_and, OfNat.one_ne_ofNat, not_false_eq_true, implies_true]
State after:
no goals