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

State before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
⊢ x ∈ swap '' s ↔ x.swap ∈ s
Tactic:
have h := @swap_mem _ _ x.snd x.fst s
State after:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (x.1, x.2) ∈ swap '' s ↔ (x.2, x.1) ∈ s
⊢ x ∈ swap '' s ↔ x.swap ∈ s

State before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (x.1, x.2) ∈ swap '' s ↔ (x.2, x.1) ∈ s
⊢ x ∈ swap '' s ↔ x.swap ∈ s
Tactic:
simp at h ⊢
State after:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ (x.2, x.1) ∈ s
⊢ (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ x.swap ∈ s

State before:
A B C 𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
x : A × B
s : Set (B × A)
h : (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ (x.2, x.1) ∈ s
⊢ (∃ a b, (a, b) ∈ s ∧ (b, a) = x) ↔ x.swap ∈ s
Tactic:
exact h
State after:
no goals