/-
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel

! This file was ported from Lean 3 source module logic.equiv.local_equiv
! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Function
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Equiv.MfldSimpsAttr
import Mathlib.Tactic.Core

/-!
# Local equivalences

This files defines equivalences between subsets of given types.
An element `e` of `LocalEquiv α β` is made of two maps `e.toFun` and `e.invFun` respectively
from α to β and from  β to α (just like equivs), which are inverse to each other on the subsets
`e.source` and `e.target` of respectively α and β.

They are designed in particular to define charts on manifolds.

The main functionality is `e.trans f`, which composes the two local equivalences by restricting
the source and target to the maximal set where the composition makes sense.

As for equivs, we register a coercion to functions and use it in our simp normal form: we write
`e x` and `e.symm y` instead of `e.toFun x` and `e.invFun y`.

## Main definitions

`Equiv.toLocalEquiv`: associating a local equiv to an equiv, with source = target = univ
`LocalEquiv.symm`    : the inverse of a local equiv
`LocalEquiv.trans`   : the composition of two local equivs
`LocalEquiv.refl`    : the identity local equiv
`LocalEquiv.ofSet`  : the identity on a set `s`
`EqOnSource`        : equivalence relation describing the "right" notion of equality for local
                        equivs (see below in implementation notes)

## Implementation notes

There are at least three possible implementations of local equivalences:
* equivs on subtypes
* pairs of functions taking values in `Option α` and `Option β`, equal to none where the local
equivalence is not defined
* pairs of functions defined everywhere, keeping the source and target as additional data

Each of these implementations has pros and cons.
* When dealing with subtypes, one still need to define additional API for composition and
restriction of domains. Checking that one always belongs to the right subtype makes things very
tedious, and leads quickly to DTT hell (as the subtype `u ∩ v` is not the "same" as `v ∩ u`, for
instance).
* With option-valued functions, the composition is very neat (it is just the usual composition, and
the domain is restricted automatically). These are implemented in `PEquiv.lean`. For manifolds,
where one wants to discuss thoroughly the smoothness of the maps, this creates however a lot of
overhead as one would need to extend all classes of smoothness to option-valued maps.
* The `LocalEquiv` version as explained above is easier to use for manifolds. The drawback is that
there is extra useless data (the values of `toFun` and `invFun` outside of `source` and `target`).
In particular, the equality notion between local equivs is not "the right one", i.e., coinciding
source and target and equality there. Moreover, there are no local equivs in this sense between
an empty type and a nonempty type. Since empty types are not that useful, and since one almost never
needs to talk about equal local equivs, this is not an issue in practice.
Still, we introduce an equivalence relation `EqOnSource` that captures this right notion of
equality, and show that many properties are invariant under this equivalence relation.

### Local coding conventions

If a lemma deals with the intersection of a set with either source or target of a `LocalEquiv`,
then it should use `e.source ∩ s` or `e.target ∩ t`, not `s ∩ e.source` or `t ∩ e.target`.

-/
open Lean Meta Elab Tactic

/-! Implementation of the `mfld_set_tac` tactic for working with the domains of partially-defined
functions (`LocalEquiv`, `LocalHomeomorph`, etc).

This is in a separate file from `Mathlib.Logic.Equiv.MfldSimpsAttr` because attributes need a new
file to become functional.
-/

-- register in the simpset `mfld_simps` several lemmas that are often useful when dealing
-- with manifolds
attribute [mfld_simps]
  id.def: ∀ {α : Sort u} (a : α), id a = a
id.def Function.comp.left_id: ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), id ∘ f = f
Function.comp.left_id Set.mem_setOf_eq: ∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ { y | p y }) = p x
Set.mem_setOf_eq Set.image_eq_empty: ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, f '' s = ∅ ↔ s = ∅
Set.image_eq_empty Set.univ_inter: ∀ {α : Type u} (a : Set α), Set.univ ∩ a = a
Set.univ_inter Set.preimage_univ: ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univ
Set.preimage_univ
  Set.prod_mk_mem_set_prod_eq: ∀ {α : Type u_2} {β : Type u_1} {s : Set α} {t : Set β} {a : α} {b : β}, ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)
Set.prod_mk_mem_set_prod_eq and_true_iff: ∀ (p : Prop), p ∧ True ↔ p
and_true_iff Set.mem_univ: ∀ {α : Type u} (x : α), x ∈ Set.univ
Set.mem_univ Set.mem_image_of_mem: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
Set.mem_image_of_mem true_and_iff: ∀ (p : Prop), True ∧ p ↔ p
true_and_iff
  Set.mem_inter_iff: ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
Set.mem_inter_iff Set.mem_preimage: ∀ {α : Type u_2} {β : Type u_1} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s
Set.mem_preimage Function.comp_apply: ∀ {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
Function.comp_apply Set.inter_subset_left: ∀ {α : Type u} (s t : Set α), s ∩ t ⊆ s
Set.inter_subset_left Set.mem_prod: ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β}, p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t
Set.mem_prod
  Set.range_id: ∀ {α : Type u_1}, Set.range id = Set.univ
Set.range_id Set.range_prod_map: ∀ {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} {m₁ : α → γ} {m₂ : β → δ},
  Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
Set.range_prod_map and_self_iff: ∀ (p : Prop), p ∧ p ↔ p
and_self_iff Set.mem_range_self: ∀ {α : Type u_1} {ι : Sort u_2} {f : ι → α} (i : ι), f i ∈ Set.range f
Set.mem_range_self eq_self_iff_true: ∀ {α : Sort u_1} (a : α), a = a ↔ True
eq_self_iff_true forall_const: ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], α → b ↔ b
forall_const
  forall_true_iff: ∀ {α : Sort u_1}, α → True ↔ True
forall_true_iff Set.inter_univ: ∀ {α : Type u} (a : Set α), a ∩ Set.univ = a
Set.inter_univ Set.preimage_id: ∀ {α : Type u_1} {s : Set α}, id ⁻¹' s = s
Set.preimage_id Function.comp.right_id: ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), f ∘ id = f
Function.comp.right_id not_false_iff: ¬False ↔ True
not_false_iff and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → c
and_imp
  Set.prod_inter_prod: ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
Set.prod_inter_prod Set.univ_prod_univ: ∀ {α : Type u_1} {β : Type u_2}, Set.univ ×ˢ Set.univ = Set.univ
Set.univ_prod_univ true_or_iff: ∀ (p : Prop), True ∨ p ↔ True
true_or_iff or_true_iff: ∀ (p : Prop), p ∨ True ↔ True
or_true_iff Prod.map_mk: ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} (f : α → γ) (g : β → δ) (a : α) (b : β),
  Prod.map f g (a, b) = (f a, g b)
Prod.map_mk Set.preimage_inter: ∀ {α : Type u_2} {β : Type u_1} {f : α → β} {s t : Set β}, f ⁻¹' (s ∩ t) = f ⁻¹' s ∩ f ⁻¹' t
Set.preimage_inter
  heq_iff_eq: ∀ {α : Sort u_1} {a b : α}, HEq a b ↔ a = b
heq_iff_eq Equiv.sigmaEquivProd_apply: ∀ (α : Type u_1) (β : Type u_2) (a : (_ : α) × β), ↑(Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
Equiv.sigmaEquivProd_apply Equiv.sigmaEquivProd_symm_apply: ∀ (α : Type u_1) (β : Type u_2) (a : α × β), ↑(Equiv.sigmaEquivProd α β).symm a = { fst := a.fst, snd := a.snd }
Equiv.sigmaEquivProd_symm_apply Subtype.coe_mk: ∀ {α : Sort u_1} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk
  Equiv.toFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ↑e
Equiv.toFun_as_coe Equiv.invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symm
Equiv.invFun_as_coe

/-- Common `@[simps]` configuration options used for manifold-related declarations. -/
def mfld_cfg: Simps.Config
mfld_cfg : Simps.Config: Type
Simps.Config where
  attrs := [`mfld_simps: Name
`mfld_simps]
  fullyApplied := false: Bool
false
#align mfld_cfg mfld_cfg: Simps.Config
mfld_cfg

namespace Tactic.MfldSetTac

/-- A very basic tactic to show that sets showing up in manifolds coincide or are included
in one another. -/
elab (name := mfldSetTac: ParserDescr
mfldSetTac) "mfld_set_tac" : tactic: Parser.Category
tactic => withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do
  let g: ?m.947
g ← getMainGoal: TacticM MVarId
getMainGoal
  let goalTy: ?m.1302
goalTy := (← instantiateMVars (← g.getDecl).type): ?m.1299
(← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars(← instantiateMVars (← g.getDecl).type): ?m.1299
 (← g.getDecl): ?m.1174
(← g: ?m.947
g(← g.getDecl): ?m.1174
.getDecl: MVarId → MetaM MetavarDecl
getDecl(← g.getDecl): ?m.1174
)(← instantiateMVars (← g.getDecl).type): ?m.1299
.type: MetavarDecl → Expr
type(← instantiateMVars (← g.getDecl).type): ?m.1299
).getAppFnArgs: Expr → Name × Array Expr
getAppFnArgs
  match goalTy: ?m.1302
goalTy with
  | (``Eq: Name
``Eq: {α : Sort u_1} → α → α → Prop
Eq, #[_ty: Expr
_ty, _e₁: Expr
_e₁, _e₂: Expr
_e₂]) =>
    evalTactic: Syntax → TacticM Unit
evalTactic (← `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps])))): ?m.2420
(← `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
`(tactic| (
      `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
apply`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 Set.ext; `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
intro`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 my_y
      `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
constructor`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 <;>
        · `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
intro`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 h_my_y
          `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
try`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 (`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
simp`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
only`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 [*, mfld_simps] `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
at`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 h_my_y; `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
simp`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
only`(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.1409 ?m.1412
 [*, mfld_simps])))(← `(tactic| (
      apply Set.ext; intro my_y
      constructor <;>
        · intro h_my_y
          try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps])))): ?m.2420
)
  | (``Subset: Name
``Subset: {α : Type u} → [self : HasSubset α] → α → α → Prop
Subset, #[_ty: Expr
_ty, _inst: Expr
_inst, _e₁: Expr
_e₁, _e₂: Expr
_e₂]) =>
    evalTactic: Syntax → TacticM Unit
evalTactic (← `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps])))): ?m.2906
(← `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
`(tactic| (
      `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
intro`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 my_y h_my_y
      `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
try`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 (`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
simp`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
only`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 [*, mfld_simps] `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
at`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 h_my_y; `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
simp`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
only`(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps]))): ?m.2646 ?m.2649
 [*, mfld_simps])))(← `(tactic| (
      intro my_y h_my_y
      try (simp only [*, mfld_simps] at h_my_y; simp only [*, mfld_simps])))): ?m.2906
)
  | _ => throwError "goal should be an equality or an inclusion": ?m.3026 ?m.3027
throwErrorthrowError "goal should be an equality or an inclusion": ?m.3026 ?m.3027
 "goal should be an equality or an inclusion"

attribute [mfld_simps] and_true: ∀ (p : Prop), (p ∧ True) = p
and_true eq_self_iff_true: ∀ {α : Sort u_1} (a : α), a = a ↔ True
eq_self_iff_true Function.comp_apply: ∀ {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)
Function.comp_apply

end Tactic.MfldSetTac

open Function Set

variable {α: Type ?u.27635
α : Type _: Type (?u.29260+1)
Type _} {β: Type ?u.40431
β : Type _: Type (?u.18434+1)
Type _} {γ: Type ?u.40159
γ : Type _: Type (?u.40256+1)
Type _} {δ: Type ?u.26389
δ : Type _: Type (?u.24668+1)
Type _}

/-- Local equivalence between subsets `source` and `target` of `α` and `β` respectively. The
(global) maps `toFun : α → β` and `invFun : β → α` map `source` to `target` and conversely, and are
inverse to each other there. The values of `toFun` outside of `source` and of `invFun` outside of
`target` are irrelevant. -/
structure LocalEquiv: Type u_1 → Type u_2 → Type (maxu_1u_2)
LocalEquiv (α: Type ?u.16161
α : Type _: Type (?u.16161+1)
Type _) (β: Type ?u.16164
β : Type _: Type (?u.16164+1)
Type _) where
  /-- The global function which has a local inverse. Its value outside of the `source` subset is
  irrelevant. -/
  toFun: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → α → β
toFun : α: Type ?u.16161
α → β: Type ?u.16164
β
  /-- The local inverse to `toFun`. Its value outside of the `target` subset is irrelevant. -/
  invFun: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → β → α
invFun : β: Type ?u.16164
β → α: Type ?u.16161
α
  /-- The domain of the local equivalence. -/
  source: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → Set α
source : Set: Type ?u.16177 → Type ?u.16177
Set α: Type ?u.16161
α
  /-- The codomain of the local equivalence. -/
  target: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → Set β
target : Set: Type ?u.16180 → Type ?u.16180
Set β: Type ?u.16164
β
  /-- The proposition that elements of `source` are mapped to elements of `target`. -/
  map_source': ∀ {α : Type u_1} {β : Type u_2} (self : LocalEquiv α β) ⦃x : α⦄, x ∈ self.source → LocalEquiv.toFun self x ∈ self.target
map_source' : ∀ ⦃x: ?m.16184
x⦄, x: ?m.16184
x ∈ source: Set α
source → toFun: α → β
toFun x: ?m.16184
x ∈ target: Set β
target
  /-- The proposition that elements of `target` are mapped to elements of `source`. -/
  map_target': ∀ {α : Type u_1} {β : Type u_2} (self : LocalEquiv α β) ⦃x : β⦄,
  x ∈ self.target → LocalEquiv.invFun self x ∈ self.source
map_target' : ∀ ⦃x: ?m.16248
x⦄, x: ?m.16248
x ∈ target: Set β
target → invFun: β → α
invFun x: ?m.16248
x ∈ source: Set α
source
  /-- The proposition that `invFun` is a local left-inverse of `toFun` on `source`. -/
  left_inv': ∀ {α : Type u_1} {β : Type u_2} (self : LocalEquiv α β) ⦃x : α⦄,
  x ∈ self.source → LocalEquiv.invFun self (LocalEquiv.toFun self x) = x
left_inv' : ∀ ⦃x: ?m.16304
x⦄, x: ?m.16304
x ∈ source: Set α
source → invFun: β → α
invFun (toFun: α → β
toFun x: ?m.16304
x) = x: ?m.16304
x
  /-- The proposition that `invFun` is a local right-inverse of `toFun` on `target`. -/
  right_inv': ∀ {α : Type u_1} {β : Type u_2} (self : LocalEquiv α β) ⦃x : β⦄,
  x ∈ self.target → LocalEquiv.toFun self (LocalEquiv.invFun self x) = x
right_inv' : ∀ ⦃x: ?m.16338
x⦄, x: ?m.16338
x ∈ target: Set β
target → toFun: α → β
toFun (invFun: β → α
invFun x: ?m.16338
x) = x: ?m.16338
x
#align local_equiv LocalEquiv: Type u_1 → Type u_2 → Type (maxu_1u_2)
LocalEquiv

namespace LocalEquiv

variable (e: LocalEquiv α β
e : LocalEquiv: Type ?u.39079 → Type ?u.39078 → Type (max?u.39079?u.39078)
LocalEquiv α: Type ?u.17316
α β: Type ?u.22997
β) (e': LocalEquiv β γ
e' : LocalEquiv: Type ?u.24816 → Type ?u.24815 → Type (max?u.24816?u.24815)
LocalEquiv β: Type ?u.17299
β γ: Type ?u.17302
γ)

instance: {α : Type u_1} → {β : Type u_2} → [inst : Inhabited α] → [inst : Inhabited β] → Inhabited (LocalEquiv α β)
instance [Inhabited: Sort ?u.17336 → Sort (max1?u.17336)
Inhabited α: Type ?u.17316
α] [Inhabited: Sort ?u.17339 → Sort (max1?u.17339)
Inhabited β: Type ?u.17319
β] : Inhabited: Sort ?u.17342 → Sort (max1?u.17342)
Inhabited (LocalEquiv: Type ?u.17344 → Type ?u.17343 → Type (max?u.17344?u.17343)
LocalEquiv α: Type ?u.17316
α β: Type ?u.17319
β) :=
  ⟨⟨const: {α : Sort ?u.17374} → (β : Sort ?u.17373) → α → β → α
const α: Type ?u.17316
α default: {α : Sort ?u.17378} → [self : Inhabited α] → α
default, const: {α : Sort ?u.17500} → (β : Sort ?u.17499) → α → β → α
const β: Type ?u.17319
β default: {α : Sort ?u.17504} → [self : Inhabited α] → α
default, ∅: ?m.17627
∅, ∅: ?m.17671
∅, mapsTo_empty: ∀ {α : Type ?u.17715} {β : Type ?u.17714} (f : α → β) (t : Set β), MapsTo f ∅ t
mapsTo_empty _: ?m.17716 → ?m.17717
_ _: Set ?m.17717
_, mapsTo_empty: ∀ {α : Type ?u.17738} {β : Type ?u.17737} (f : α → β) (t : Set β), MapsTo f ∅ t
mapsTo_empty _: ?m.17739 → ?m.17740
_ _: Set ?m.17740
_, eqOn_empty: ∀ {α : Type ?u.17760} {β : Type ?u.17761} (f₁ f₂ : α → β), EqOn f₁ f₂ ∅
eqOn_empty _: ?m.17762 → ?m.17763
_ _: ?m.17762 → ?m.17763
_,
      eqOn_empty: ∀ {α : Type ?u.17778} {β : Type ?u.17779} (f₁ f₂ : α → β), EqOn f₁ f₂ ∅
eqOn_empty _: ?m.17780 → ?m.17781
_ _: ?m.17780 → ?m.17781
_⟩⟩

/-- The inverse of a local equiv -/
protected def symm: LocalEquiv β α
symm : LocalEquiv: Type ?u.17922 → Type ?u.17921 → Type (max?u.17922?u.17921)
LocalEquiv β: Type ?u.17904
β α: Type ?u.17901
α where
  toFun := e: LocalEquiv α β
e.invFun: {α : Type ?u.17931} → {β : Type ?u.17930} → LocalEquiv α β → β → α
invFun
  invFun := e: LocalEquiv α β
e.toFun: {α : Type ?u.17940} → {β : Type ?u.17939} → LocalEquiv α β → α → β
toFun
  source := e: LocalEquiv α β
e.target: {α : Type ?u.17947} → {β : Type ?u.17946} → LocalEquiv α β → Set β
target
  target := e: LocalEquiv α β
e.source: {α : Type ?u.17953} → {β : Type ?u.17952} → LocalEquiv α β → Set α
source
  map_source' := e: LocalEquiv α β
e.map_target': ∀ {α : Type ?u.17959} {β : Type ?u.17958} (self : LocalEquiv α β) ⦃x : β⦄, x ∈ self.target → invFun self x ∈ self.source
map_target'
  map_target' := e: LocalEquiv α β
e.map_source': ∀ {α : Type ?u.17967} {β : Type ?u.17966} (self : LocalEquiv α β) ⦃x : α⦄, x ∈ self.source → toFun self x ∈ self.target
map_source'
  left_inv' := e: LocalEquiv α β
e.right_inv': ∀ {α : Type ?u.17975} {β : Type ?u.17974} (self : LocalEquiv α β) ⦃x : β⦄,
  x ∈ self.target → toFun self (invFun self x) = x
right_inv'
  right_inv' := e: LocalEquiv α β
e.left_inv': ∀ {α : Type ?u.17986} {β : Type ?u.17985} (self : LocalEquiv α β) ⦃x : α⦄,
  x ∈ self.source → invFun self (toFun self x) = x
left_inv'
#align local_equiv.symm LocalEquiv.symm: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → LocalEquiv β α
LocalEquiv.symm

instance: {α : Type u_1} → {β : Type u_2} → CoeFun (LocalEquiv α β) fun x => α → β
instance : CoeFun: (α : Sort ?u.18202) → outParam (α → Sort ?u.18201) → Sort (max(max1?u.18202)?u.18201)
CoeFun (LocalEquiv: Type ?u.18204 → Type ?u.18203 → Type (max?u.18204?u.18203)
LocalEquiv α: Type ?u.18181
α β: Type ?u.18184
β) fun _: ?m.18206
_ => α: Type ?u.18181
α → β: Type ?u.18184
β :=
  ⟨LocalEquiv.toFun: {α : Type ?u.18235} → {β : Type ?u.18234} → LocalEquiv α β → α → β
LocalEquiv.toFun⟩

/-- See Note [custom simps projection] -/
def Simps.symm_apply: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → β → α
Simps.symm_apply (e: LocalEquiv α β
e : LocalEquiv: Type ?u.18452 → Type ?u.18451 → Type (max?u.18452?u.18451)
LocalEquiv α: Type ?u.18431
α β: Type ?u.18434
β) : β: Type ?u.18434
β → α: Type ?u.18431
α :=
  e: LocalEquiv α β
e.symm: {α : Type ?u.18460} → {β : Type ?u.18459} → LocalEquiv α β → LocalEquiv β α
symm
#align local_equiv.simps.symm_apply LocalEquiv.Simps.symm_apply: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → β → α
LocalEquiv.Simps.symm_apply

initialize_simps_projections LocalEquiv: Type u_1 → Type u_2 → Type (maxu_1u_2)
LocalEquiv (toFun: (α : Type u_1) → (β : Type u_2) → LocalEquiv α β → α → β
toFun → apply: (α : Type u_1) → (β : Type u_2) → LocalEquiv α β → α → β
apply, invFun: (α : Type u_1) → (β : Type u_2) → LocalEquiv α β → β → α
invFun → symm_apply: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → β → α
symm_apply)

-- Porting note: this can be proven with `dsimp only`
-- @[simp, mfld_simps]
-- theorem coe_mk (f : α → β) (g s t ml mr il ir) : (LocalEquiv.mk f g s t ml mr il ir : α → β) = f
-- := by dsimp only
-- #align local_equiv.coe_mk LocalEquiv.coe_mk
#noalign local_equiv.coe_mk

@[simp, mfld_simps]
theorem coe_symm_mk: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : Set α) (t : Set β) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t)
  (mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x),
  (LocalEquiv.symm
        { toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
          right_inv' := ir }).toFun =     g
coe_symm_mk (f: α → β
f : α: Type ?u.18725
α → β: Type ?u.18728
β) (g: ?m.18749
g s: Set α
s t: Set β
t ml: ?m.18758
ml mr: ?m.18761
mr il: ?m.18764
il ir: ∀ ⦃x : β⦄, x ∈ t → f (g x) = x
ir) :
    ((LocalEquiv.mk: {α : Type ?u.18775} →
  {β : Type ?u.18774} →
    (toFun : α → β) →
      (invFun : β → α) →
        (source : Set α) →
          (target : Set β) →
            (∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) →
              (∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source) →
                (∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x) →
                  (∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x) → LocalEquiv α β
LocalEquiv.mk f: α → β
f g: ?m.18749
g s: ?m.18752
s t: ?m.18755
t ml: ?m.18758
ml mr: ?m.18761
mr il: ?m.18764
il ir: ?m.18767
ir).symm: {α : Type ?u.18808} → {β : Type ?u.18807} → LocalEquiv α β → LocalEquiv β α
symm : β: Type ?u.18728
β → α: Type ?u.18725
α) = g: ?m.18749
g :=
  rfl: ∀ {α : Sort ?u.18866} {a : α}, a = a
rfl
#align local_equiv.coe_symm_mk LocalEquiv.coe_symm_mk: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : Set α) (t : Set β) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t)
  (mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x),
  (LocalEquiv.symm
        { toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
          right_inv' := ir }).toFun =     g
LocalEquiv.coe_symm_mk

-- Porting note: this is now a syntactic tautology
-- @[simp, mfld_simps]
-- theorem toFun_as_coe : e.toFun = e := rfl
-- #align local_equiv.to_fun_as_coe LocalEquiv.toFun_as_coe
#noalign local_equiv.to_fun_as_coe

@[simp, mfld_simps]
theorem invFun_as_coe: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), e.invFun = (LocalEquiv.symm e).toFun
invFun_as_coe : e: LocalEquiv α β
e.invFun: {α : Type ?u.19019} → {β : Type ?u.19018} → LocalEquiv α β → β → α
invFun = e: LocalEquiv α β
e.symm: {α : Type ?u.19026} → {β : Type ?u.19025} → LocalEquiv α β → LocalEquiv β α
symm :=
  rfl: ∀ {α : Sort ?u.19239} {a : α}, a = a
rfl
#align local_equiv.inv_fun_as_coe LocalEquiv.invFun_as_coe: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), e.invFun = (LocalEquiv.symm e).toFun
LocalEquiv.invFun_as_coe

@[simp, mfld_simps]
theorem map_source: ∀ {x : α}, x ∈ e.source → toFun e x ∈ e.target
map_source {x: α
x : α: Type ?u.19263
α} (h: x ∈ e.source
h : x: α
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.19301} → {β : Type ?u.19300} → LocalEquiv α β → Set α
source) : e: LocalEquiv α β
e x: α
x ∈ e: LocalEquiv α β
e.target: {α : Type ?u.19366} → {β : Type ?u.19365} → LocalEquiv α β → Set β
target :=
  e: LocalEquiv α β
e.map_source': ∀ {α : Type ?u.19386} {β : Type ?u.19385} (self : LocalEquiv α β) ⦃x : α⦄, x ∈ self.source → toFun self x ∈ self.target
map_source' h: x ∈ e.source
h
#align local_equiv.map_source LocalEquiv.map_source: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.target
LocalEquiv.map_source

@[simp, mfld_simps]
theorem map_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β}, x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.source
map_target {x: β
x : β: Type ?u.19456
β} (h: x ∈ e.target
h : x: β
x ∈ e: LocalEquiv α β
e.target: {α : Type ?u.19491} → {β : Type ?u.19490} → LocalEquiv α β → Set β
target) : e: LocalEquiv α β
e.symm: {α : Type ?u.19525} → {β : Type ?u.19524} → LocalEquiv α β → LocalEquiv β α
symm x: β
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.19565} → {β : Type ?u.19564} → LocalEquiv α β → Set α
source :=
  e: LocalEquiv α β
e.map_target': ∀ {α : Type ?u.19585} {β : Type ?u.19584} (self : LocalEquiv α β) ⦃x : β⦄, x ∈ self.target → invFun self x ∈ self.source
map_target' h: x ∈ e.target
h
#align local_equiv.map_target LocalEquiv.map_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β}, x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.source
LocalEquiv.map_target

@[simp, mfld_simps]
theorem left_inv: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv {x: α
x : α: Type ?u.19659
α} (h: x ∈ e.source
h : x: α
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.19697} → {β : Type ?u.19696} → LocalEquiv α β → Set α
source) : e: LocalEquiv α β
e.symm: {α : Type ?u.19717} → {β : Type ?u.19716} → LocalEquiv α β → LocalEquiv β α
symm (e: LocalEquiv α β
e x: α
x) = x: α
x :=
  e: LocalEquiv α β
e.left_inv': ∀ {α : Type ?u.19792} {β : Type ?u.19791} (self : LocalEquiv α β) ⦃x : α⦄,
  x ∈ self.source → invFun self (toFun self x) = x
left_inv' h: x ∈ e.source
h
#align local_equiv.left_inv LocalEquiv.left_inv: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
LocalEquiv.left_inv

@[simp, mfld_simps]
theorem right_inv: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β}, x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
right_inv {x: β
x : β: Type ?u.19845
β} (h: x ∈ e.target
h : x: β
x ∈ e: LocalEquiv α β
e.target: {α : Type ?u.19880} → {β : Type ?u.19879} → LocalEquiv α β → Set β
target) : e: LocalEquiv α β
e (e: LocalEquiv α β
e.symm: {α : Type ?u.19931} → {β : Type ?u.19930} → LocalEquiv α β → LocalEquiv β α
symm x: β
x) = x: β
x :=
  e: LocalEquiv α β
e.right_inv': ∀ {α : Type ?u.19975} {β : Type ?u.19974} (self : LocalEquiv α β) ⦃x : β⦄,
  x ∈ self.target → toFun self (invFun self x) = x
right_inv' h: x ∈ e.target
h
#align local_equiv.right_inv LocalEquiv.right_inv: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {x : β}, x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
LocalEquiv.right_inv

theorem eq_symm_apply: ∀ {x : α} {y : β}, x ∈ e.source → y ∈ e.target → (x = toFun (LocalEquiv.symm e) y ↔ toFun e x = y)
eq_symm_apply {x: α
x : α: Type ?u.20026
α} {y: β
y : β: Type ?u.20029
β} (hx: x ∈ e.source
hx : x: α
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.20066} → {β : Type ?u.20065} → LocalEquiv α β → Set α
source) (hy: y ∈ e.target
hy : y: β
y ∈ e: LocalEquiv α β
e.target: {α : Type ?u.20100} → {β : Type ?u.20099} → LocalEquiv α β → Set β
target) :
    x: α
x = e: LocalEquiv α β
e.symm: {α : Type ?u.20118} → {β : Type ?u.20117} → LocalEquiv α β → LocalEquiv β α
symm y: β
y ↔ e: LocalEquiv α β
e x: α
x = y: β
y :=
  ⟨fun h: ?m.20205
h => by
Goals accomplished! 🐙 α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: x = toFun (LocalEquiv.symm e) y

toFun e x = yrw [α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: x = toFun (LocalEquiv.symm e) y

toFun e x = y← e: LocalEquiv α β
e.right_inv: ∀ {α : Type ?u.20221} {β : Type ?u.20220} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
right_inv hy: y ∈ e.target
hy,α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: x = toFun (LocalEquiv.symm e) y

toFun e x = toFun e (toFun (LocalEquiv.symm e) y) α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: x = toFun (LocalEquiv.symm e) y

toFun e x = yh: x = toFun (LocalEquiv.symm e) y
hα: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: x = toFun (LocalEquiv.symm e) y

toFun e (toFun (LocalEquiv.symm e) y) = toFun e (toFun (LocalEquiv.symm e) y)]
Goals accomplished! 🐙, fun h: ?m.20212
h => by
Goals accomplished! 🐙 α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: toFun e x = y

x = toFun (LocalEquiv.symm e) yrw [α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: toFun e x = y

x = toFun (LocalEquiv.symm e) y← e: LocalEquiv α β
e.left_inv: ∀ {α : Type ?u.20247} {β : Type ?u.20248} (e : LocalEquiv α β) {x : α},
  x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv hx: x ∈ e.source
hx,α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: toFun e x = y

toFun (LocalEquiv.symm e) (toFun e x) = toFun (LocalEquiv.symm e) y α: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: toFun e x = y

x = toFun (LocalEquiv.symm e) yh: toFun e x = y
hα: Type u_1

β: Type u_2

γ: Type ?u.20032

δ: Type ?u.20035

e: LocalEquiv α β

e': LocalEquiv β γ

x: α

y: β

hx: x ∈ e.source

hy: y ∈ e.target

h: toFun e x = y

toFun (LocalEquiv.symm e) y = toFun (LocalEquiv.symm e) y]
Goals accomplished! 🐙⟩
#align local_equiv.eq_symm_apply LocalEquiv.eq_symm_apply: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α} {y : β},
  x ∈ e.source → y ∈ e.target → (x = toFun (LocalEquiv.symm e) y ↔ toFun e x = y)
LocalEquiv.eq_symm_apply

protected theorem mapsTo: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), MapsTo e.toFun e.source e.target
mapsTo : MapsTo: {α : Type ?u.20307} → {β : Type ?u.20306} → (α → β) → Set α → Set β → Prop
MapsTo e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.20346} → {β : Type ?u.20345} → LocalEquiv α β → Set α
source e: LocalEquiv α β
e.target: {α : Type ?u.20352} → {β : Type ?u.20351} → LocalEquiv α β → Set β
target := fun _: ?m.20359
_ => e: LocalEquiv α β
e.map_source: ∀ {α : Type ?u.20361} {β : Type ?u.20362} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.target
map_source
#align local_equiv.maps_to LocalEquiv.mapsTo: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), MapsTo e.toFun e.source e.target
LocalEquiv.mapsTo

theorem symm_mapsTo: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), MapsTo (LocalEquiv.symm e).toFun e.target e.source
symm_mapsTo : MapsTo: {α : Type ?u.20408} → {β : Type ?u.20407} → (α → β) → Set α → Set β → Prop
MapsTo e: LocalEquiv α β
e.symm: {α : Type ?u.20412} → {β : Type ?u.20411} → LocalEquiv α β → LocalEquiv β α
symm e: LocalEquiv α β
e.target: {α : Type ?u.20456} → {β : Type ?u.20455} → LocalEquiv α β → Set β
target e: LocalEquiv α β
e.source: {α : Type ?u.20462} → {β : Type ?u.20461} → LocalEquiv α β → Set α
source :=
  e: LocalEquiv α β
e.symm: {α : Type ?u.20469} → {β : Type ?u.20468} → LocalEquiv α β → LocalEquiv β α
symm.mapsTo: ∀ {α : Type ?u.20474} {β : Type ?u.20475} (e : LocalEquiv α β), MapsTo e.toFun e.source e.target
mapsTo
#align local_equiv.symm_maps_to LocalEquiv.symm_mapsTo: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), MapsTo (LocalEquiv.symm e).toFun e.target e.source
LocalEquiv.symm_mapsTo

protected theorem leftInvOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
leftInvOn : LeftInvOn: {α : Type ?u.20518} → {β : Type ?u.20517} → (β → α) → (α → β) → Set α → Prop
LeftInvOn e: LocalEquiv α β
e.symm: {α : Type ?u.20522} → {β : Type ?u.20521} → LocalEquiv α β → LocalEquiv β α
symm e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.20599} → {β : Type ?u.20598} → LocalEquiv α β → Set α
source := fun _: ?m.20606
_ => e: LocalEquiv α β
e.left_inv: ∀ {α : Type ?u.20608} {β : Type ?u.20609} (e : LocalEquiv α β) {x : α},
  x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv
#align local_equiv.left_inv_on LocalEquiv.leftInvOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
LocalEquiv.leftInvOn

protected theorem rightInvOn: RightInvOn (LocalEquiv.symm e).toFun e.toFun e.target
rightInvOn : RightInvOn: {α : Type ?u.20658} → {β : Type ?u.20657} → (β → α) → (α → β) → Set β → Prop
RightInvOn e: LocalEquiv α β
e.symm: {α : Type ?u.20662} → {β : Type ?u.20661} → LocalEquiv α β → LocalEquiv β α
symm e: LocalEquiv α β
e e: LocalEquiv α β
e.target: {α : Type ?u.20739} → {β : Type ?u.20738} → LocalEquiv α β → Set β
target := fun _: ?m.20746
_ => e: LocalEquiv α β
e.right_inv: ∀ {α : Type ?u.20749} {β : Type ?u.20748} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
right_inv
#align local_equiv.right_inv_on LocalEquiv.rightInvOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), RightInvOn (LocalEquiv.symm e).toFun e.toFun e.target
LocalEquiv.rightInvOn

protected theorem invOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InvOn (LocalEquiv.symm e).toFun e.toFun e.source e.target
invOn : InvOn: {α : Type ?u.20798} → {β : Type ?u.20797} → (β → α) → (α → β) → Set α → Set β → Prop
InvOn e: LocalEquiv α β
e.symm: {α : Type ?u.20802} → {β : Type ?u.20801} → LocalEquiv α β → LocalEquiv β α
symm e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.20879} → {β : Type ?u.20878} → LocalEquiv α β → Set α
source e: LocalEquiv α β
e.target: {α : Type ?u.20885} → {β : Type ?u.20884} → LocalEquiv α β → Set β
target :=
  ⟨e: LocalEquiv α β
e.leftInvOn: ∀ {α : Type ?u.20899} {β : Type ?u.20900} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
leftInvOn, e: LocalEquiv α β
e.rightInvOn: ∀ {α : Type ?u.20918} {β : Type ?u.20919} (e : LocalEquiv α β), RightInvOn (LocalEquiv.symm e).toFun e.toFun e.target
rightInvOn⟩
#align local_equiv.inv_on LocalEquiv.invOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InvOn (LocalEquiv.symm e).toFun e.toFun e.source e.target
LocalEquiv.invOn

protected theorem injOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InjOn e.toFun e.source
injOn : InjOn: {α : Type ?u.20960} → {β : Type ?u.20959} → (α → β) → Set α → Prop
InjOn e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.20999} → {β : Type ?u.20998} → LocalEquiv α β → Set α
source :=
  e: LocalEquiv α β
e.leftInvOn: ∀ {α : Type ?u.21005} {β : Type ?u.21006} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
leftInvOn.injOn: ∀ {α : Type ?u.21011} {β : Type ?u.21012} {s : Set α} {f : α → β} {f₁' : β → α}, LeftInvOn f₁' f s → InjOn f s
injOn
#align local_equiv.inj_on LocalEquiv.injOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InjOn e.toFun e.source
LocalEquiv.injOn

protected theorem bijOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), BijOn e.toFun e.source e.target
bijOn : BijOn: {α : Type ?u.21071} → {β : Type ?u.21070} → (α → β) → Set α → Set β → Prop
BijOn e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.21110} → {β : Type ?u.21109} → LocalEquiv α β → Set α
source e: LocalEquiv α β
e.target: {α : Type ?u.21116} → {β : Type ?u.21115} → LocalEquiv α β → Set β
target :=
  e: LocalEquiv α β
e.invOn: ∀ {α : Type ?u.21122} {β : Type ?u.21123} (e : LocalEquiv α β),
  InvOn (LocalEquiv.symm e).toFun e.toFun e.source e.target
invOn.bijOn: ∀ {α : Type ?u.21128} {β : Type ?u.21129} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  InvOn f' f s t → MapsTo f s t → MapsTo f' t s → BijOn f s t
bijOn e: LocalEquiv α β
e.mapsTo: ∀ {α : Type ?u.21167} {β : Type ?u.21168} (e : LocalEquiv α β), MapsTo e.toFun e.source e.target
mapsTo e: LocalEquiv α β
e.symm_mapsTo: ∀ {α : Type ?u.21185} {β : Type ?u.21184} (e : LocalEquiv α β), MapsTo (LocalEquiv.symm e).toFun e.target e.source
symm_mapsTo
#align local_equiv.bij_on LocalEquiv.bijOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), BijOn e.toFun e.source e.target
LocalEquiv.bijOn

protected theorem surjOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), SurjOn e.toFun e.source e.target
surjOn : SurjOn: {α : Type ?u.21226} → {β : Type ?u.21225} → (α → β) → Set α → Set β → Prop
SurjOn e: LocalEquiv α β
e e: LocalEquiv α β
e.source: {α : Type ?u.21265} → {β : Type ?u.21264} → LocalEquiv α β → Set α
source e: LocalEquiv α β
e.target: {α : Type ?u.21271} → {β : Type ?u.21270} → LocalEquiv α β → Set β
target :=
  e: LocalEquiv α β
e.bijOn: ∀ {α : Type ?u.21277} {β : Type ?u.21278} (e : LocalEquiv α β), BijOn e.toFun e.source e.target
bijOn.surjOn: ∀ {α : Type ?u.21283} {β : Type ?u.21284} {s : Set α} {t : Set β} {f : α → β}, BijOn f s t → SurjOn f s t
surjOn
#align local_equiv.surj_on LocalEquiv.surjOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), SurjOn e.toFun e.source e.target
LocalEquiv.surjOn

/-- Associate a `LocalEquiv` to an `Equiv`. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).toFun = ↑e
simps (config := mfld_cfg: Simps.Config
mfld_cfg)]
def _root_.Equiv.toLocalEquiv: α ≃ β → LocalEquiv α β
_root_.Equiv.toLocalEquiv (e: α ≃ β
e : α: Type ?u.21321
α ≃ β: Type ?u.21324
β) : LocalEquiv: Type ?u.21346 → Type ?u.21345 → Type (max?u.21346?u.21345)
LocalEquiv α: Type ?u.21321
α β: Type ?u.21324
β where
  toFun := e: α ≃ β
e
  invFun := e: α ≃ β
e.symm: {α : Sort ?u.21424} → {β : Sort ?u.21423} → α ≃ β → β ≃ α
symm
  source := univ: {α : Type ?u.21497} → Set α
univ
  target := univ: {α : Type ?u.21501} → Set α
univ
  map_source' _: ?m.21506
_ _: ?m.21509
_ := mem_univ: ∀ {α : Type ?u.21511} (x : α), x ∈ univ
mem_univ _: ?m.21512
_
  map_target' _: ?m.21526
_ _: ?m.21529
_ := mem_univ: ∀ {α : Type ?u.21531} (x : α), x ∈ univ
mem_univ _: ?m.21532
_
  left_inv' x: ?m.21546
x _: ?m.21549
_ := e: α ≃ β
e.left_inv: ∀ {α : Sort ?u.21552} {β : Sort ?u.21551} (self : α ≃ β), LeftInverse self.invFun self.toFun
left_inv x: ?m.21546
x
  right_inv' x: ?m.21564
x _: ?m.21567
_ := e: α ≃ β
e.right_inv: ∀ {α : Sort ?u.21570} {β : Sort ?u.21569} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
right_inv x: ?m.21564
x
#align equiv.to_local_equiv Equiv.toLocalEquiv: {α : Type u_1} → {β : Type u_2} → α ≃ β → LocalEquiv α β
Equiv.toLocalEquiv
#align equiv.to_local_equiv_symm_apply Equiv.toLocalEquiv_symm_apply: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (LocalEquiv.symm (Equiv.toLocalEquiv e)).toFun = ↑e.symm
Equiv.toLocalEquiv_symm_apply
#align equiv.to_local_equiv_target Equiv.toLocalEquiv_target: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).target = univ
Equiv.toLocalEquiv_target
#align equiv.to_local_equiv_apply Equiv.toLocalEquiv_apply: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).toFun = ↑e
Equiv.toLocalEquiv_apply
#align equiv.to_local_equiv_source Equiv.toLocalEquiv_source: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).source = univ
Equiv.toLocalEquiv_source

instance inhabitedOfEmpty: {α : Type u_1} → {β : Type u_2} → [inst : IsEmpty α] → [inst : IsEmpty β] → Inhabited (LocalEquiv α β)
inhabitedOfEmpty [IsEmpty: Sort ?u.21971 → Prop
IsEmpty α: Type ?u.21951
α] [IsEmpty: Sort ?u.21974 → Prop
IsEmpty β: Type ?u.21954
β] : Inhabited: Sort ?u.21977 → Sort (max1?u.21977)
Inhabited (LocalEquiv: Type ?u.21979 → Type ?u.21978 → Type (max?u.21979?u.21978)
LocalEquiv α: Type ?u.21951
α β: Type ?u.21954
β) :=
  ⟨((Equiv.equivEmpty: (α : Sort ?u.21988) → [inst : IsEmpty α] → α ≃ Empty
Equiv.equivEmpty α: Type ?u.21951
α).trans: {α : Sort ?u.21995} → {β : Sort ?u.21994} → {γ : Sort ?u.21993} → α ≃ β → β ≃ γ → α ≃ γ
trans (Equiv.equivEmpty: (α : Sort ?u.22006) → [inst : IsEmpty α] → α ≃ Empty
Equiv.equivEmpty β: Type ?u.21954
β).symm: {α : Sort ?u.22011} → {β : Sort ?u.22010} → α ≃ β → β ≃ α
symm).toLocalEquiv: {α : Type ?u.22024} → {β : Type ?u.22023} → α ≃ β → LocalEquiv α β
toLocalEquiv⟩
#align local_equiv.inhabited_of_empty LocalEquiv.inhabitedOfEmpty: {α : Type u_1} → {β : Type u_2} → [inst : IsEmpty α] → [inst : IsEmpty β] → Inhabited (LocalEquiv α β)
LocalEquiv.inhabitedOfEmpty

/-- Create a copy of a `LocalEquiv` providing better definitional equalities. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  (copy e f hf g hg s hs t ht).target = t
simps (config := { fullyApplied := false: Bool
false })]
def copy: (e : LocalEquiv α β) →
  (f : α → β) →
    e.toFun = f →
      (g : β → α) →
        (LocalEquiv.symm e).toFun = g → (s : Set α) → e.source = s → (t : Set β) → e.target = t → LocalEquiv α β
copy (e: LocalEquiv α β
e : LocalEquiv: Type ?u.22114 → Type ?u.22113 → Type (max?u.22114?u.22113)
LocalEquiv α: Type ?u.22093
α β: Type ?u.22096
β) (f: α → β
f : α: Type ?u.22093
α → β: Type ?u.22096
β) (hf: e.toFun = f
hf : ⇑e: LocalEquiv α β
e = f: α → β
f) (g: β → α
g : β: Type ?u.22096
β → α: Type ?u.22093
α) (hg: (LocalEquiv.symm e).toFun = g
hg : ⇑e: LocalEquiv α β
e.symm: {α : Type ?u.22166} → {β : Type ?u.22165} → LocalEquiv α β → LocalEquiv β α
symm = g: β → α
g) (s: Set α
s : Set: Type ?u.22210 → Type ?u.22210
Set α: Type ?u.22093
α)
    (hs: e.source = s
hs : e: LocalEquiv α β
e.source: {α : Type ?u.22215} → {β : Type ?u.22214} → LocalEquiv α β → Set α
source = s: Set α
s) (t: Set β
t : Set: Type ?u.22224 → Type ?u.22224
Set β: Type ?u.22096
β) (ht: e.target = t
ht : e: LocalEquiv α β
e.target: {α : Type ?u.22229} → {β : Type ?u.22228} → LocalEquiv α β → Set β
target = t: Set β
t) :
    LocalEquiv: Type ?u.22239 → Type ?u.22238 → Type (max?u.22239?u.22238)
LocalEquiv α: Type ?u.22093
α β: Type ?u.22096
β where
  toFun := f: α → β
f
  invFun := g: β → α
g
  source := s: Set α
s
  target := t: Set β
t
  map_source' _: ?m.22263
_ := ht: e.target = t
ht ▸ hs: e.source = s
hs ▸ hf: e.toFun = f
hf ▸ e: LocalEquiv α β
e.map_source: ∀ {α : Type ?u.22265} {β : Type ?u.22266} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.target
map_source
  map_target' _: ?m.22317
_ := hs: e.source = s
hs ▸ ht: e.target = t
ht ▸ hg: (LocalEquiv.symm e).toFun = g
hg ▸ e: LocalEquiv α β
e.map_target: ∀ {α : Type ?u.22320} {β : Type ?u.22319} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.source
map_target
  left_inv' _: ?m.22371
_ := hs: e.source = s
hs ▸ hf: e.toFun = f
hf ▸ hg: (LocalEquiv.symm e).toFun = g
hg ▸ e: LocalEquiv α β
e.left_inv: ∀ {α : Type ?u.22373} {β : Type ?u.22374} (e : LocalEquiv α β) {x : α},
  x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv
  right_inv' _: ?m.22428
_ := ht: e.target = t
ht ▸ hf: e.toFun = f
hf ▸ hg: (LocalEquiv.symm e).toFun = g
hg ▸ e: LocalEquiv α β
e.right_inv: ∀ {α : Type ?u.22431} {β : Type ?u.22430} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
right_inv
#align local_equiv.copy LocalEquiv.copy: {α : Type u_1} →
  {β : Type u_2} →
    (e : LocalEquiv α β) →
      (f : α → β) →
        e.toFun = f →
          (g : β → α) →
            (LocalEquiv.symm e).toFun = g → (s : Set α) → e.source = s → (t : Set β) → e.target = t → LocalEquiv α β
LocalEquiv.copy
#align local_equiv.copy_source LocalEquiv.copy_source: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  (copy e f hf g hg s hs t ht).source = s
LocalEquiv.copy_source
#align local_equiv.copy_apply LocalEquiv.copy_apply: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  (copy e f hf g hg s hs t ht).toFun = f
LocalEquiv.copy_apply
#align local_equiv.copy_symm_apply LocalEquiv.copy_symm_apply: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  (LocalEquiv.symm (copy e f hf g hg s hs t ht)).toFun = g
LocalEquiv.copy_symm_apply
#align local_equiv.copy_target LocalEquiv.copy_target: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  (copy e f hf g hg s hs t ht).target = t
LocalEquiv.copy_target

theorem copy_eq: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  copy e f hf g hg s hs t ht = e
copy_eq (e: LocalEquiv α β
e : LocalEquiv: Type ?u.23015 → Type ?u.23014 → Type (max?u.23015?u.23014)
LocalEquiv α: Type ?u.22994
α β: Type ?u.22997
β) (f: α → β
f : α: Type ?u.22994
α → β: Type ?u.22997
β) (hf: e.toFun = f
hf : ⇑e: LocalEquiv α β
e = f: α → β
f) (g: β → α
g : β: Type ?u.22997
β → α: Type ?u.22994
α) (hg: (LocalEquiv.symm e).toFun = g
hg : ⇑e: LocalEquiv α β
e.symm: {α : Type ?u.23067} → {β : Type ?u.23066} → LocalEquiv α β → LocalEquiv β α
symm = g: β → α
g)
    (s: Set α
s : Set: Type ?u.23111 → Type ?u.23111
Set α: Type ?u.22994
α) (hs: e.source = s
hs : e: LocalEquiv α β
e.source: {α : Type ?u.23116} → {β : Type ?u.23115} → LocalEquiv α β → Set α
source = s: Set α
s) (t: Set β
t : Set: Type ?u.23125 → Type ?u.23125
Set β: Type ?u.22997
β) (ht: e.target = t
ht : e: LocalEquiv α β
e.target: {α : Type ?u.23130} → {β : Type ?u.23129} → LocalEquiv α β → Set β
target = t: Set β
t) :
    e: LocalEquiv α β
e.copy: {α : Type ?u.23141} →
  {β : Type ?u.23140} →
    (e : LocalEquiv α β) →
      (f : α → β) →
        e.toFun = f →
          (g : β → α) →
            (LocalEquiv.symm e).toFun = g → (s : Set α) → e.source = s → (t : Set β) → e.target = t → LocalEquiv α β
copy f: α → β
f hf: e.toFun = f
hf g: β → α
g hg: (LocalEquiv.symm e).toFun = g
hg s: Set α
s hs: e.source = s
hs t: Set β
t ht: e.target = t
ht = e: LocalEquiv α β
e := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.23000

δ: Type ?u.23003

e✝: LocalEquiv α β

e': LocalEquiv β γ

e: LocalEquiv α β

f: α → β

hf: e.toFun = f

g: β → α

hg: (LocalEquiv.symm e).toFun = g

s: Set α

hs: e.source = s

t: Set β

ht: e.target = t

copy e f hf g hg s hs t ht = esubsts f: α → β
f g: β → α
g s: Set α
s t: Set β
tα: Type u_1

β: Type u_2

γ: Type ?u.23000

δ: Type ?u.23003

e✝: LocalEquiv α β

e': LocalEquiv β γ

e: LocalEquiv α β

copy e e.toFun (_ : e.toFun = e.toFun) (LocalEquiv.symm e).toFun
    (_ : (LocalEquiv.symm e).toFun = (LocalEquiv.symm e).toFun) e.source (_ : e.source = e.source) e.target
    (_ : e.target = e.target) =   e
  α: Type u_1

β: Type u_2

γ: Type ?u.23000

δ: Type ?u.23003

e✝: LocalEquiv α β

e': LocalEquiv β γ

e: LocalEquiv α β

f: α → β

hf: e.toFun = f

g: β → α

hg: (LocalEquiv.symm e).toFun = g

s: Set α

hs: e.source = s

t: Set β

ht: e.target = t

copy e f hf g hg s hs t ht = ecases e: LocalEquiv α β
eα: Type u_1

β: Type u_2

γ: Type ?u.23000

δ: Type ?u.23003

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

mkcopy
    { 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 := 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 := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.toFun)
    (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
    (_ :
      (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 =         (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 := 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'✝ }
  α: Type u_1

β: Type u_2

γ: Type ?u.23000

δ: Type ?u.23003

e✝: LocalEquiv α β

e': LocalEquiv β γ

e: LocalEquiv α β

f: α → β

hf: e.toFun = f

g: β → α

hg: (LocalEquiv.symm e).toFun = g

s: Set α

hs: e.source = s

t: Set β

ht: e.target = t

copy e f hf g hg s hs t ht = erfl
Goals accomplished! 🐙
#align local_equiv.copy_eq LocalEquiv.copy_eq: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) (f : α → β) (hf : e.toFun = f) (g : β → α)
  (hg : (LocalEquiv.symm e).toFun = g) (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t),
  copy e f hf g hg s hs t ht = e
LocalEquiv.copy_eq

/-- Associate to a `LocalEquiv` an `Equiv` between the source and the target. -/
protected def toEquiv: {α : Type u_1} → {β : Type u_2} → (e : LocalEquiv α β) → ↑e.source ≃ ↑e.target
toEquiv : e: LocalEquiv α β
e.source: {α : Type ?u.23400} → {β : Type ?u.23399} → LocalEquiv α β → Set α
source ≃ e: LocalEquiv α β
e.target: {α : Type ?u.23558} → {β : Type ?u.23557} → LocalEquiv α β → Set β
target where
  toFun x: ?m.23717
x := ⟨e: LocalEquiv α β
e x: ?m.23717
x, e: LocalEquiv α β
e.map_source: ∀ {α : Type ?u.23841} {β : Type ?u.23842} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.target
map_source x: ?m.23717
x.mem: ∀ {α : Type ?u.23860} {s : Set α} (p : ↑s), ↑p ∈ s
mem⟩
  invFun y: ?m.23872
y := ⟨e: LocalEquiv α β
e.symm: {α : Type ?u.23887} → {β : Type ?u.23886} → LocalEquiv α β → LocalEquiv β α
symm y: ?m.23872
y, e: LocalEquiv α β
e.map_target: ∀ {α : Type ?u.24006} {β : Type ?u.24005} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.source
map_target y: ?m.23872
y.mem: ∀ {α : Type ?u.24024} {s : Set α} (p : ↑s), ↑p ∈ s
mem⟩
  left_inv := fun ⟨_, hx: val✝ ∈ e.source
hx⟩ => Subtype.eq: ∀ {α : Type ?u.24083} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.eq <| e: LocalEquiv α β
e.left_inv: ∀ {α : Type ?u.24098} {β : Type ?u.24099} (e : LocalEquiv α β) {x : α},
  x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv hx: val✝ ∈ e.source
hx
  right_inv := fun ⟨_, hy: val✝ ∈ e.target
hy⟩ => Subtype.eq: ∀ {α : Type ?u.24241} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.eq <| e: LocalEquiv α β
e.right_inv: ∀ {α : Type ?u.24257} {β : Type ?u.24256} (e : LocalEquiv α β) {x : β},
  x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = x
right_inv hy: val✝ ∈ e.target
hy
#align local_equiv.to_equiv LocalEquiv.toEquiv: {α : Type u_1} → {β : Type u_2} → (e : LocalEquiv α β) → ↑e.source ≃ ↑e.target
LocalEquiv.toEquiv

@[simp, mfld_simps]
theorem symm_source: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), (LocalEquiv.symm e).source = e.target
symm_source : e: LocalEquiv α β
e.symm: {α : Type ?u.24681} → {β : Type ?u.24680} → LocalEquiv α β → LocalEquiv β α
symm.source: {α : Type ?u.24687} → {β : Type ?u.24686} → LocalEquiv α β → Set α
source = e: LocalEquiv α β
e.target: {α : Type ?u.24694} → {β : Type ?u.24693} → LocalEquiv α β → Set β
target :=
  rfl: ∀ {α : Sort ?u.24701} {a : α}, a = a
rfl
#align local_equiv.symm_source LocalEquiv.symm_source: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), (LocalEquiv.symm e).source = e.target
LocalEquiv.symm_source

@[simp, mfld_simps]
theorem symm_target: (LocalEquiv.symm e).target = e.source
symm_target : e: LocalEquiv α β
e.symm: {α : Type ?u.24751} → {β : Type ?u.24750} → LocalEquiv α β → LocalEquiv β α
symm.target: {α : Type ?u.24757} → {β : Type ?u.24756} → LocalEquiv α β → Set β
target = e: LocalEquiv α β
e.source: {α : Type ?u.24764} → {β : Type ?u.24763} → LocalEquiv α β → Set α
source :=
  rfl: ∀ {α : Sort ?u.24771} {a : α}, a = a
rfl
#align local_equiv.symm_target LocalEquiv.symm_target: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), (LocalEquiv.symm e).target = e.source
LocalEquiv.symm_target

@[simp, mfld_simps]
theorem symm_symm: LocalEquiv.symm (LocalEquiv.symm e) = e
symm_symm : e: LocalEquiv α β
e.symm: {α : Type ?u.24821} → {β : Type ?u.24820} → LocalEquiv α β → LocalEquiv β α
symm.symm: {α : Type ?u.24827} → {β : Type ?u.24826} → LocalEquiv α β → LocalEquiv β α
symm = e: LocalEquiv α β
e := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.24805

δ: Type ?u.24808

e: LocalEquiv α β

e': LocalEquiv β γ

LocalEquiv.symm (LocalEquiv.symm e) = ecases e: LocalEquiv α β
eα: Type u_1

β: Type u_2

γ: Type ?u.24805

δ: Type ?u.24808

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

mkLocalEquiv.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'✝ }
  α: Type u_1

β: Type u_2

γ: Type ?u.24805

δ: Type ?u.24808

e: LocalEquiv α β

e': LocalEquiv β γ

LocalEquiv.symm (LocalEquiv.symm e) = erfl
Goals accomplished! 🐙
#align local_equiv.symm_symm LocalEquiv.symm_symm: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), LocalEquiv.symm (LocalEquiv.symm e) = e
LocalEquiv.symm_symm

theorem image_source_eq_target: e.toFun '' e.source = e.target
image_source_eq_target : e: LocalEquiv α β
e '' e: LocalEquiv α β
e.source: {α : Type ?u.25055} → {β : Type ?u.25054} → LocalEquiv α β → Set α
source = e: LocalEquiv α β
e.target: {α : Type ?u.25062} → {β : Type ?u.25061} → LocalEquiv α β → Set β
target :=
  e: LocalEquiv α β
e.bijOn: ∀ {α : Type ?u.25069} {β : Type ?u.25070} (e : LocalEquiv α β), BijOn e.toFun e.source e.target
bijOn.image_eq: ∀ {α : Type ?u.25075} {β : Type ?u.25076} {s : Set α} {t : Set β} {f : α → β}, BijOn f s t → f '' s = t
image_eq
#align local_equiv.image_source_eq_target LocalEquiv.image_source_eq_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), e.toFun '' e.source = e.target
LocalEquiv.image_source_eq_target

theorem forall_mem_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {p : β → Prop},
  (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)
forall_mem_target {p: β → Prop
p : β: Type ?u.25109
β → Prop: Type
Prop} : (∀ y: ?m.25131
y ∈ e: LocalEquiv α β
e.target: {α : Type ?u.25151} → {β : Type ?u.25150} → LocalEquiv α β → Set β
target, p: β → Prop
p y: ?m.25131
y) ↔ ∀ x: ?m.25173
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.25193} → {β : Type ?u.25192} → LocalEquiv α β → Set α
source, p: β → Prop
p (e: LocalEquiv α β
e x: ?m.25173
x) := by
Goals accomplished! 🐙
  α: Type u_2

β: Type u_1

γ: Type ?u.25112

δ: Type ?u.25115

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)rw [α: Type u_2

β: Type u_1

γ: Type ?u.25112

δ: Type ?u.25115

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)← image_source_eq_target: ∀ {α : Type ?u.25248} {β : Type ?u.25247} (e : LocalEquiv α β), e.toFun '' e.source = e.target
image_source_eq_target,α: Type u_2

β: Type u_1

γ: Type ?u.25112

δ: Type ?u.25115

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∀ (y : β), y ∈ e.toFun '' e.source → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x) α: Type u_2

β: Type u_1

γ: Type ?u.25112

δ: Type ?u.25115

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)ball_image_iff: ∀ {α : Type ?u.25274} {β : Type ?u.25275} {f : α → β} {s : Set α} {p : β → Prop},
  (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
ball_image_iffα: Type u_2

β: Type u_1

γ: Type ?u.25112

δ: Type ?u.25115

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∀ (x : α), x ∈ e.source → p (toFun e x)) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)]
Goals accomplished! 🐙
#align local_equiv.forall_mem_target LocalEquiv.forall_mem_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {p : β → Prop},
  (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)
LocalEquiv.forall_mem_target

theorem exists_mem_target: ∀ {p : β → Prop}, (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)
exists_mem_target {p: β → Prop
p : β: Type ?u.25343
β → Prop: Type
Prop} : (∃ y: ?m.25367
y ∈ e: LocalEquiv α β
e.target: {α : Type ?u.25375} → {β : Type ?u.25374} → LocalEquiv α β → Set β
target, p: β → Prop
p y: ?m.25367
y) ↔ ∃ x: ?m.25398
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.25406} → {β : Type ?u.25405} → LocalEquiv α β → Set α
source, p: β → Prop
p (e: LocalEquiv α β
e x: ?m.25398
x) := by
Goals accomplished! 🐙
  α: Type u_2

β: Type u_1

γ: Type ?u.25346

δ: Type ?u.25349

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)rw [α: Type u_2

β: Type u_1

γ: Type ?u.25346

δ: Type ?u.25349

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)← image_source_eq_target: ∀ {α : Type ?u.25460} {β : Type ?u.25459} (e : LocalEquiv α β), e.toFun '' e.source = e.target
image_source_eq_target,α: Type u_2

β: Type u_1

γ: Type ?u.25346

δ: Type ?u.25349

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∃ y, y ∈ e.toFun '' e.source ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x) α: Type u_2

β: Type u_1

γ: Type ?u.25346

δ: Type ?u.25349

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)bex_image_iff: ∀ {α : Type ?u.25480} {β : Type ?u.25481} {f : α → β} {s : Set α} {p : β → Prop},
  (∃ y, y ∈ f '' s ∧ p y) ↔ ∃ x, x ∈ s ∧ p (f x)
bex_image_iffα: Type u_2

β: Type u_1

γ: Type ?u.25346

δ: Type ?u.25349

e: LocalEquiv α β

e': LocalEquiv β γ

p: β → Prop

(∃ x, x ∈ e.source ∧ p (toFun e x)) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)]
Goals accomplished! 🐙
#align local_equiv.exists_mem_target LocalEquiv.exists_mem_target: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β) {p : β → Prop},
  (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (toFun e x)
LocalEquiv.exists_mem_target

/-- We say that `t : Set β` is an image of `s : Set α` under a local equivalence if
any of the following equivalent conditions hold:

* `e '' (e.source ∩ s) = e.target ∩ t`;
* `e.source ∩ e ⁻¹ t = e.source ∩ s`;
* `∀ x ∈ e.source, e x ∈ t ↔ x ∈ s` (this one is used in the definition).
-/
def IsImage: Set α → Set β → Prop
IsImage (s: Set α
s : Set: Type ?u.25557 → Type ?u.25557
Set α: Type ?u.25537
α) (t: Set β
t : Set: Type ?u.25560 → Type ?u.25560
Set β: Type ?u.25540
β) : Prop: Type
Prop :=
  ∀ ⦃x: ?m.25567
x⦄, x: ?m.25567
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.25587} → {β : Type ?u.25586} → LocalEquiv α β → Set α
source → (e: LocalEquiv α β
e x: ?m.25567
x ∈ t: Set β
t ↔ x: ?m.25567
x ∈ s: Set α
s)
#align local_equiv.is_image LocalEquiv.IsImage: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → Set α → Set β → Prop
LocalEquiv.IsImage

namespace IsImage

variable {e: ?m.25701
e} {s: Set α
s : Set: Type ?u.26593 → Type ?u.26593
Set α: Type ?u.25681
α} {t: Set β
t : Set: Type ?u.25707 → Type ?u.25707
Set β: Type ?u.25684
β} {x: α
x : α: Type ?u.25681
α} {y: β
y : β: Type ?u.25684
β}

theorem apply_mem_iff: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {x : α},
  IsImage e s t → x ∈ e.source → (toFun e x ∈ t ↔ x ∈ s)
apply_mem_iff (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.25745} → {β : Type ?u.25744} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) (hx: x ∈ e.source
hx : x: α
x ∈ e: LocalEquiv α β
e.source: {α : Type ?u.25777} → {β : Type ?u.25776} → LocalEquiv α β → Set α
source) : e: LocalEquiv α β
e x: α
x ∈ t: Set β
t ↔ x: α
x ∈ s: Set α
s :=
  h: IsImage e s t
h hx: x ∈ e.source
hx
#align local_equiv.is_image.apply_mem_iff LocalEquiv.IsImage.apply_mem_iff: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {x : α},
  IsImage e s t → x ∈ e.source → (toFun e x ∈ t ↔ x ∈ s)
LocalEquiv.IsImage.apply_mem_iff

theorem symm_apply_mem_iff: IsImage e s t → ∀ ⦃y : β⦄, y ∈ e.target → (toFun (LocalEquiv.symm e) y ∈ s ↔ y ∈ t)
symm_apply_mem_iff (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.25899} → {β : Type ?u.25898} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : ∀ ⦃y: ?m.25916
y⦄, y: ?m.25916
y ∈ e: LocalEquiv α β
e.target: {α : Type ?u.25936} → {β : Type ?u.25935} → LocalEquiv α β → Set β
target → (e: LocalEquiv α β
e.symm: {α : Type ?u.25958} → {β : Type ?u.25957} → LocalEquiv α β → LocalEquiv β α
symm y: ?m.25916
y ∈ s: Set α
s ↔ y: ?m.25916
y ∈ t: Set β
t) :=
  e: LocalEquiv α β
e.forall_mem_target: ∀ {α : Type ?u.26022} {β : Type ?u.26021} (e : LocalEquiv α β) {p : β → Prop},
  (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (toFun e x)
forall_mem_target.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr fun x: ?m.26043
x hx: ?m.26046
hx => by
Goals accomplished! 🐙 α: Type u_1

β: Type u_2

γ: Type ?u.25874

δ: Type ?u.25877

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x✝: α

y: β

h: IsImage e s t

x: α

hx: x ∈ e.source

toFun (LocalEquiv.symm e) (toFun e x) ∈ s ↔ toFun e x ∈ trw [α: Type u_1

β: Type u_2

γ: Type ?u.25874

δ: Type ?u.25877

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x✝: α

y: β

h: IsImage e s t

x: α

hx: x ∈ e.source

toFun (LocalEquiv.symm e) (toFun e x) ∈ s ↔ toFun e x ∈ te: LocalEquiv α β
e.left_inv: ∀ {α : Type ?u.26055} {β : Type ?u.26056} (e : LocalEquiv α β) {x : α},
  x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = x
left_inv hx: x ∈ e.source
hx,α: Type u_1

β: Type u_2

γ: Type ?u.25874

δ: Type ?u.25877

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x✝: α

y: β

h: IsImage e s t

x: α

hx: x ∈ e.source

x ∈ s ↔ toFun e x ∈ t α: Type u_1

β: Type u_2

γ: Type ?u.25874

δ: Type ?u.25877

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x✝: α

y: β

h: IsImage e s t

x: α

hx: x ∈ e.source

toFun (LocalEquiv.symm e) (toFun e x) ∈ s ↔ toFun e x ∈ th: IsImage e s t
h hx: x ∈ e.source
hxα: Type u_1

β: Type u_2

γ: Type ?u.25874

δ: Type ?u.25877

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x✝: α

y: β

h: IsImage e s t

x: α

hx: x ∈ e.source

x ∈ s ↔ x ∈ s]
Goals accomplished! 🐙
#align local_equiv.is_image.symm_apply_mem_iff LocalEquiv.IsImage.symm_apply_mem_iff: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → ∀ ⦃y : β⦄, y ∈ e.target → (toFun (LocalEquiv.symm e) y ∈ s ↔ y ∈ t)
LocalEquiv.IsImage.symm_apply_mem_iff

protected theorem symm: IsImage e s t → IsImage (LocalEquiv.symm e) t s
symm (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.26135} → {β : Type ?u.26134} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : e: LocalEquiv α β
e.symm: {α : Type ?u.26152} → {β : Type ?u.26151} → LocalEquiv α β → LocalEquiv β α
symm.IsImage: {α : Type ?u.26156} → {β : Type ?u.26155} → LocalEquiv α β → Set α → Set β → Prop
IsImage t: Set β
t s: Set α
s :=
  h: IsImage e s t
h.symm_apply_mem_iff: ∀ {α : Type ?u.26171} {β : Type ?u.26172} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → ∀ ⦃y : β⦄, y ∈ e.target → (toFun (LocalEquiv.symm e) y ∈ s ↔ y ∈ t)
symm_apply_mem_iff
#align local_equiv.is_image.symm LocalEquiv.IsImage.symm: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → IsImage (LocalEquiv.symm e) t s
LocalEquiv.IsImage.symm

@[simp]
theorem symm_iff: ∀ {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage (LocalEquiv.symm e) t s ↔ IsImage e s t
symm_iff : e: LocalEquiv α β
e.symm: {α : Type ?u.26243} → {β : Type ?u.26242} → LocalEquiv α β → LocalEquiv β α
symm.IsImage: {α : Type ?u.26249} → {β : Type ?u.26248} → LocalEquiv α β → Set α → Set β → Prop
IsImage t: Set β
t s: Set α
s ↔ e: LocalEquiv α β
e.IsImage: {α : Type ?u.26264} → {β : Type ?u.26263} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t :=
  ⟨fun h: ?m.26284
h => h: ?m.26284
h.symm: ∀ {α : Type ?u.26286} {β : Type ?u.26287} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → IsImage (LocalEquiv.symm e) t s
symm, fun h: ?m.26324
h => h: ?m.26324
h.symm: ∀ {α : Type ?u.26326} {β : Type ?u.26327} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → IsImage (LocalEquiv.symm e) t s
symm⟩
#align local_equiv.is_image.symm_iff LocalEquiv.IsImage.symm_iff: ∀ {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage (LocalEquiv.symm e) t s ↔ IsImage e s t
LocalEquiv.IsImage.symm_iff

protected theorem mapsTo: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo e.toFun (e.source ∩ s) (e.target ∩ t)
mapsTo (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.26411} → {β : Type ?u.26410} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : MapsTo: {α : Type ?u.26428} → {β : Type ?u.26427} → (α → β) → Set α → Set β → Prop
MapsTo e: LocalEquiv α β
e (e: LocalEquiv α β
e.source: {α : Type ?u.26473} → {β : Type ?u.26472} → LocalEquiv α β → Set α
source ∩ s: Set α
s) (e: LocalEquiv α β
e.target: {α : Type ?u.26494} → {β : Type ?u.26493} → LocalEquiv α β → Set β
target ∩ t: Set β
t) :=
  fun _: ?m.26510
_ hx: ?m.26513
hx => ⟨e: LocalEquiv α β
e.mapsTo: ∀ {α : Type ?u.26523} {β : Type ?u.26524} (e : LocalEquiv α β), MapsTo e.toFun e.source e.target
mapsTo hx: ?m.26513
hx.1: ∀ {a b : Prop}, a ∧ b → a
1, (h: IsImage e s t
h hx: ?m.26513
hx.1: ∀ {a b : Prop}, a ∧ b → a
1).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hx: ?m.26513
hx.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align local_equiv.is_image.maps_to LocalEquiv.IsImage.mapsTo: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo e.toFun (e.source ∩ s) (e.target ∩ t)
LocalEquiv.IsImage.mapsTo

theorem symm_mapsTo: IsImage e s t → MapsTo (LocalEquiv.symm e).toFun (e.target ∩ t) (e.source ∩ s)
symm_mapsTo (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.26604} → {β : Type ?u.26603} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : MapsTo: {α : Type ?u.26621} → {β : Type ?u.26620} → (α → β) → Set α → Set β → Prop
MapsTo e: LocalEquiv α β
e.symm: {α : Type ?u.26625} → {β : Type ?u.26624} → LocalEquiv α β → LocalEquiv β α
symm (e: LocalEquiv α β
e.target: {α : Type ?u.26675} → {β : Type ?u.26674} → LocalEquiv α β → Set β
target ∩ t: Set β
t) (e: LocalEquiv α β
e.source: {α : Type ?u.26696} → {β : Type ?u.26695} → LocalEquiv α β → Set α
source ∩ s: Set α
s) :=
  h: IsImage e s t
h.symm: ∀ {α : Type ?u.26711} {β : Type ?u.26712} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → IsImage (LocalEquiv.symm e) t s
symm.mapsTo: ∀ {α : Type ?u.26729} {β : Type ?u.26730} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo e.toFun (e.source ∩ s) (e.target ∩ t)
mapsTo
#align local_equiv.is_image.symm_maps_to LocalEquiv.IsImage.symm_mapsTo: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo (LocalEquiv.symm e).toFun (e.target ∩ t) (e.source ∩ s)
LocalEquiv.IsImage.symm_mapsTo

/-- Restrict a `LocalEquiv` to a pair of corresponding sets. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : IsImage e s t),
  (restr h).target = e.target ∩ t
simps (config := { fullyApplied := false: Bool
false })]
def restr: {α : Type u_1} → {β : Type u_2} → {e : LocalEquiv α β} → {s : Set α} → {t : Set β} → IsImage e s t → LocalEquiv α β
restr (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.26809} → {β : Type ?u.26808} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : LocalEquiv: Type ?u.26826 → Type ?u.26825 → Type (max?u.26826?u.26825)
LocalEquiv α: Type ?u.26778
α β: Type ?u.26781
β where
  toFun := e: LocalEquiv α β
e
  invFun := e: LocalEquiv α β
e.symm: {α : Type ?u.26867} → {β : Type ?u.26866} → LocalEquiv α β → LocalEquiv β α
symm
  source := e: LocalEquiv α β
e.source: {α : Type ?u.26917} → {β : Type ?u.26916} → LocalEquiv α β → Set α
source ∩ s: Set α
s
  target := e: LocalEquiv α β
e.target: {α : Type ?u.26938} → {β : Type ?u.26937} → LocalEquiv α β → Set β
target ∩ t: Set β
t
  map_source' := h: IsImage e s t
h.mapsTo: ∀ {α : Type ?u.26950} {β : Type ?u.26951} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo e.toFun (e.source ∩ s) (e.target ∩ t)
mapsTo
  map_target' := h: IsImage e s t
h.symm_mapsTo: ∀ {α : Type ?u.26972} {β : Type ?u.26973} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → MapsTo (LocalEquiv.symm e).toFun (e.target ∩ t) (e.source ∩ s)
symm_mapsTo
  left_inv' := e: LocalEquiv α β
e.leftInvOn: ∀ {α : Type ?u.26987} {β : Type ?u.26988} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.source
leftInvOn.mono: ∀ {α : Type ?u.26991} {β : Type ?u.26992} {s s₁ : Set α} {f : α → β} {f' : β → α},
  LeftInvOn f' f s → s₁ ⊆ s → LeftInvOn f' f s₁
mono (inter_subset_left: ∀ {α : Type ?u.27028} (s t : Set α), s ∩ t ⊆ s
inter_subset_left _: Set ?m.27029
_ _: Set ?m.27029
_)
  right_inv' := e: LocalEquiv α β
e.rightInvOn: ∀ {α : Type ?u.27043} {β : Type ?u.27044} (e : LocalEquiv α β), RightInvOn (LocalEquiv.symm e).toFun e.toFun e.target
rightInvOn.mono: ∀ {α : Type ?u.27047} {β : Type ?u.27048} {t t₁ : Set β} {f : α → β} {f' : β → α},
  RightInvOn f' f t → t₁ ⊆ t → RightInvOn f' f t₁
mono (inter_subset_left: ∀ {α : Type ?u.27084} (s t : Set α), s ∩ t ⊆ s
inter_subset_left _: Set ?m.27085
_ _: Set ?m.27085
_)
#align local_equiv.is_image.restr LocalEquiv.IsImage.restr: {α : Type u_1} → {β : Type u_2} → {e : LocalEquiv α β} → {s : Set α} → {t : Set β} → IsImage e s t → LocalEquiv α β
LocalEquiv.IsImage.restr
#align local_equiv.is_image.restr_apply LocalEquiv.IsImage.restr_apply: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : IsImage e s t),
  (restr h).toFun = e.toFun
LocalEquiv.IsImage.restr_apply
#align local_equiv.is_image.restr_source LocalEquiv.IsImage.restr_source: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : IsImage e s t),
  (restr h).source = e.source ∩ s
LocalEquiv.IsImage.restr_source
#align local_equiv.is_image.restr_target LocalEquiv.IsImage.restr_target: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : IsImage e s t),
  (restr h).target = e.target ∩ t
LocalEquiv.IsImage.restr_target
#align local_equiv.is_image.restr_symm_apply LocalEquiv.IsImage.restr_symm_apply: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} (h : IsImage e s t),
  (LocalEquiv.symm (restr h)).toFun = (LocalEquiv.symm e).toFun
LocalEquiv.IsImage.restr_symm_apply

theorem image_eq: IsImage e s t → e.toFun '' (e.source ∩ s) = e.target ∩ t
image_eq (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.27499} → {β : Type ?u.27498} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : e: LocalEquiv α β
e '' (e: LocalEquiv α β
e.source: {α : Type ?u.27562} → {β : Type ?u.27561} → LocalEquiv α β → Set α
source ∩ s: Set α
s) = e: LocalEquiv α β
e.target: {α : Type ?u.27579} → {β : Type ?u.27578} → LocalEquiv α β → Set β
target ∩ t: Set β
t :=
  h: IsImage e s t
h.restr: {α : Type ?u.27595} →
  {β : Type ?u.27594} → {e : LocalEquiv α β} → {s : Set α} → {t : Set β} → IsImage e s t → LocalEquiv α β
restr.image_source_eq_target: ∀ {α : Type ?u.27613} {β : Type ?u.27612} (e : LocalEquiv α β), e.toFun '' e.source = e.target
image_source_eq_target
#align local_equiv.is_image.image_eq LocalEquiv.IsImage.image_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.toFun '' (e.source ∩ s) = e.target ∩ t
LocalEquiv.IsImage.image_eq

theorem symm_image_eq: IsImage e s t → (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s
symm_image_eq (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.27666} → {β : Type ?u.27665} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : e: LocalEquiv α β
e.symm: {α : Type ?u.27688} → {β : Type ?u.27687} → LocalEquiv α β → LocalEquiv β α
symm '' (e: LocalEquiv α β
e.target: {α : Type ?u.27738} → {β : Type ?u.27737} → LocalEquiv α β → Set β
target ∩ t: Set β
t) = e: LocalEquiv α β
e.source: {α : Type ?u.27755} → {β : Type ?u.27754} → LocalEquiv α β → Set α
source ∩ s: Set α
s :=
  h: IsImage e s t
h.symm: ∀ {α : Type ?u.27770} {β : Type ?u.27771} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → IsImage (LocalEquiv.symm e) t s
symm.image_eq: ∀ {α : Type ?u.27788} {β : Type ?u.27789} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.toFun '' (e.source ∩ s) = e.target ∩ t
image_eq
#align local_equiv.is_image.symm_image_eq LocalEquiv.IsImage.symm_image_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s
LocalEquiv.IsImage.symm_image_eq

theorem iff_preimage_eq: IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
iff_preimage_eq : e: LocalEquiv α β
e.IsImage: {α : Type ?u.27867} → {β : Type ?u.27866} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t ↔ e: LocalEquiv α β
e.source: {α : Type ?u.27886} → {β : Type ?u.27885} → LocalEquiv α β → Set α
source ∩ e: LocalEquiv α β
e ⁻¹' t: Set β
t = e: LocalEquiv α β
e.source: {α : Type ?u.27941} → {β : Type ?u.27940} → LocalEquiv α β → Set α
source ∩ s: Set α
s := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

γ: Type ?u.27842

δ: Type ?u.27845

e: LocalEquiv α β

e': LocalEquiv β γ

s: Set α

t: Set β

x: α

y: β

IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ ssimp only [IsImage: {α : Type ?u.27962} → {β : Type ?u.27961} → LocalEquiv α β → Set α → Set β → Prop
IsImage, ext_iff: ∀ {α : Type ?u.27964} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
ext_iff, mem_inter_iff: ∀ {α : Type ?u.27982} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b
mem_inter_iff, mem_preimage: ∀ {α : Type ?u.28010} {β : Type ?u.28009} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ s
mem_preimage, and_congr_right_iff: ∀ {a b c : Prop}, (a ∧ b ↔ a ∧ c) ↔ a → (b ↔ c)
and_congr_right_iff]
Goals accomplished! 🐙
#align local_equiv.is_image.iff_preimage_eq LocalEquiv.IsImage.iff_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
LocalEquiv.IsImage.iff_preimage_eq

alias iff_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
iff_preimage_eq ↔ preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
preimage_eq of_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.source ∩ e.toFun ⁻¹' t = e.source ∩ s → IsImage e s t
of_preimage_eq
#align local_equiv.is_image.of_preimage_eq LocalEquiv.IsImage.of_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.source ∩ e.toFun ⁻¹' t = e.source ∩ s → IsImage e s t
LocalEquiv.IsImage.of_preimage_eq
#align local_equiv.is_image.preimage_eq LocalEquiv.IsImage.preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
LocalEquiv.IsImage.preimage_eq

theorem iff_symm_preimage_eq: IsImage e s t ↔ e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t
iff_symm_preimage_eq : e: LocalEquiv α β
e.IsImage: {α : Type ?u.28325} → {β : Type ?u.28324} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t ↔ e: LocalEquiv α β
e.target: {α : Type ?u.28344} → {β : Type ?u.28343} → LocalEquiv α β → Set β
target ∩ e: LocalEquiv α β
e.symm: {α : Type ?u.28354} → {β : Type ?u.28353} → LocalEquiv α β → LocalEquiv β α
symm ⁻¹' s: Set α
s = e: LocalEquiv α β
e.target: {α : Type ?u.28408} → {β : Type ?u.28407} → LocalEquiv α β → Set β
target ∩ t: Set β
t :=
  symm_iff: ∀ {α : Type ?u.28417} {β : Type ?u.28416} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage (LocalEquiv.symm e) t s ↔ IsImage e s t
symm_iff.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans iff_preimage_eq: ∀ {α : Type ?u.28446} {β : Type ?u.28447} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
iff_preimage_eq
#align local_equiv.is_image.iff_symm_preimage_eq LocalEquiv.IsImage.iff_symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t
LocalEquiv.IsImage.iff_symm_preimage_eq

alias iff_symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t
iff_symm_preimage_eq ↔ symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t
symm_preimage_eq of_symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t → IsImage e s t
of_symm_preimage_eq
#align local_equiv.is_image.of_symm_preimage_eq LocalEquiv.IsImage.of_symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t → IsImage e s t
LocalEquiv.IsImage.of_symm_preimage_eq
#align local_equiv.is_image.symm_preimage_eq LocalEquiv.IsImage.symm_preimage_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t
LocalEquiv.IsImage.symm_preimage_eq

theorem of_image_eq: ∀ {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.toFun '' (e.source ∩ s) = e.target ∩ t → IsImage e s t
of_image_eq (h: e.toFun '' (e.source ∩ s) = e.target ∩ t
h : e: LocalEquiv α β
e '' (e: LocalEquiv α β
e.source: {α : Type ?u.28575} → {β : Type ?u.28574} → LocalEquiv α β → Set α
source ∩ s: Set α
s) = e: LocalEquiv α β
e.target: {α : Type ?u.28593} → {β : Type ?u.28592} → LocalEquiv α β → Set β
target ∩ t: Set β
t) : e: LocalEquiv α β
e.IsImage: {α : Type ?u.28610} → {β : Type ?u.28609} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t :=
  of_symm_preimage_eq: ∀ {α : Type ?u.28623} {β : Type ?u.28624} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t → IsImage e s t
of_symm_preimage_eq <| Eq.trans: ∀ {α : Sort ?u.28643} {a b c : α}, a = b → b = c → a = c
Eq.trans (of_symm_preimage_eq: ∀ {α : Type ?u.28651} {β : Type ?u.28652} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ t → IsImage e s t
of_symm_preimage_eq rfl: ∀ {α : Sort ?u.28658} {a : α}, a = a
rfl).image_eq: ∀ {α : Type ?u.28668} {β : Type ?u.28669} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → e.toFun '' (e.source ∩ s) = e.target ∩ t
image_eq.symm: ∀ {α : Sort ?u.28685} {a b : α}, a = b → b = a
symm h: e.toFun '' (e.source ∩ s) = e.target ∩ t
h
#align local_equiv.is_image.of_image_eq LocalEquiv.IsImage.of_image_eq: ∀ {α : Type u_2} {β : Type u_1} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.toFun '' (e.source ∩ s) = e.target ∩ t → IsImage e s t
LocalEquiv.IsImage.of_image_eq

theorem of_symm_image_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s → IsImage e s t
of_symm_image_eq (h: (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s
h : e: LocalEquiv α β
e.symm: {α : Type ?u.28753} → {β : Type ?u.28752} → LocalEquiv α β → LocalEquiv β α
symm '' (e: LocalEquiv α β
e.target: {α : Type ?u.28805} → {β : Type ?u.28804} → LocalEquiv α β → Set β
target ∩ t: Set β
t) = e: LocalEquiv α β
e.source: {α : Type ?u.28823} → {β : Type ?u.28822} → LocalEquiv α β → Set α
source ∩ s: Set α
s) : e: LocalEquiv α β
e.IsImage: {α : Type ?u.28840} → {β : Type ?u.28839} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t :=
  of_preimage_eq: ∀ {α : Type ?u.28853} {β : Type ?u.28854} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  e.source ∩ e.toFun ⁻¹' t = e.source ∩ s → IsImage e s t
of_preimage_eq <| Eq.trans: ∀ {α : Sort ?u.28873} {a b c : α}, a = b → b = c → a = c
Eq.trans (iff_preimage_eq: ∀ {α : Type ?u.28881} {β : Type ?u.28882} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ s
iff_preimage_eq.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 rfl: ∀ {α : Sort ?u.28892} {a : α}, a = a
rfl).symm_image_eq: ∀ {α : Type ?u.28902} {β : Type ?u.28903} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  IsImage e s t → (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s
symm_image_eq.symm: ∀ {α : Sort ?u.28919} {a b : α}, a = b → b = a
symm h: (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s
h
#align local_equiv.is_image.of_symm_image_eq LocalEquiv.IsImage.of_symm_image_eq: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β},
  (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ s → IsImage e s t
LocalEquiv.IsImage.of_symm_image_eq

protected theorem compl: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β}, IsImage e s t → IsImage e (sᶜ) (tᶜ)
compl (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.28982} → {β : Type ?u.28981} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) : e: LocalEquiv α β
e.IsImage: {α : Type ?u.28999} → {β : Type ?u.28998} → LocalEquiv α β → Set α → Set β → Prop
IsImage (s: Set α
sᶜ) (t: Set β
tᶜ) := fun _: ?m.29069
_ hx: ?m.29072
hx => not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr (h: IsImage e s t
h hx: ?m.29072
hx)
#align local_equiv.is_image.compl LocalEquiv.IsImage.compl: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β}, IsImage e s t → IsImage e (sᶜ) (tᶜ)
LocalEquiv.IsImage.compl

protected theorem inter: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  IsImage e s t → IsImage e s' t' → IsImage e (s ∩ s') (t ∩ t')
inter {s': ?m.29133
s' t': ?m.29136
t'} (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29140} → {β : Type ?u.29139} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) (h': IsImage e s' t'
h' : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29157} → {β : Type ?u.29156} → LocalEquiv α β → Set α → Set β → Prop
IsImage s': ?m.29133
s' t': ?m.29136
t') :
    e: LocalEquiv α β
e.IsImage: {α : Type ?u.29168} → {β : Type ?u.29167} → LocalEquiv α β → Set α → Set β → Prop
IsImage (s: Set α
s ∩ s': ?m.29133
s') (t: Set β
t ∩ t': ?m.29136
t') := fun _: ?m.29220
_ hx: ?m.29223
hx => and_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)
and_congr (h: IsImage e s t
h hx: ?m.29223
hx) (h': IsImage e s' t'
h' hx: ?m.29223
hx)
#align local_equiv.is_image.inter LocalEquiv.IsImage.inter: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  IsImage e s t → IsImage e s' t' → IsImage e (s ∩ s') (t ∩ t')
LocalEquiv.IsImage.inter

protected theorem union: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  IsImage e s t → IsImage e s' t' → IsImage e (s ∪ s') (t ∪ t')
union {s': Set α
s' t': Set β
t'} (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29297} → {β : Type ?u.29296} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) (h': IsImage e s' t'
h' : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29314} → {β : Type ?u.29313} → LocalEquiv α β → Set α → Set β → Prop
IsImage s': ?m.29290
s' t': ?m.29293
t') :
    e: LocalEquiv α β
e.IsImage: {α : Type ?u.29325} → {β : Type ?u.29324} → LocalEquiv α β → Set α → Set β → Prop
IsImage (s: Set α
s ∪ s': ?m.29290
s') (t: Set β
t ∪ t': ?m.29293
t') := fun _: ?m.29377
_ hx: ?m.29380
hx => or_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)
or_congr (h: IsImage e s t
h hx: ?m.29380
hx) (h': IsImage e s' t'
h' hx: ?m.29380
hx)
#align local_equiv.is_image.union LocalEquiv.IsImage.union: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  IsImage e s t → IsImage e s' t' → IsImage e (s ∪ s') (t ∪ t')
LocalEquiv.IsImage.union

protected theorem diff: ∀ {α : Type u_1} {β : Type u_2} {e : LocalEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  IsImage e s t → IsImage e s' t' → IsImage e (s \ s') (t \ t')
diff {s': ?m.29447
s' t': Set β
t'} (h: IsImage e s t
h : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29454} → {β : Type ?u.29453} → LocalEquiv α β → Set α → Set β → Prop
IsImage s: Set α
s t: Set β
t) (h': IsImage e s' t'
h' : e: LocalEquiv α β
e.IsImage: {α : Type ?u.29471} → {β : Type ?u.29470} → LocalEquiv α β → Set α → Set β → Prop
IsImage s': ?m.29447
s' t': ?m.29450
t') :
    e: LocalEquiv α β
e.IsImage: {α : Type ?u.29482} → {β : Type ?u.29481} → LocalEquiv α β → Set α → Set β → Prop
IsImage (s: Set α
s \ s': ?m.29447
s') (t: Set β
t \ t': ?m.29450
t') :=
  h: IsImage e s t
h.inter: ∀ {α : Type ?u.29555} {