Theorem: swap_swap (Ray/Misc/Prod.lean)

State before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
⊢ swap '' (swap '' s) = s
Tactic:
ext x
State after:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ swap '' (swap '' s) ↔ x ∈ s

State before:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ swap '' (swap '' s) ↔ x ∈ s
Tactic:
simp only [Set.mem_image, Prod.exists]
State after:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) ↔ x ∈ s

State before:
case h
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) ↔ x ∈ s
Tactic:
constructor
State after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) → x ∈ s

case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ s → ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x

State before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ (∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x) → x ∈ s
Tactic:
intro ⟨a,b,⟨⟨c,d,e,f⟩,g⟩⟩
State after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ x ∈ s

State before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ x ∈ s
Tactic:
rw [←g, ←f]
State after:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ (c, d).swap.swap ∈ s

State before:
case h.mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
a : B
b c : A
d : B
e : (c, d) ∈ s
f : (c, d).swap = (a, b)
g : (a, b).swap = x
⊢ (c, d).swap.swap ∈ s
Tactic:
simpa only [swap]
State after:
no goals

State before:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
⊢ x ∈ s → ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Tactic:
intro m
State after:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
m : x ∈ s
⊢ ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x

State before:
case h.mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
s : Set (A × B)
x : A × B
m : x ∈ s
⊢ ∃ a b, (∃ a_1 b_1, (a_1, b_1) ∈ s ∧ (a_1, b_1).swap = (a, b)) ∧ (a, b).swap = x
Tactic:
exact ⟨x.2,x.1,⟨x.1,x.2,m,rfl⟩,rfl⟩
State after:
no goals