[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = ↑(LocalEquiv.symm e) y
⊢ ↑e x = y
[PROOFSTEP]
rw [← e.right_inv hy, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : ↑e x = y
⊢ x = ↑(LocalEquiv.symm e) y
[PROOFSTEP]
rw [← e.left_inv hx, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : α ≃ β
s : Set α
t : Set β
h : ↑e '' s = t
x : β
hx : x ∈ t
⊢ ↑e.symm x ∈ s
[PROOFSTEP]
subst t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : α ≃ β
s : Set α
x : β
hx : x ∈ ↑e '' s
⊢ ↑e.symm x ∈ s
[PROOFSTEP]
rcases hx with ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : α ≃ β
s : Set α
x : α
hx : x ∈ s
⊢ ↑e.symm (↑e x) ∈ s
[PROOFSTEP]
rwa [e.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : α ≃ β
⊢ ↑e '' univ = univ
[PROOFSTEP]
rw [image_univ, e.surjective.range_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : LocalEquiv α β
f : α → β
hf : ↑e = f
g : β → α
hg : ↑(LocalEquiv.symm e) = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ copy e f hf g hg s hs t ht = e
[PROOFSTEP]
substs f g s t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : LocalEquiv α β
⊢ copy e ↑e (_ : ↑e = ↑e) ↑(LocalEquiv.symm e) (_ : ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e)) e.source
      (_ : e.source = e.source) e.target (_ : e.target = e.target) =
    e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ copy
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
      (_ :
        ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
          ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
      ↑(LocalEquiv.symm
          { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
      (_ :
        ↑(LocalEquiv.symm
              { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
                map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }) =
          ↑(LocalEquiv.symm
              { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
                map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }))
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source
      (_ :
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
          { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source)
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
      (_ :
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target =
          { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target) =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ LocalEquiv.symm (LocalEquiv.symm e) = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e' : LocalEquiv β γ
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ LocalEquiv.symm
      (LocalEquiv.symm
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }) =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
p : β → Prop
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (↑e x)
[PROOFSTEP]
rw [← image_source_eq_target, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
p : β → Prop
⊢ (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)
[PROOFSTEP]
rw [← image_source_eq_target, bex_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
h : IsImage e s t
x : α
hx : x ∈ e.source
⊢ ↑(LocalEquiv.symm e) (↑e x) ∈ s ↔ ↑e x ∈ t
[PROOFSTEP]
rw [e.left_inv hx, h hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
⊢ IsImage e s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
[PROOFSTEP]
simp only [IsImage, ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : IsImage e s t
h' : IsImage e' s t
⊢ LeftInvOn (piecewise t ↑(LocalEquiv.symm e) ↑(LocalEquiv.symm e')) (piecewise s ↑e ↑e') (Set.ite s e.source e'.source)
[PROOFSTEP]
rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : IsImage e s t
h' : IsImage e' s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ piecewise t (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (piecewise s (↑e) (↑e') x) = x
[PROOFSTEP]
rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : IsImage e s t
h' : IsImage e' s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
⊢ piecewise t (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (piecewise s (↑e) (↑e') x) = x
[PROOFSTEP]
rw [piecewise_eq_of_not_mem _ _ _ hs, piecewise_eq_of_not_mem _ _ _ ((h'.compl he).2 hs), e'.left_inv he]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
h' : IsImage e' s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t
[PROOFSTEP]
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (e.target ∩ t)
[PROOFSTEP]
rw [← h.image_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑(LocalEquiv.symm e)) (↑(LocalEquiv.symm e')) (↑e '' (e.source ∩ s))
[PROOFSTEP]
rintro y ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
[PROOFSTEP]
have hx' := hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
[PROOFSTEP]
rw [hs] at hx'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x✝ : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
⊢ ↑(LocalEquiv.symm e) (↑e x) = ↑(LocalEquiv.symm e') (↑e x)
[PROOFSTEP]
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ e.target ↔ x ∈ e.source
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
e' : LocalEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target
[PROOFSTEP]
rw [hs.inter_eq, ht.inter_eq, image_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' s
[PROOFSTEP]
rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' (e.source ∩ s)
[PROOFSTEP]
rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' s
[PROOFSTEP]
rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
x : α
hx : x ∈ e.source
⊢ x ∈ ↑e ⁻¹' (↑(LocalEquiv.symm e) ⁻¹' s) ↔ x ∈ s
[PROOFSTEP]
simp only [mem_preimage, e.left_inv hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
⊢ e = e'
[PROOFSTEP]
have A : (e : α → β) = e' := by
  ext x
  exact h x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
⊢ ↑e = ↑e'
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
x : α
⊢ ↑e x = ↑e' x
[PROOFSTEP]
exact h x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ e = e'
[PROOFSTEP]
have B : (e.symm : β → α) = e'.symm := by
  ext x
  exact hsymm x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e')
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
x : β
⊢ ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
[PROOFSTEP]
exact hsymm x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e')
⊢ e = e'
[PROOFSTEP]
have I : e '' e.source = e.target := e.image_source_eq_target
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e')
I : ↑e '' e.source = e.target
⊢ e = e'
[PROOFSTEP]
have I' : e' '' e'.source = e'.target := e'.image_source_eq_target
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e')
I : ↑e '' e.source = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'
[PROOFSTEP]
rw [A, hs, I'] at I
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑(LocalEquiv.symm e) = ↑(LocalEquiv.symm e')
I : e'.target = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
e' : LocalEquiv α β
I' : ↑e' '' e'.source = e'.target
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
h :
  ∀ (x : α),
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        x =
      ↑e' x
hsymm :
  ∀ (x : β),
    ↑(LocalEquiv.symm
            { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
        x =
      ↑(LocalEquiv.symm e') x
hs :
  { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
    e'.source
A :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    ↑e'
B :
  ↑(LocalEquiv.symm
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }) =
    ↑(LocalEquiv.symm e')
I :
  e'.target =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
⊢ { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    e'
[PROOFSTEP]
cases e'
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
I' :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } ''
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
h :
  ∀ (x : α),
    ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
            map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }
        x =
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        x
hsymm :
  ∀ (x : β),
    ↑(LocalEquiv.symm
            { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹,
              map_source' := map_source'✝¹, map_target' := map_target'✝¹, left_inv' := left_inv'✝¹,
              right_inv' := right_inv'✝¹ })
        x =
      ↑(LocalEquiv.symm
            { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
        x
hs :
  { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.source =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source
A :
  ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ } =
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
B :
  ↑(LocalEquiv.symm
        { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }) =
    ↑(LocalEquiv.symm
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
I :
  { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target =
    { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.target
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
      map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
h : ∀ (x : α), toFun✝¹ x = toFun✝ x
hsymm : ∀ (x : β), invFun✝¹ x = invFun✝ x
hs : source✝¹ = source✝
A : toFun✝¹ = toFun✝
B : invFun✝¹ = invFun✝
I : target✝ = target✝¹
I' : (fun a => toFun✝ a) '' source✝ = target✝
⊢ toFun✝¹ = toFun✝ ∧ invFun✝¹ = invFun✝ ∧ source✝¹ = source✝ ∧ target✝¹ = target✝
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : LocalEquiv α β
s : Set α
h : e.source ⊆ s
⊢ (LocalEquiv.restr e s).source = e.source
[PROOFSTEP]
simp [inter_eq_self_of_subset_left h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ (LocalEquiv.restr (LocalEquiv.refl α) s).source = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ (LocalEquiv.restr (LocalEquiv.refl α) s).target = s
[PROOFSTEP]
change univ ∩ id ⁻¹' s = s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ univ ∩ id ⁻¹' s = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ e' : LocalEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ (↑e' ∘ ↑e) x ∈ e'.target
[PROOFSTEP]
simp [← h, hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ e' : LocalEquiv β γ
h : e.target = e'.source
y : γ
hy : y ∈ e'.target
⊢ (↑(LocalEquiv.symm e) ∘ ↑(LocalEquiv.symm e')) y ∈ e.source
[PROOFSTEP]
simp [h, hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ e' : LocalEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ (↑(LocalEquiv.symm e) ∘ ↑(LocalEquiv.symm e')) ((↑e' ∘ ↑e) x) = x
[PROOFSTEP]
simp [hx, ← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ e' : LocalEquiv β γ
h : e.target = e'.source
y : γ
hy : y ∈ e'.target
⊢ (↑e' ∘ ↑e) ((↑(LocalEquiv.symm e) ∘ ↑(LocalEquiv.symm e')) y) = y
[PROOFSTEP]
simp [hy, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ LocalEquiv.symm (LocalEquiv.trans e e') = LocalEquiv.trans (LocalEquiv.symm e') (LocalEquiv.symm e)
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e' : LocalEquiv β γ
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ LocalEquiv.symm
      (LocalEquiv.trans
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        e') =
    LocalEquiv.trans (LocalEquiv.symm e')
      (LocalEquiv.symm
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
[PROOFSTEP]
cases e'
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : β → γ
invFun✝ : γ → β
source✝ : Set β
target✝ : Set γ
map_source'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : β⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : γ⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ LocalEquiv.symm
      (LocalEquiv.trans
        { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }) =
    LocalEquiv.trans
      (LocalEquiv.symm
        { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ })
      (LocalEquiv.symm
        { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ })
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
[PROOFSTEP]
mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e e').source = ↑(LocalEquiv.symm e) '' (e.target ∩ e'.source)
[PROOFSTEP]
rw [e.trans_source', e.symm_image_target_inter_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
e'' : LocalEquiv γ δ
⊢ (LocalEquiv.trans (LocalEquiv.trans e e') e'').source = (LocalEquiv.trans e (LocalEquiv.trans e' e'')).source
[PROOFSTEP]
simp [trans_source, @preimage_comp α β γ, inter_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e (LocalEquiv.refl β)).source = e.source
[PROOFSTEP]
simp [trans_source]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans (LocalEquiv.refl α) e).source = e.source
[PROOFSTEP]
simp [trans_source, preimage_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ (LocalEquiv.trans e (LocalEquiv.restr (LocalEquiv.refl β) s)).source = (LocalEquiv.restr e (↑e ⁻¹' s)).source
[PROOFSTEP]
simp [trans_source]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ (LocalEquiv.trans e (LocalEquiv.restr (LocalEquiv.refl β) s)).source =
    (LocalEquiv.restr e (e.source ∩ ↑e ⁻¹' s)).source
[PROOFSTEP]
simp [trans_source]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)
[PROOFSTEP]
rw [← inter_assoc, inter_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ (LocalEquiv.trans (LocalEquiv.restr e s) e').source = (LocalEquiv.restr (LocalEquiv.trans e e') s).source
[PROOFSTEP]
simp [trans_source, inter_comm, inter_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
e' : LocalEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑(LocalEquiv.symm (LocalEquiv.symm (LocalEquiv.symm e))) ⁻¹' e'.source
[PROOFSTEP]
rwa [mem_preimage, LocalEquiv.symm_symm, e.left_inv he]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ Equivalence EqOnSource
[PROOFSTEP]
constructor
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ (x : LocalEquiv α β), EqOnSource x x
[PROOFSTEP]
simp only [Equivalence, EqOnSource, EqOn]
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ {x y : LocalEquiv α β}, EqOnSource x y → EqOnSource y x
[PROOFSTEP]
simp only [Equivalence, EqOnSource, EqOn]
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ {x y z : LocalEquiv α β}, EqOnSource x y → EqOnSource y z → EqOnSource x z
[PROOFSTEP]
simp only [Equivalence, EqOnSource, EqOn]
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ (x : LocalEquiv α β), True ∧ ∀ ⦃x_1 : α⦄, x_1 ∈ x.source → True
[PROOFSTEP]
aesop
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ {x y : LocalEquiv α β},
    (x.source = y.source ∧ ∀ ⦃x_1 : α⦄, x_1 ∈ x.source → ↑x x_1 = ↑y x_1) →
      y.source = x.source ∧ ∀ ⦃x_1 : α⦄, x_1 ∈ y.source → ↑y x_1 = ↑x x_1
[PROOFSTEP]
aesop
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ ∀ {x y z : LocalEquiv α β},
    (x.source = y.source ∧ ∀ ⦃x_1 : α⦄, x_1 ∈ x.source → ↑x x_1 = ↑y x_1) →
      (y.source = z.source ∧ ∀ ⦃x : α⦄, x ∈ y.source → ↑y x = ↑z x) →
        x.source = z.source ∧ ∀ ⦃x_1 : α⦄, x_1 ∈ x.source → ↑x x_1 = ↑z x_1
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ e.target = e'.target
[PROOFSTEP]
simp only [← image_source_eq_target, ← source_eq h, h.2.image_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ LocalEquiv.symm e ≈ LocalEquiv.symm e'
[PROOFSTEP]
refine' ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn _ _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑(LocalEquiv.symm e')) (↑e) (LocalEquiv.symm e).source
[PROOFSTEP]
simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ MapsTo (↑(LocalEquiv.symm e')) (LocalEquiv.symm e).source e.source
[PROOFSTEP]
simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑(LocalEquiv.symm e')) (↑e) e'.target
[PROOFSTEP]
exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ LocalEquiv.trans e f ≈ LocalEquiv.trans e' f'
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (LocalEquiv.trans e f).source = (LocalEquiv.trans e' f').source
[PROOFSTEP]
rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑(LocalEquiv.symm e) '' (e.target ∩ f.source) = ↑(LocalEquiv.symm e') '' (e.target ∩ f.source)
[PROOFSTEP]
exact (he.symm'.eqOn.mono <| inter_subset_left _ _).image_eq
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(LocalEquiv.trans e f)) (↑(LocalEquiv.trans e' f')) (LocalEquiv.trans e f).source
[PROOFSTEP]
intro x hx
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (LocalEquiv.trans e f).source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
[PROOFSTEP]
rw [trans_source] at hx
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
f f' : LocalEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ ↑e ⁻¹' f.source
⊢ ↑(LocalEquiv.trans e f) x = ↑(LocalEquiv.trans e' f') x
[PROOFSTEP]
simp [Function.comp_apply, LocalEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set α
⊢ LocalEquiv.restr e s ≈ LocalEquiv.restr e' s
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set α
⊢ (LocalEquiv.restr e s).source = (LocalEquiv.restr e' s).source
[PROOFSTEP]
simp [he.1]
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(LocalEquiv.restr e s)) (↑(LocalEquiv.restr e' s)) (LocalEquiv.restr e s).source
[PROOFSTEP]
intro x hx
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (LocalEquiv.restr e s).source
⊢ ↑(LocalEquiv.restr e s) x = ↑(LocalEquiv.restr e' s) x
[PROOFSTEP]
simp only [mem_inter_iff, restr_source] at hx
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ e.source ∧ x ∈ s
⊢ ↑(LocalEquiv.restr e s) x = ↑(LocalEquiv.restr e' s) x
[PROOFSTEP]
exact he.2 hx.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
[PROOFSTEP]
rw [he.eqOn.inter_preimage_eq, source_eq he]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ LocalEquiv.trans e (LocalEquiv.symm e) ≈ ofSet e.source
[PROOFSTEP]
have A : (e.trans e.symm).source = e.source := by mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
[PROOFSTEP]
mfld_set_tac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
⊢ LocalEquiv.trans e (LocalEquiv.symm e) ≈ ofSet e.source
[PROOFSTEP]
refine' ⟨by rw [A, ofSet_source], fun x hx => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
⊢ (LocalEquiv.trans e (LocalEquiv.symm e)).source = (ofSet e.source).source
[PROOFSTEP]
rw [A, ofSet_source]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ (LocalEquiv.trans e (LocalEquiv.symm e)).source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
[PROOFSTEP]
rw [A] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
A : (LocalEquiv.trans e (LocalEquiv.symm e)).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(LocalEquiv.trans e (LocalEquiv.symm e)) x = ↑(ofSet e.source) x
[PROOFSTEP]
simp only [hx, mfld_simps]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'
[PROOFSTEP]
refine LocalEquiv.ext (fun x => ?_) (fun x => ?_) h.1
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x
[PROOFSTEP]
apply h.2
[GOAL]
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source
[PROOFSTEP]
rw [s]
[GOAL]
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑(LocalEquiv.symm e) x = ↑(LocalEquiv.symm e') x
[PROOFSTEP]
apply h.symm'.2
[GOAL]
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ (LocalEquiv.symm e).source
[PROOFSTEP]
rw [symm_source, t]
[GOAL]
case refine_2.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ x ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ (fun p => (↑e p.fst, ↑e' p.snd)) p ∈ e.target ×ˢ e'.target
[PROOFSTEP]
simp at hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : α × γ
hp : p.fst ∈ e.source ∧ p.snd ∈ e'.source
⊢ (fun p => (↑e p.fst, ↑e' p.snd)) p ∈ e.target ×ˢ e'.target
[PROOFSTEP]
simp [hp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ (fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) p ∈ e.source ×ˢ e'.source
[PROOFSTEP]
simp at hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : β × δ
hp : p.fst ∈ e.target ∧ p.snd ∈ e'.target
⊢ (fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) p ∈ e.source ×ˢ e'.source
[PROOFSTEP]
simp [map_target, hp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ (fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) ((fun p => (↑e p.fst, ↑e' p.snd)) p) = p
[PROOFSTEP]
simp at hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : α × γ
hp : p.fst ∈ e.source ∧ p.snd ∈ e'.source
⊢ (fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) ((fun p => (↑e p.fst, ↑e' p.snd)) p) = p
[PROOFSTEP]
simp [hp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ (fun p => (↑e p.fst, ↑e' p.snd)) ((fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) p) = p
[PROOFSTEP]
simp at hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
p : β × δ
hp : p.fst ∈ e.target ∧ p.snd ∈ e'.target
⊢ (fun p => (↑e p.fst, ↑e' p.snd)) ((fun p => (↑(LocalEquiv.symm e) p.fst, ↑(LocalEquiv.symm e') p.snd)) p) = p
[PROOFSTEP]
simp [hp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
⊢ LocalEquiv.symm (prod e e') = prod (LocalEquiv.symm e) (LocalEquiv.symm e')
[PROOFSTEP]
ext x
[GOAL]
case h.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
x : β × δ
⊢ (↑(LocalEquiv.symm (prod e e')) x).fst = (↑(prod (LocalEquiv.symm e) (LocalEquiv.symm e')) x).fst
[PROOFSTEP]
simp [prod_coe_symm]
[GOAL]
case h.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
x : β × δ
⊢ (↑(LocalEquiv.symm (prod e e')) x).snd = (↑(prod (LocalEquiv.symm e) (LocalEquiv.symm e')) x).snd
[PROOFSTEP]
simp [prod_coe_symm]
[GOAL]
case hsymm.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
x : α × γ
⊢ (↑(LocalEquiv.symm (LocalEquiv.symm (prod e e'))) x).fst =
    (↑(LocalEquiv.symm (prod (LocalEquiv.symm e) (LocalEquiv.symm e'))) x).fst
[PROOFSTEP]
simp [prod_coe_symm]
[GOAL]
case hsymm.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
x : α × γ
⊢ (↑(LocalEquiv.symm (LocalEquiv.symm (prod e e'))) x).snd =
    (↑(LocalEquiv.symm (prod (LocalEquiv.symm e) (LocalEquiv.symm e'))) x).snd
[PROOFSTEP]
simp [prod_coe_symm]
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e : LocalEquiv α β
e' : LocalEquiv γ δ
x : β × δ
⊢ x ∈ (LocalEquiv.symm (prod e e')).source ↔ x ∈ (prod (LocalEquiv.symm e) (LocalEquiv.symm e')).source
[PROOFSTEP]
simp [prod_coe_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ prod (LocalEquiv.refl α) (LocalEquiv.refl β) = LocalEquiv.refl (α × β)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
⊢ (↑(prod (LocalEquiv.refl α) (LocalEquiv.refl β)) (x, y)).fst = (↑(LocalEquiv.refl (α × β)) (x, y)).fst
[PROOFSTEP]
simp
[GOAL]
case h.mk.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
⊢ (↑(prod (LocalEquiv.refl α) (LocalEquiv.refl β)) (x, y)).snd = (↑(LocalEquiv.refl (α × β)) (x, y)).snd
[PROOFSTEP]
simp
[GOAL]
case hsymm.mk.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
⊢ (↑(LocalEquiv.symm (prod (LocalEquiv.refl α) (LocalEquiv.refl β))) (x, y)).fst =
    (↑(LocalEquiv.symm (LocalEquiv.refl (α × β))) (x, y)).fst
[PROOFSTEP]
simp
[GOAL]
case hsymm.mk.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
⊢ (↑(LocalEquiv.symm (prod (LocalEquiv.refl α) (LocalEquiv.refl β))) (x, y)).snd =
    (↑(LocalEquiv.symm (LocalEquiv.refl (α × β))) (x, y)).snd
[PROOFSTEP]
simp
[GOAL]
case hs.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
x : α
y : β
⊢ (x, y) ∈ (prod (LocalEquiv.refl α) (LocalEquiv.refl β)).source ↔ (x, y) ∈ (LocalEquiv.refl (α × β)).source
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
⊢ LocalEquiv.trans (prod e e') (prod f f') = prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f')
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (↑(LocalEquiv.trans (prod e e') (prod f f')) (x, y)).fst =
    (↑(prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f')) (x, y)).fst
[PROOFSTEP]
simp [ext_iff]
[GOAL]
case h.mk.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (↑(LocalEquiv.trans (prod e e') (prod f f')) (x, y)).snd =
    (↑(prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f')) (x, y)).snd
[PROOFSTEP]
simp [ext_iff]
[GOAL]
case hsymm.mk.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : γ
y : ε
⊢ (↑(LocalEquiv.symm (LocalEquiv.trans (prod e e') (prod f f'))) (x, y)).fst =
    (↑(LocalEquiv.symm (prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f'))) (x, y)).fst
[PROOFSTEP]
simp [ext_iff]
[GOAL]
case hsymm.mk.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : γ
y : ε
⊢ (↑(LocalEquiv.symm (LocalEquiv.trans (prod e e') (prod f f'))) (x, y)).snd =
    (↑(LocalEquiv.symm (prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f'))) (x, y)).snd
[PROOFSTEP]
simp [ext_iff]
[GOAL]
case hs.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (x, y) ∈ (LocalEquiv.trans (prod e e') (prod f f')).source ↔
    (x, y) ∈ (prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f')).source
[PROOFSTEP]
simp [ext_iff]
[GOAL]
case hs.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_5
ε : Type u_6
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
⊢ (LocalEquiv.pi fun i => LocalEquiv.refl (αi i)) = LocalEquiv.refl ((i : ι) → αi i)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(LocalEquiv.pi fun i => LocalEquiv.refl (αi i)) x✝¹ x✝ = ↑(LocalEquiv.refl ((i : ι) → αi i)) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
case hsymm.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(LocalEquiv.symm (LocalEquiv.pi fun i => LocalEquiv.refl (αi i))) x✝¹ x✝ =
    ↑(LocalEquiv.symm (LocalEquiv.refl ((i : ι) → αi i))) x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (LocalEquiv.pi fun i => LocalEquiv.refl (αi i)).source ↔ x✝ ∈ (LocalEquiv.refl ((i : ι) → αi i)).source
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → LocalEquiv (αi i) (βi i)
ei' : (i : ι) → LocalEquiv (βi i) (γi i)
⊢ LocalEquiv.trans (LocalEquiv.pi ei) (LocalEquiv.pi ei') = LocalEquiv.pi fun i => LocalEquiv.trans (ei i) (ei' i)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → LocalEquiv (αi i) (βi i)
ei' : (i : ι) → LocalEquiv (βi i) (γi i)
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(LocalEquiv.trans (LocalEquiv.pi ei) (LocalEquiv.pi ei')) x✝¹ x✝ =
    ↑(LocalEquiv.pi fun i => LocalEquiv.trans (ei i) (ei' i)) x✝¹ x✝
[PROOFSTEP]
simp [forall_and]
[GOAL]
case hsymm.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → LocalEquiv (αi i) (βi i)
ei' : (i : ι) → LocalEquiv (βi i) (γi i)
x✝¹ : (i : ι) → γi i
x✝ : ι
⊢ ↑(LocalEquiv.symm (LocalEquiv.trans (LocalEquiv.pi ei) (LocalEquiv.pi ei'))) x✝¹ x✝ =
    ↑(LocalEquiv.symm (LocalEquiv.pi fun i => LocalEquiv.trans (ei i) (ei' i))) x✝¹ x✝
[PROOFSTEP]
simp [forall_and]
[GOAL]
case hs.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : LocalEquiv α β
e' : LocalEquiv β γ
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → LocalEquiv (αi i) (βi i)
ei' : (i : ι) → LocalEquiv (βi i) (γi i)
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (LocalEquiv.trans (LocalEquiv.pi ei) (LocalEquiv.pi ei')).source ↔
    x✝ ∈ (LocalEquiv.pi fun i => LocalEquiv.trans (ei i) (ei' i)).source
[PROOFSTEP]
simp [forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
e' : β ≃ γ
⊢ (toLocalEquiv (e.trans e')).source = (LocalEquiv.trans (toLocalEquiv e) (toLocalEquiv e')).source
[PROOFSTEP]
simp [LocalEquiv.trans_source, Equiv.toLocalEquiv]


[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ↑e.symm '' t ⊆ s ↔ t ⊆ ↑e '' s
[PROOFSTEP]
rw [image_subset_iff, e.image_eq_preimage]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ s ⊆ ↑e.symm '' t ↔ ↑e.symm.symm '' s ⊆ t
[PROOFSTEP]
rw [e.symm.subset_image]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ↑e.symm.symm '' s ⊆ t ↔ ↑e '' s ⊆ t
[PROOFSTEP]
rw [e.symm_symm]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ↑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
[PROOFSTEP]
simpa only [Equiv.image_eq_preimage] using prod_assoc_symm_preimage
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ↑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
[PROOFSTEP]
simpa only [Equiv.image_eq_preimage] using prod_assoc_preimage
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
s : Set (α × β)
x : ↑s
⊢ (↑x).snd ∈ {y | ((↑x).fst, y) ∈ s}
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : ↑s
⊢ ↑e ↑x ∈ ↑e '' s
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
y : ↑(↑e '' s)
⊢ ↑e.symm ↑y ∈ s
[PROOFSTEP]
rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ ↑e.symm ↑{ val := ↑e a, property := (_ : ∃ a_1, a_1 ∈ s ∧ ↑e a_1 = ↑e a) } ∈ s
[PROOFSTEP]
simpa using m
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : ↑s
⊢ (fun y => { val := ↑e.symm ↑y, property := (_ : ↑e.symm ↑y ∈ s) })
      ((fun x => { val := ↑e ↑x, property := (_ : ↑e ↑x ∈ ↑e '' s) }) x) =
    x
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
y : ↑(↑e '' s)
⊢ (fun x => { val := ↑e ↑x, property := (_ : ↑e ↑x ∈ ↑e '' s) })
      ((fun y => { val := ↑e.symm ↑y, property := (_ : ↑e.symm ↑y ∈ s) }) y) =
    y
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun o =>
        match o with
        | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
        | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
      ((fun x =>
          if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
          else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
        { val := x, property := h' }) =
    { val := x, property := h' }
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : ↑s ⊕ ↑t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        o) =
    o
[PROOFSTEP]
rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : ↑s ⊕ ↑t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        o) =
    o
[PROOFSTEP]
rcases o with (⟨x, h⟩ | ⟨x, h⟩)
[GOAL]
case inl.mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ s
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        (Sum.inl { val := x, property := h })) =
    Sum.inl { val := x, property := h }
[PROOFSTEP]
simp [hs _ h]
[GOAL]
case inr.mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.13643
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ t
⊢ (fun x =>
        if hp : p ↑x then Sum.inl { val := ↑x, property := (_ : ↑x ∈ s) }
        else Sum.inr { val := ↑x, property := (_ : ↑x ∈ t) })
      ((fun o =>
          match o with
          | Sum.inl x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) }
          | Sum.inr x => { val := ↑x, property := (_ : ↑x ∈ s ∨ ↑x ∈ t) })
        (Sum.inr { val := x, property := h })) =
    Sum.inr { val := x, property := h }
[PROOFSTEP]
simp [ht _ h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
x : α
h : x ∈ {a}
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := x, property := h }) =
    { val := x, property := h }
[PROOFSTEP]
simp at h
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
x : α
h✝ : x ∈ {a}
h : x = a
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := x, property := h✝ }) =
    { val := x, property := h✝ }
[PROOFSTEP]
subst x
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20174
a : α
x✝ : ↑{a}
h : a = a
⊢ (fun x => { val := a, property := (_ : a ∈ {a}) }) ((fun x => PUnit.unit) { val := a, property := (_ : a = a) }) =
    { val := a, property := (_ : a = a) }
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
H : ¬a ∈ s
⊢ insert a s = s ∪ {a}
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
H : ¬a ∈ s
x : α
x✝ : x ∈ s ∩ {a}
hx : x ∈ s
right✝ : x ∈ {a}
⊢ x ∈ ∅
[PROOFSTEP]
simp_all
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.24478
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.24478
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∪ sᶜ = univ
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
[PROOFSTEP]
have : ((⟨x, Or.inl hx⟩ : (s ∪ sᶜ : Set α)) : α) ∈ s := hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inl { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.Set.sumCompl]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inl { val := x, property := hx }
[PROOFSTEP]
simpa using Set.union_apply_left (by simp) this
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ s
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
⊢ ↑(Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }
[PROOFSTEP]
have : ((⟨x, Or.inr hx⟩ : (s ∪ sᶜ : Set α)) : α) ∈ sᶜ := hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm x = Sum.inr { val := x, property := hx }
[PROOFSTEP]
rw [Equiv.Set.sumCompl]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ ↑(Trans.trans (Trans.trans (Set.union (_ : s ∩ sᶜ ⊆ ∅)).symm (Set.ofEq (_ : s ∪ sᶜ = univ))) (Set.univ α)).symm x =
    Sum.inr { val := x, property := hx }
[PROOFSTEP]
simpa using Set.union_apply_right (by simp) this
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : ¬x ∈ s
this : ↑{ val := x, property := (_ : x ∈ s ∨ x ∈ sᶜ) } ∈ sᶜ
⊢ s ∩ sᶜ ⊆ ∅
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ ↑(Set.sumCompl s).symm ↑x = Sum.inl x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ s
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inl { val := x, property := hx }
[PROOFSTEP]
exact Set.sumCompl_symm_apply_of_mem hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : ↑sᶜ
⊢ ↑(Set.sumCompl s).symm ↑x = Sum.inr x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∈ sᶜ
⊢ ↑(Set.sumCompl s).symm ↑{ val := x, property := hx } = Sum.inr { val := x, property := hx }
[PROOFSTEP]
exact Set.sumCompl_symm_apply_of_not_mem hx
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.32810
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∩ (t \ s) ⊆ ∅
[PROOFSTEP]
simp [inter_diff_self]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.32810
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
⊢ s ∪ t \ s = t
[PROOFSTEP]
simp [union_diff_self, union_eq_self_of_subset_left h]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h).symm x = Sum.inl { val := ↑x, property := hx }
[PROOFSTEP]
apply (Equiv.Set.sumDiffSubset h).injective
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inl { val := ↑x, property := hx })
[PROOFSTEP]
simp only [apply_symm_apply, sumDiffSubset_apply_inl]
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ x = inclusion h { val := ↑x, property := hx }
[PROOFSTEP]
exact Subtype.eq rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ ↑(Set.sumDiffSubset h).symm x = Sum.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
[PROOFSTEP]
apply (Equiv.Set.sumDiffSubset h).injective
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ ↑(Set.sumDiffSubset h) (↑(Set.sumDiffSubset h).symm x) =
    ↑(Set.sumDiffSubset h) (Sum.inr { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) })
[PROOFSTEP]
simp only [apply_symm_apply, sumDiffSubset_apply_inr]
[GOAL]
case a
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x => x ∈ s
x : ↑t
hx : ¬↑x ∈ s
⊢ x = inclusion (_ : t \ s ⊆ t) { val := ↑x, property := (_ : ↑x ∈ t ∧ ¬↑x ∈ s) }
[PROOFSTEP]
exact Subtype.eq rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑(s ∪ t \ s) ⊕ ↑(s ∩ t)
[PROOFSTEP]
rw [union_diff_self]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑(t \ s) ⊕ ↑(s ∩ t) ≃ ↑(t \ s ∪ s ∩ t)
[PROOFSTEP]
refine' (Set.union' (· ∉ s) _ _).symm
[GOAL]
case refine'_1
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : α), x ∈ t \ s → (fun x => ¬x ∈ s) x
case refine'_2
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ∀ (x : α), x ∈ s ∩ t → ¬(fun x => ¬x ∈ s) x
[PROOFSTEP]
exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t
[PROOFSTEP]
{ rw [(_ : t \ s ∪ s ∩ t = t)]
  rw [union_comm, inter_comm, inter_union_diff]
}
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t
[PROOFSTEP]
rw [(_ : t \ s ∪ s ∩ t = t)]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ t \ s ∪ s ∩ t = t
[PROOFSTEP]
rw [union_comm, inter_comm, inter_union_diff]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e₁ : ↑sᶜ ≃ ↑tᶜ
x : ↑s
⊢ ↑(Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t)) ↑x = ↑(↑e₀ x)
[PROOFSTEP]
simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl, Set.sumCompl_symm_apply, Trans.trans]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
⊢ (fun e₁ =>
        { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
          property := (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
      ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e) =
    e
[PROOFSTEP]
ext x
[GOAL]
case a.H
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
hx : x ∈ s
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply, trans_apply,
  Subtype.coe_mk, Set.sumCompl_apply_inl, Trans.trans]
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : { e // ∀ (x : ↑s), ↑e ↑x = ↑(↑e₀ x) }
x : α
hx : ¬x ∈ s
⊢ ↑↑((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            ((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t)) e))
      x =
    ↑↑e x
[PROOFSTEP]
simp only [Set.sumCompl_symm_apply_of_not_mem hx, Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, trans_apply,
  sumCongr_apply, Subtype.coe_mk, Trans.trans]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u
β : Type v
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e₀ : ↑s ≃ ↑t
e : ↑sᶜ ≃ ↑tᶜ
x : { a // a ∈ sᶜ }
⊢ ↑((fun e => subtypeEquiv ↑e (_ : ∀ (a : α), ¬a ∈ s ↔ ¬↑↑e a ∈ t))
          ((fun e₁ =>
              { val := Trans.trans (Trans.trans (Set.sumCompl s).symm (sumCongr e₀ e₁)) (Set.sumCompl t),
                property :=
                  (_ : ∀ (x : ↑s), ↑(Set.sumCompl t) (↑(sumCongr e₀ e₁) (↑(Set.sumCompl s).symm ↑x)) = ↑(↑e₀ x)) })
            e))
      x =
    ↑e x
[PROOFSTEP]
simp only [Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, Function.comp_apply, sumCongr_apply,
  Equiv.coe_trans, Subtype.coe_eta, Subtype.coe_mk, Trans.trans, Set.sumCompl_symm_apply_compl]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
x✝ : ↑(pi univ s)
f : (i : α) → β i
hf : f ∈ pi univ s
⊢ (fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) })
      ((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) }) { val := f, property := hf }) =
    { val := f, property := hf }
[PROOFSTEP]
ext a
[GOAL]
case a.h
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
x✝ : ↑(pi univ s)
f : (i : α) → β i
hf : f ∈ pi univ s
a : α
⊢ ↑((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) })
          ((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) }) { val := f, property := hf }))
      a =
    ↑{ val := f, property := hf } a
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
f : (a : α) → ↑(s a)
⊢ (fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) })
      ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) }) f) =
    f
[PROOFSTEP]
ext a
[GOAL]
case h.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
s : (a : α) → Set (β a)
f : (a : α) → ↑(s a)
a : α
⊢ ↑((fun f a => { val := ↑f a, property := (_ : ↑f a ∈ s a) })
        ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), a ∈ univ → ↑(f a) ∈ s a) }) f) a) =
    ↑(f a)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
x : α
h : x ∈ s
⊢ ↑(Set.image f s H).symm { val := f x, property := (_ : ∃ a, a ∈ s ∧ f a = f x) } = { val := x, property := h }
[PROOFSTEP]
apply (Set.image f s H).injective
[GOAL]
case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
x : α
h : x ∈ s
⊢ ↑(Set.image f s H) (↑(Set.image f s H).symm { val := f x, property := (_ : ∃ a, a ∈ s ∧ f a = f x) }) =
    ↑(Set.image f s H) { val := x, property := h }
[PROOFSTEP]
simp [(Set.image f s H).apply_symm_apply]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
ext ⟨b, a, has, rfl⟩
[GOAL]
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
have : ∀ h : ∃ a', a' ∈ s ∧ a' = a, Classical.choose h = a := fun h => (Classical.choose_spec h).2
[GOAL]
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
this : ∀ (h : ∃ a', a' ∈ s ∧ a' = a), Classical.choose h = a
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
[PROOFSTEP]
simp [Equiv.Set.image, Equiv.Set.imageOfInjOn, hf.eq_iff, this]
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
⊢ Subtype.val '' x ∈ 𝒫 S
[PROOFSTEP]
rintro _ ⟨a : S, _, rfl⟩
[GOAL]
case intro.intro
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
a : ↑S
left✝ : a ∈ x
⊢ ↑a ∈ S
[PROOFSTEP]
exact a.2
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : ↑(𝒫 S)
⊢ (fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) })
      ((fun x => Subtype.val ⁻¹' ↑x) x) =
    x
[PROOFSTEP]
ext y
[GOAL]
case a.h
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : ↑(𝒫 S)
y : α
⊢ y ∈
      ↑((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) })
          ((fun x => Subtype.val ⁻¹' ↑x) x)) ↔
    y ∈ ↑x
[PROOFSTEP]
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
⊢ (fun x => Subtype.val ⁻¹' ↑x)
      ((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) }) x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.53602
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈
      (fun x => Subtype.val ⁻¹' ↑x)
        ((fun x => { val := Subtype.val '' x, property := (_ : ∀ ⦃a : α⦄, a ∈ Subtype.val '' x → a ∈ S) }) x) ↔
    x✝ ∈ x
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ f ↑x ∈ range f
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s
[PROOFSTEP]
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ { val := f ↑{ val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) },
      property :=
        (_ :
          f ↑{ val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) } ∈
            range f) } ∈
    s
[PROOFSTEP]
simpa [apply_rangeSplitting f] using m
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ (fun x => { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
      ((fun x =>
          { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
            property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
        x) =
    x
[PROOFSTEP]
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
y : ↑(range f)
m : y ∈ s
⊢ (fun x => { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
      ((fun x =>
          { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
            property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
        { val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) }) =
    { val := rangeSplitting f y, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f y) }
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
s : Set ↑(range f)
x : ↑s
⊢ (fun x =>
        { val := { val := f ↑x, property := (_ : f ↑x ∈ range f) },
          property := (_ : { val := f ↑x, property := (_ : f ↑x ∈ range f) } ∈ s) })
      ((fun x =>
          { val := rangeSplitting f ↑x, property := (_ : ∃ a, a ∈ s ∧ rangeSplitting f a = rangeSplitting f ↑x) })
        x) =
    x
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : β
h : Sum.inr val✝ ∈ range Sum.inl
⊢ False
[PROOFSTEP]
rcases h with ⟨x, h'⟩
[GOAL]
case intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : α
h : Sum.inl val✝ ∈ range Sum.inr
⊢ False
[PROOFSTEP]
rcases h with ⟨x, h'⟩
[GOAL]
case intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False
[PROOFSTEP]
cases h'
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) } = a
[PROOFSTEP]
apply (ofInjective f hf).injective
[GOAL]
case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf) (↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) }) =
    ↑(ofInjective f hf) a
[PROOFSTEP]
simp [apply_ofInjective_symm hf]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ ↑(ofInjective f hf).symm = rangeSplitting f
[PROOFSTEP]
ext ⟨y, x, rfl⟩
[GOAL]
case h.mk.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ ↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) } =
    rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) }
[PROOFSTEP]
apply hf
[GOAL]
case h.mk.intro.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f (↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) }) =
    f (rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) })
[PROOFSTEP]
simp [apply_rangeSplitting f]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f (_ : Injective f)
[PROOFSTEP]
ext
[GOAL]
case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑(↑(ofLeftInverse f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f (_ : Injective f)
[PROOFSTEP]
ext
[GOAL]
case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑(↑(ofLeftInverse' f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
⊢ ↑(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s = (pi univ fun i => s ↑i) ×ˢ pi univ fun i => s ↑i
[PROOFSTEP]
ext ⟨f, g⟩
[GOAL]
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ↑(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s ↔ (f, g) ∈ (pi univ fun i => s ↑i) ×ˢ pi univ fun i => s ↑i
[PROOFSTEP]
simp only [mem_preimage, mem_univ_pi, prod_mk_mem_set_prod_eq, Subtype.forall, ← forall_and]
[GOAL]
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f { val := x, property := b } ∈ s x) ∧ ∀ (b : ¬p x), g { val := x, property := b } ∈ s x
[PROOFSTEP]
refine' forall_congr' fun i => _
[GOAL]
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
[PROOFSTEP]
dsimp only [Subtype.coe_mk]
  -- Porting note: Two lines below were `by_cases hi <;> simp [hi]`
    -- This regression is https://github.com/leanprover/lean4/issues/1926
[GOAL]
case h.mk
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
[PROOFSTEP]
by_cases hi : p i
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
[PROOFSTEP]
simp [forall_prop_of_true hi, forall_prop_of_false (not_not.2 hi), hi]
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : α → Type u_2
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
hi : ¬p i
⊢ ↑(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔
    (∀ (b : p i), f { val := i, property := b } ∈ s i) ∧ ∀ (b : ¬p i), g { val := i, property := b } ∈ s i
[PROOFSTEP]
simp [forall_prop_of_false hi, hi, forall_prop_of_true hi]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
⊢ (fun i => if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
by_cases h : p i
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
rw [dif_pos h, Function.update_apply_equiv_apply, Equiv.symm_symm, Function.update_apply, Function.update_apply,
  dif_pos h]
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
[PROOFSTEP]
have h_coe : (⟨i, h⟩ : Subtype p) = e j ↔ i = e j := Subtype.ext_iff.trans (by rw [Subtype.coe_mk])
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ ↑{ val := i, property := h } = ↑(↑e j) ↔ i = ↑(↑e j)
[PROOFSTEP]
rw [Subtype.coe_mk]
[GOAL]
case pos
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
h_coe : { val := i, property := h } = ↑e j ↔ i = ↑(↑e j)
⊢ (if { val := i, property := h } = ↑e j then x else (v ∘ ↑e.symm) { val := i, property := h }) =
    if i = ↑(↑e j) then x else v (↑e.symm { val := i, property := h })
[PROOFSTEP]
simp [h_coe]
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
have : i ≠ e j := by
  contrapose! h
  have : p (e j : α) := (e j).2
  rwa [← h] at this
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
⊢ i ≠ ↑(↑e j)
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(↑e j)
⊢ p i
[PROOFSTEP]
have : p (e j : α) := (e j).2
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : i = ↑(↑e j)
this : p ↑(↑e j)
⊢ p i
[PROOFSTEP]
rwa [← h] at this
[GOAL]
case neg
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α : Type u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
e : β ≃ Subtype p
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : ¬p i
this : i ≠ ↑(↑e j)
⊢ (if h : p i then update v j x (↑e.symm { val := i, property := h }) else w i) =
    update (fun i => if h : p i then v (↑e.symm { val := i, property := h }) else w i) (↑(↑e j)) x i
[PROOFSTEP]
simp [h, this]