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

State before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s ↔ (a, b) ∈ s
Tactic:
constructor
State after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s → (a, b) ∈ s

case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (a, b) ∈ s → (b, a) ∈ swap '' s

State before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (b, a) ∈ swap '' s → (a, b) ∈ s
Tactic:
intro m
State after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (b, a) ∈ swap '' s
⊢ (a, b) ∈ s

State before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (b, a) ∈ swap '' s
⊢ (a, b) ∈ s
Tactic:
simp at m
State after:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : ∃ a_1 b_1, (a_1, b_1) ∈ s ∧ b_1 = b ∧ a_1 = a
⊢ (a, b) ∈ s

State before:
case mp
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : ∃ a_1 b_1, (a_1, b_1) ∈ s ∧ b_1 = b ∧ a_1 = a
⊢ (a, b) ∈ s
Tactic:
rcases m with ⟨a', b', m, hb, ha⟩
State after:
case mp.intro.intro.intro.intro
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
a' : A
b' : B
m : (a', b') ∈ s
hb : b' = b
ha : a' = a
⊢ (a, b) ∈ s

State before:
case mp.intro.intro.intro.intro
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
a' : A
b' : B
m : (a', b') ∈ s
hb : b' = b
ha : a' = a
⊢ (a, b) ∈ s
Tactic:
rwa [← ha, ← hb]
State after:
no goals

State before:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
⊢ (a, b) ∈ s → (b, a) ∈ swap '' s
Tactic:
intro m
State after:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (a, b) ∈ s
⊢ (b, a) ∈ swap '' s

State before:
case mpr
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
a : A
b : B
s : Set (A × B)
m : (a, b) ∈ s
⊢ (b, a) ∈ swap '' s
Tactic:
exact Set.mem_image_of_mem swap m
State after:
no goals