[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]
