Theorem: Equiv.subsetEquivSubset_image_val (Matroid/ForMathlib/Logic_Embedding_Set.lean)

State before:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
⊢ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) = ↑(⇑e '' (inclusion has '' u))
Tactic:
ext x
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ x ∈ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) ↔ x ∈ ↑(⇑e '' (inclusion has '' u))

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ x ∈ ↑(⇑(e.subsetEquivSubset has hbt h_eq) '' u) ↔ x ∈ ↑(⇑e '' (inclusion has '' u))
Tactic:
simp only [mem_image, mem_image_equiv, Subtype.exists, exists_and_right, exists_eq_right,
  inclusion_mk, Subtype.mk.injEq, exists_and_right, exists_eq_right, exists_and_left,
  subsetEquivSubset, coe_fn_mk, Subtype.mk.injEq, exists_prop]
State after:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) ↔
    ∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩

State before:
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) ↔
    ∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩
Tactic:
constructor
State after:
case h.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) →
    ∃ (x_1 : x ∈ t), ∃ a_2, (∃ (x : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_2 ∈ s), e ⟨a_2, ⋯⟩ = ⟨x, ⋯⟩

case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩) →
    x ∈ b ∧ ∃ a_2, ∃ (h : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u ∧ ↑(e ⟨a_2, ⋯⟩) = x

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (∃ (x_1 : x ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨x, ⋯⟩) →
    x ∈ b ∧ ∃ a_2, ∃ (h : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u ∧ ↑(e ⟨a_2, ⋯⟩) = x
Tactic:
simp only [forall_exists_index, and_imp]
State after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ ∀ (x_1 : x ∈ t) (x_2 : α) (x_3 : x_2 ∈ a),
    ⟨x_2, ⋯⟩ ∈ u →
      ∀ (x_4 : x_2 ∈ s), e ⟨x_2, ⋯⟩ = ⟨x, ⋯⟩ → x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ ∀ (x_1 : x ∈ t) (x_2 : α) (x_3 : x_2 ∈ a),
    ⟨x_2, ⋯⟩ ∈ u →
      ∀ (x_4 : x_2 ∈ s), e ⟨x_2, ⋯⟩ = ⟨x, ⋯⟩ → x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Tactic:
rintro hxt v hva hvu hvs hvx
State after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x
Tactic:
refine ⟨?_, ⟨v, hva, hvu, by rw [hvx]⟩⟩
State after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ x ∈ b
Tactic:
specialize h_eq ⟨v, hvs⟩
State after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : ↑(e ⟨v, hvs⟩) ∈ b ↔ ↑⟨v, hvs⟩ ∈ a
⊢ x ∈ b

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : ↑(e ⟨v, hvs⟩) ∈ b ↔ ↑⟨v, hvs⟩ ∈ a
⊢ x ∈ b
Tactic:
rw [hvx, Subtype.coe_mk, Subtype.coe_mk] at h_eq
State after:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : x ∈ b ↔ v ∈ a
⊢ x ∈ b

State before:
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
h_eq : x ∈ b ↔ v ∈ a
⊢ x ∈ b
Tactic:
rwa [h_eq]
State after:
no goals

State before:
case h.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
⊢ (x ∈ b ∧ ∃ a_1, ∃ (h : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u ∧ ↑(e ⟨a_1, ⋯⟩) = x) →
    ∃ (x_1 : x ∈ t), ∃ a_2, (∃ (x : a_2 ∈ a), ⟨a_2, ⋯⟩ ∈ u) ∧ ∃ (x_2 : a_2 ∈ s), e ⟨a_2, ⋯⟩ = ⟨x, ⋯⟩
Tactic:
rintro ⟨hxb, ⟨v, hva, hvu, rfl⟩⟩
State after:
case h.mp.intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hxb : ↑(e ⟨v, ⋯⟩) ∈ b
⊢ ∃ (x : ↑(e ⟨v, ⋯⟩) ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_1 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨↑(e ⟨v, ⋯⟩), ⋯⟩

State before:
case h.mp.intro.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hxb : ↑(e ⟨v, ⋯⟩) ∈ b
⊢ ∃ (x : ↑(e ⟨v, ⋯⟩) ∈ t), ∃ a_1, (∃ (x : a_1 ∈ a), ⟨a_1, ⋯⟩ ∈ u) ∧ ∃ (x_1 : a_1 ∈ s), e ⟨a_1, ⋯⟩ = ⟨↑(e ⟨v, ⋯⟩), ⋯⟩
Tactic:
simp [has hva, hva, hvu]
State after:
no goals

State before:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
a✝ : α✝
b✝ : β✝
s✝ : Set α✝
f : ↑s✝ ↪ β✝
α : Type u_4
β : Type u_5
a s : Set α
b t : Set β
e : ↑s ≃ ↑t
has : a ⊆ s
hbt : b ⊆ t
h_eq : ∀ (x : ↑s), ↑(e x) ∈ b ↔ ↑x ∈ a
u : Set ↑a
x : β
hxt : x ∈ t
v : α
hva : v ∈ a
hvu : ⟨v, ⋯⟩ ∈ u
hvs : v ∈ s
hvx : e ⟨v, ⋯⟩ = ⟨x, ⋯⟩
⊢ ↑(e ⟨v, ⋯⟩) = x
Tactic:
rw [hvx]
State after:
no goals