Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
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 = aid.def Function.comp.left_id: ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), id ∘ f = fFunction.comp.left_id Set.mem_setOf_eq: ∀ {α : Type u} {x : α} {p : α → Prop}, (x ∈ { y | p y }) = p xSet.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 = aSet.univ_inter Set.preimage_univ: ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, f ⁻¹' Set.univ = Set.univSet.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 ↔ pand_true_iff Set.mem_univ: ∀ {α : Type u} (x : α), x ∈ Set.univSet.mem_univ Set.mem_image_of_mem: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' aSet.mem_image_of_mem true_and_iff: ∀ (p : Prop), True ∧ p ↔ ptrue_and_iff
Set.mem_inter_iff: ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ bSet.mem_inter_iff Set.mem_preimage: ∀ {α : Type u_2} {β : Type u_1} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ sSet.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 ⊆ sSet.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 ∈ tSet.mem_prod
Set.range_id: ∀ {α : Type u_1}, Set.range id = Set.univSet.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 ↔ pand_self_iff Set.mem_range_self: ∀ {α : Type u_1} {ι : Sort u_2} {f : ι → α} (i : ι), f i ∈ Set.range fSet.mem_range_self eq_self_iff_true: ∀ {α : Sort u_1} (a : α), a = a ↔ Trueeq_self_iff_true forall_const: ∀ {b : Prop} (α : Sort u_1) [i : Nonempty α], α → b ↔ bforall_const
forall_true_iff: ∀ {α : Sort u_1}, α → True ↔ Trueforall_true_iff Set.inter_univ: ∀ {α : Type u} (a : Set α), a ∩ Set.univ = aSet.inter_univ Set.preimage_id: ∀ {α : Type u_1} {s : Set α}, id ⁻¹' s = sSet.preimage_id Function.comp.right_id: ∀ {α : Sort u₁} {β : Sort u₂} (f : α → β), f ∘ id = fFunction.comp.right_id not_false_iff: ¬False ↔ Truenot_false_iff and_imp: ∀ {a b c : Prop}, a ∧ b → c ↔ a → b → cand_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.univSet.univ_prod_univ true_or_iff: ∀ (p : Prop), True ∨ p ↔ Truetrue_or_iff or_true_iff: ∀ (p : Prop), p ∨ True ↔ Trueor_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 ⁻¹' tSet.preimage_inter
heq_iff_eq: ∀ {α : Sort u_1} {a b : α}, HEq a b ↔ a = bheq_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 } = aSubtype.coe_mk
Equiv.toFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ↑eEquiv.toFun_as_coe Equiv.invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symmEquiv.invFun_as_coe

/-- Common `@[simps]` configuration options used for manifold-related declarations. -/
def mfld_cfg: Simps.Configmfld_cfg : Simps.Config: TypeSimps.Config where
attrs := [`mfld_simps: Name`mfld_simps]
fullyApplied := false: Boolfalse
#align mfld_cfg mfld_cfg: Simps.Configmfld_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: ParserDescrmfldSetTac) "mfld_set_tac" : tactic: Parser.Categorytactic => withMainContext: {α : Type} → TacticM α → TacticM αwithMainContext do
let g: ?m.947g ← getMainGoal: TacticM MVarIdgetMainGoal
let goalTy: ?m.1302goalTy := (← instantiateMVars (← g.getDecl).type): ?m.1299(← instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m ExprinstantiateMVars(← instantiateMVars (← g.getDecl).type): ?m.1299 (← g.getDecl): ?m.1174(← g: ?m.947g(← g.getDecl): ?m.1174.getDecl: MVarId → MetaM MetavarDeclgetDecl(← g.getDecl): ?m.1174)(← instantiateMVars (← g.getDecl).type): ?m.1299.type: MetavarDecl → Exprtype(← instantiateMVars (← g.getDecl).type): ?m.1299).getAppFnArgs: Expr → Name × Array ExprgetAppFnArgs
match goalTy: ?m.1302goalTy with
| (``Eq: Name``Eq: {α : Sort u_1} → α → α → PropEq, #[_ty: Expr_ty, _e₁: Expr_e₁, _e₂: Expr_e₂]) =>
evalTactic: Syntax → TacticM UnitevalTactic (← `(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.1412apply`(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.1412intro`(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.1412constructor`(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.1412intro`(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.1412try`(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.1412simp`(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.1412only`(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.1412at`(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.1412simp`(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.1412only`(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 α] → α → α → PropSubset, #[_ty: Expr_ty, _inst: Expr_inst, _e₁: Expr_e₁, _e₂: Expr_e₂]) =>
evalTactic: Syntax → TacticM UnitevalTactic (← `(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.2649intro`(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.2649try`(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.2649simp`(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.2649only`(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.2649at`(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.2649simp`(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.2649only`(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.3027throwErrorthrowError "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) = pand_true eq_self_iff_true: ∀ {α : Sort u_1} (a : α), a = a ↔ Trueeq_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.16177Set α: 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.16180Set β: 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.targetmap_source' : ∀ ⦃x: ?m.16184x⦄, x: ?m.16184x ∈ source: Set αsource → toFun: α → βtoFun x: ?m.16184x ∈ 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.sourcemap_target' : ∀ ⦃x: ?m.16248x⦄, x: ?m.16248x ∈ target: Set βtarget → invFun: β → αinvFun x: ?m.16248x ∈ 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) = xleft_inv' : ∀ ⦃x: ?m.16304x⦄, x: ?m.16304x ∈ source: Set αsource → invFun: β → αinvFun (toFun: α → βtoFun x: ?m.16304x) = x: ?m.16304x
/-- 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) = xright_inv' : ∀ ⦃x: ?m.16338x⦄, x: ?m.16338x ∈ target: Set βtarget → toFun: α → βtoFun (invFun: β → αinvFun x: ?m.16338x) = x: ?m.16338x
#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 ∅ tmapsTo_empty _: ?m.17716 → ?m.17717_ _: Set ?m.17717_, mapsTo_empty: ∀ {α : Type ?u.17738} {β : Type ?u.17737} (f : α → β) (t : Set β), MapsTo f ∅ tmapsTo_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.sourcemap_target'
map_target' := e: LocalEquiv α βe.map_source': ∀ {α : Type ?u.17967} {β : Type ?u.17966} (self : LocalEquiv α β) ⦃x : α⦄, x ∈ self.source → toFun self x ∈ self.targetmap_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) = xright_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) = xleft_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 =     gcoe_symm_mk (f: α → βf : α: Type ?u.18725α → β: Type ?u.18728β) (g: ?m.18749g s: Set αs t: Set βt ml: ?m.18758ml mr: ?m.18761mr il: ?m.18764il ir: ∀ ⦃x : β⦄, x ∈ t → f (g x) = xir) :
((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.18749g s: ?m.18752s t: ?m.18755t ml: ?m.18758ml mr: ?m.18761mr il: ?m.18764il ir: ?m.18767ir).symm: {α : Type ?u.18808} → {β : Type ?u.18807} → LocalEquiv α β → LocalEquiv β αsymm : β: Type ?u.18728β → α: Type ?u.18725α) = g: ?m.18749g :=
rfl: ∀ {α : Sort ?u.18866} {a : α}, a = arfl
#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 =     gLocalEquiv.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).toFuninvFun_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 = arfl
#align local_equiv.inv_fun_as_coe LocalEquiv.invFun_as_coe: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), e.invFun = (LocalEquiv.symm e).toFunLocalEquiv.invFun_as_coe

@[simp, mfld_simps]
theorem map_source: ∀ {x : α}, x ∈ e.source → toFun e x ∈ e.targetmap_source {x: αx : α: Type ?u.19263α} (h: x ∈ e.sourceh : 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.targetmap_source' h: x ∈ e.sourceh
#align local_equiv.map_source LocalEquiv.map_source: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.targetLocalEquiv.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.sourcemap_target {x: βx : β: Type ?u.19456β} (h: x ∈ e.targeth : 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.sourcemap_target' h: x ∈ e.targeth
#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.sourceLocalEquiv.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) = xleft_inv {x: αx : α: Type ?u.19659α} (h: x ∈ e.sourceh : 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) = xleft_inv' h: x ∈ e.sourceh
#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) = xLocalEquiv.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) = xright_inv {x: βx : β: Type ?u.19845β} (h: x ∈ e.targeth : 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) = xright_inv' h: x ∈ e.targeth
#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) = xLocalEquiv.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.sourcehx : x: αx ∈ e: LocalEquiv α βe.source: {α : Type ?u.20066} → {β : Type ?u.20065} → LocalEquiv α β → Set αsource) (hy: y ∈ e.targethy : 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.20205h => byGoals accomplished! 🐙 α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: x = toFun (LocalEquiv.symm e) ytoFun e x = yrw [α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: x = toFun (LocalEquiv.symm e) ytoFun 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) = xright_inv hy: y ∈ e.targethy,α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: x = toFun (LocalEquiv.symm e) ytoFun e x = toFun e (toFun (LocalEquiv.symm e) y) α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: x = toFun (LocalEquiv.symm e) ytoFun e x = yh: x = toFun (LocalEquiv.symm e) yhα: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: x = toFun (LocalEquiv.symm e) ytoFun e (toFun (LocalEquiv.symm e) y) = toFun e (toFun (LocalEquiv.symm e) y)]Goals accomplished! 🐙, fun h: ?m.20212h => byGoals accomplished! 🐙 α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: toFun e x = yx = toFun (LocalEquiv.symm e) yrw [α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: toFun e x = yx = 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) = xleft_inv hx: x ∈ e.sourcehx,α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: toFun e x = ytoFun (LocalEquiv.symm e) (toFun e x) = toFun (LocalEquiv.symm e) y α: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: toFun e x = yx = toFun (LocalEquiv.symm e) yh: toFun e x = yhα: Type u_1β: Type u_2γ: Type ?u.20032δ: Type ?u.20035e: LocalEquiv α βe': LocalEquiv β γx: αy: βhx: x ∈ e.sourcehy: y ∈ e.targeth: toFun e x = ytoFun (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.targetmapsTo : MapsTo: {α : Type ?u.20307} → {β : Type ?u.20306} → (α → β) → Set α → Set β → PropMapsTo 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.targetmap_source
#align local_equiv.maps_to LocalEquiv.mapsTo: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), MapsTo e.toFun e.source e.targetLocalEquiv.mapsTo

theorem symm_mapsTo: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), MapsTo (LocalEquiv.symm e).toFun e.target e.sourcesymm_mapsTo : MapsTo: {α : Type ?u.20408} → {β : Type ?u.20407} → (α → β) → Set α → Set β → PropMapsTo 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.targetmapsTo
#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.sourceLocalEquiv.symm_mapsTo

protected theorem leftInvOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), LeftInvOn (LocalEquiv.symm e).toFun e.toFun e.sourceleftInvOn : LeftInvOn: {α : Type ?u.20518} → {β : Type ?u.20517} → (β → α) → (α → β) → Set α → PropLeftInvOn 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) = xleft_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.sourceLocalEquiv.leftInvOn

protected theorem rightInvOn: RightInvOn (LocalEquiv.symm e).toFun e.toFun e.targetrightInvOn : RightInvOn: {α : Type ?u.20658} → {β : Type ?u.20657} → (β → α) → (α → β) → Set β → PropRightInvOn 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) = xright_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.targetLocalEquiv.rightInvOn

protected theorem invOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InvOn (LocalEquiv.symm e).toFun e.toFun e.source e.targetinvOn : InvOn: {α : Type ?u.20798} → {β : Type ?u.20797} → (β → α) → (α → β) → Set α → Set β → PropInvOn 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.sourceleftInvOn, e: LocalEquiv α βe.rightInvOn: ∀ {α : Type ?u.20918} {β : Type ?u.20919} (e : LocalEquiv α β), RightInvOn (LocalEquiv.symm e).toFun e.toFun e.targetrightInvOn⟩
#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.targetLocalEquiv.invOn

protected theorem injOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InjOn e.toFun e.sourceinjOn : InjOn: {α : Type ?u.20960} → {β : Type ?u.20959} → (α → β) → Set α → PropInjOn 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.sourceleftInvOn.injOn: ∀ {α : Type ?u.21011} {β : Type ?u.21012} {s : Set α} {f : α → β} {f₁' : β → α}, LeftInvOn f₁' f s → InjOn f sinjOn
#align local_equiv.inj_on LocalEquiv.injOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), InjOn e.toFun e.sourceLocalEquiv.injOn

protected theorem bijOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), BijOn e.toFun e.source e.targetbijOn : BijOn: {α : Type ?u.21071} → {β : Type ?u.21070} → (α → β) → Set α → Set β → PropBijOn 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.targetinvOn.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 tbijOn e: LocalEquiv α βe.mapsTo: ∀ {α : Type ?u.21167} {β : Type ?u.21168} (e : LocalEquiv α β), MapsTo e.toFun e.source e.targetmapsTo e: LocalEquiv α βe.symm_mapsTo: ∀ {α : Type ?u.21185} {β : Type ?u.21184} (e : LocalEquiv α β), MapsTo (LocalEquiv.symm e).toFun e.target e.sourcesymm_mapsTo
#align local_equiv.bij_on LocalEquiv.bijOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), BijOn e.toFun e.source e.targetLocalEquiv.bijOn

protected theorem surjOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), SurjOn e.toFun e.source e.targetsurjOn : SurjOn: {α : Type ?u.21226} → {β : Type ?u.21225} → (α → β) → Set α → Set β → PropSurjOn 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.targetbijOn.surjOn: ∀ {α : Type ?u.21283} {β : Type ?u.21284} {s : Set α} {t : Set β} {f : α → β}, BijOn f s t → SurjOn f s tsurjOn
#align local_equiv.surj_on LocalEquiv.surjOn: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), SurjOn e.toFun e.source e.targetLocalEquiv.surjOn

/-- Associate a `LocalEquiv` to an `Equiv`. -/
@[simps: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).toFun = ↑esimps (config := mfld_cfg: Simps.Configmfld_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 ∈ univmem_univ _: ?m.21512_
map_target' _: ?m.21526_ _: ?m.21529_ := mem_univ: ∀ {α : Type ?u.21531} (x : α), x ∈ univmem_univ _: ?m.21532_
left_inv' x: ?m.21546x _: ?m.21549_ := e: α ≃ βe.left_inv: ∀ {α : Sort ?u.21552} {β : Sort ?u.21551} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv x: ?m.21546x
right_inv' x: ?m.21564x _: ?m.21567_ := e: α ≃ βe.right_inv: ∀ {α : Sort ?u.21570} {β : Sort ?u.21569} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv x: ?m.21564x
#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.symmEquiv.toLocalEquiv_symm_apply
#align equiv.to_local_equiv_target Equiv.toLocalEquiv_target: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).target = univEquiv.toLocalEquiv_target
#align equiv.to_local_equiv_apply Equiv.toLocalEquiv_apply: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).toFun = ↑eEquiv.toLocalEquiv_apply
#align equiv.to_local_equiv_source Equiv.toLocalEquiv_source: ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (Equiv.toLocalEquiv e).source = univEquiv.toLocalEquiv_source

instance inhabitedOfEmpty: {α : Type u_1} → {β : Type u_2} → [inst : IsEmpty α] → [inst : IsEmpty β] → Inhabited (LocalEquiv α β)inhabitedOfEmpty [IsEmpty: Sort ?u.21971 → PropIsEmpty α: Type ?u.21951α] [IsEmpty: Sort ?u.21974 → PropIsEmpty β: 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 α] → α ≃ EmptyEquiv.equivEmpty α: Type ?u.21951α).trans: {α : Sort ?u.21995} → {β : Sort ?u.21994} → {γ : Sort ?u.21993} → α ≃ β → β ≃ γ → α ≃ γtrans (Equiv.equivEmpty: (α : Sort ?u.22006) → [inst : IsEmpty α] → α ≃ EmptyEquiv.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 = tsimps (config := { fullyApplied := false: Boolfalse })]
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 = fhf : ⇑e: LocalEquiv α βe = f: α → βf) (g: β → αg : β: Type ?u.22096β → α: Type ?u.22093α) (hg: (LocalEquiv.symm e).toFun = ghg : ⇑e: LocalEquiv α βe.symm: {α : Type ?u.22166} → {β : Type ?u.22165} → LocalEquiv α β → LocalEquiv β αsymm = g: β → αg) (s: Set αs : Set: Type ?u.22210 → Type ?u.22210Set α: Type ?u.22093α)
(hs: e.source = shs : 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.22224Set β: Type ?u.22096β) (ht: e.target = tht : 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 = tht ▸ hs: e.source = shs ▸ hf: e.toFun = fhf ▸ e: LocalEquiv α βe.map_source: ∀ {α : Type ?u.22265} {β : Type ?u.22266} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.targetmap_source
map_target' _: ?m.22317_ := hs: e.source = shs ▸ ht: e.target = tht ▸ hg: (LocalEquiv.symm e).toFun = ghg ▸ e: LocalEquiv α βe.map_target: ∀ {α : Type ?u.22320} {β : Type ?u.22319} (e : LocalEquiv α β) {x : β},
x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.sourcemap_target
left_inv' _: ?m.22371_ := hs: e.source = shs ▸ hf: e.toFun = fhf ▸ hg: (LocalEquiv.symm e).toFun = ghg ▸ e: LocalEquiv α βe.left_inv: ∀ {α : Type ?u.22373} {β : Type ?u.22374} (e : LocalEquiv α β) {x : α},
x ∈ e.source → toFun (LocalEquiv.symm e) (toFun e x) = xleft_inv
right_inv' _: ?m.22428_ := ht: e.target = tht ▸ hf: e.toFun = fhf ▸ hg: (LocalEquiv.symm e).toFun = ghg ▸ e: LocalEquiv α βe.right_inv: ∀ {α : Type ?u.22431} {β : Type ?u.22430} (e : LocalEquiv α β) {x : β},
x ∈ e.target → toFun e (toFun (LocalEquiv.symm e) x) = xright_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 = sLocalEquiv.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 = fLocalEquiv.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 = gLocalEquiv.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 = tLocalEquiv.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 = ecopy_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 = fhf : ⇑e: LocalEquiv α βe = f: α → βf) (g: β → αg : β: Type ?u.22997β → α: Type ?u.22994α) (hg: (LocalEquiv.symm e).toFun = ghg : ⇑e: LocalEquiv α βe.symm: {α : Type ?u.23067} → {β : Type ?u.23066} → LocalEquiv α β → LocalEquiv β αsymm = g: β → αg)
(s: Set αs : Set: Type ?u.23111 → Type ?u.23111Set α: Type ?u.22994α) (hs: e.source = shs : 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.23125Set β: Type ?u.22997β) (ht: e.target = tht : 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 = fhf g: β → αg hg: (LocalEquiv.symm e).toFun = ghg s: Set αs hs: e.source = shs t: Set βt ht: e.target = tht = e: LocalEquiv α βe := byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.23000δ: Type ?u.23003e✝: LocalEquiv α βe': LocalEquiv β γe: LocalEquiv α βf: α → βhf: e.toFun = fg: β → αhg: (LocalEquiv.symm e).toFun = gs: Set αhs: e.source = st: Set βht: e.target = tcopy 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.23003e✝: 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.23003e✝: LocalEquiv α βe': LocalEquiv β γe: LocalEquiv α βf: α → βhf: e.toFun = fg: β → αhg: (LocalEquiv.symm e).toFun = gs: Set αhs: e.source = st: Set βht: e.target = tcopy e f hf g hg s hs t ht = ecases e: LocalEquiv α βeα: Type u_1β: Type u_2γ: Type ?u.23000δ: Type ?u.23003e: 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) = xright_inv'✝: ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = xmkcopy
{ 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.23003e✝: LocalEquiv α βe': LocalEquiv β γe: LocalEquiv α βf: α → βhf: e.toFun = fg: β → αhg: (LocalEquiv.symm e).toFun = gs: Set αhs: e.source = st: Set βht: e.target = tcopy e f hf g hg s hs t ht = erflGoals 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 = eLocalEquiv.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.targettoEquiv : 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.23717x := ⟨e: LocalEquiv α βe x: ?m.23717x, e: LocalEquiv α βe.map_source: ∀ {α : Type ?u.23841} {β : Type ?u.23842} (e : LocalEquiv α β) {x : α}, x ∈ e.source → toFun e x ∈ e.targetmap_source x: ?m.23717x.mem: ∀ {α : Type ?u.23860} {s : Set α} (p : ↑s), ↑p ∈ smem⟩
invFun y: ?m.23872y := ⟨e: LocalEquiv α βe.symm: {α : Type ?u.23887} → {β : Type ?u.23886} → LocalEquiv α β → LocalEquiv β αsymm y: ?m.23872y, e: LocalEquiv α βe.map_target: ∀ {α : Type ?u.24006} {β : Type ?u.24005} (e : LocalEquiv α β) {x : β},
x ∈ e.target → toFun (LocalEquiv.symm e) x ∈ e.sourcemap_target y: ?m.23872y.mem: ∀ {α : Type ?u.24024} {s : Set α} (p : ↑s), ↑p ∈ smem⟩
left_inv := fun ⟨_, hx: val✝ ∈ e.sourcehx⟩ => Subtype.eq: ∀ {α : Type ?u.24083} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.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) = xleft_inv hx: val✝ ∈ e.sourcehx
right_inv := fun ⟨_, hy: val✝ ∈ e.targethy⟩ => Subtype.eq: ∀ {α : Type ?u.24241} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.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) = xright_inv hy: val✝ ∈ e.targethy
#align local_equiv.to_equiv LocalEquiv.toEquiv: {α : Type u_1} → {β : Type u_2} → (e : LocalEquiv α β) → ↑e.source ≃ ↑e.targetLocalEquiv.toEquiv

@[simp, mfld_simps]
theorem symm_source: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), (LocalEquiv.symm e).source = e.targetsymm_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 = arfl
#align local_equiv.symm_source LocalEquiv.symm_source: ∀ {α : Type u_2} {β : Type u_1} (e : LocalEquiv α β), (LocalEquiv.symm e).source = e.targetLocalEquiv.symm_source

@[simp, mfld_simps]
theorem symm_target: (LocalEquiv.symm e).target = e.sourcesymm_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 = arfl
#align local_equiv.symm_target LocalEquiv.symm_target: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), (LocalEquiv.symm e).target = e.sourceLocalEquiv.symm_target

@[simp, mfld_simps]
theorem symm_symm: LocalEquiv.symm (LocalEquiv.symm e) = esymm_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 := byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.24805δ: Type ?u.24808e: LocalEquiv α βe': LocalEquiv β γLocalEquiv.symm (LocalEquiv.symm e) = ecases e: LocalEquiv α βeα: Type u_1β: Type u_2γ: Type ?u.24805δ: Type ?u.24808e': 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) = xright_inv'✝: ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = xmkLocalEquiv.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.24808e: LocalEquiv α βe': LocalEquiv β γLocalEquiv.symm (LocalEquiv.symm e) = erflGoals accomplished! 🐙
#align local_equiv.symm_symm LocalEquiv.symm_symm: ∀ {α : Type u_1} {β : Type u_2} (e : LocalEquiv α β), LocalEquiv.symm (LocalEquiv.symm e) = eLocalEquiv.symm_symm

theorem image_source_eq_target: e.toFun '' e.source = e.targetimage_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.targetbijOn.image_eq: ∀ {α : Type ?u.25075} {β : Type ?u.25076} {s : Set α} {t : Set β} {f : α → β}, BijOn f s t → f '' s = timage_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.targetLocalEquiv.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: β → Propp : β: Type ?u.25109β → Prop: TypeProp} : (∀ y: ?m.25131y ∈ e: LocalEquiv α βe.target: {α : Type ?u.25151} → {β : Type ?u.25150} → LocalEquiv α β → Set βtarget, p: β → Propp y: ?m.25131y) ↔ ∀ x: ?m.25173x ∈ e: LocalEquiv α βe.source: {α : Type ?u.25193} → {β : Type ?u.25192} → LocalEquiv α β → Set αsource, p: β → Propp (e: LocalEquiv α βe x: ?m.25173x) := byGoals accomplished! 🐙
α: Type u_2β: Type u_1γ: Type ?u.25112δ: Type ?u.25115e: 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.25115e: 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.targetimage_source_eq_target,α: Type u_2β: Type u_1γ: Type ?u.25112δ: Type ?u.25115e: 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.25115e: 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.25115e: 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: β → Propp : β: Type ?u.25343β → Prop: TypeProp} : (∃ y: ?m.25367y ∈ e: LocalEquiv α βe.target: {α : Type ?u.25375} → {β : Type ?u.25374} → LocalEquiv α β → Set βtarget, p: β → Propp y: ?m.25367y) ↔ ∃ x: ?m.25398x ∈ e: LocalEquiv α βe.source: {α : Type ?u.25406} → {β : Type ?u.25405} → LocalEquiv α β → Set αsource, p: β → Propp (e: LocalEquiv α βe x: ?m.25398x) := byGoals accomplished! 🐙
α: Type u_2β: Type u_1γ: Type ?u.25346δ: Type ?u.25349e: 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.25349e: 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.targetimage_source_eq_target,α: Type u_2β: Type u_1γ: Type ?u.25346δ: Type ?u.25349e: 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.25349e: 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.25349e: 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 β → PropIsImage (s: Set αs : Set: Type ?u.25557 → Type ?u.25557Set α: Type ?u.25537α) (t: Set βt : Set: Type ?u.25560 → Type ?u.25560Set β: Type ?u.25540β) : Prop: TypeProp :=
∀ ⦃x: ?m.25567x⦄, x: ?m.25567x ∈ e: LocalEquiv α βe.source: {α : Type ?u.25587} → {β : Type ?u.25586} → LocalEquiv α β → Set αsource → (e: LocalEquiv α βe x: ?m.25567x ∈ t: Set βt ↔ x: ?m.25567x ∈ s: Set αs)
#align local_equiv.is_image LocalEquiv.IsImage: {α : Type u_1} → {β : Type u_2} → LocalEquiv α β → Set α → Set β → PropLocalEquiv.IsImage

namespace IsImage

variable {e: ?m.25701e} {s: Set αs : Set: Type ?u.26593 → Type ?u.26593Set α: Type ?u.25681α} {t: Set βt : Set: Type ?u.25707 → Type ?u.25707Set β: 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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.25745} → {β : Type ?u.25744} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt) (hx: x ∈ e.sourcehx : 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 th hx: x ∈ e.sourcehx
#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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.25899} → {β : Type ?u.25898} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt) : ∀ ⦃y: ?m.25916y⦄, y: ?m.25916y ∈ 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.25916y ∈ s: Set αs ↔ y: ?m.25916y ∈ 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 → ampr fun x: ?m.26043x hx: ?m.26046hx => byGoals accomplished! 🐙 α: Type u_1β: Type u_2γ: Type ?u.25874δ: Type ?u.25877e: LocalEquiv α βe': LocalEquiv β γs: Set αt: Set βx✝: αy: βh: IsImage e s tx: αhx: x ∈ e.sourcetoFun (LocalEquiv.symm e) (toFun e x) ∈ s ↔ toFun e x ∈ trw [α: Type u_1β: Type u_2γ: Type ?u.25874δ: Type ?u.25877e: LocalEquiv α βe': LocalEquiv β γs: Set αt: Set βx✝: αy: βh: IsImage e s tx: αhx: x ∈ e.sourcetoFun (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) = xleft_inv hx: x ∈ e.sourcehx,α: Type u_1β: Type u_2γ: Type ?u.25874δ: Type ?u.25877e: LocalEquiv α βe': LocalEquiv β γs: Set αt: Set βx✝: αy: βh: IsImage e s tx: αhx: x ∈ e.sourcex ∈ s ↔ toFun e x ∈ t α: Type u_1β: Type u_2γ: Type ?u.25874δ: Type ?u.25877e: LocalEquiv α βe': LocalEquiv β γs: Set αt: Set βx✝: αy: βh: IsImage e s tx: αhx: x ∈ e.sourcetoFun (LocalEquiv.symm e) (toFun e x) ∈ s ↔ toFun e x ∈ th: IsImage e s th hx: x ∈ e.sourcehxα: Type u_1β: Type u_2γ: Type ?u.25874δ: Type ?u.25877e: LocalEquiv α βe': LocalEquiv β γs: Set αt: Set βx✝: αy: βh: IsImage e s tx: αhx: x ∈ e.sourcex ∈ 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 ssymm (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.26135} → {β : Type ?u.26134} → LocalEquiv α β → Set α → Set β → PropIsImage 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 β → PropIsImage t: Set βt s: Set αs :=
h: IsImage e s th.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 sLocalEquiv.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 tsymm_iff : e: LocalEquiv α βe.symm: {α : Type ?u.26243} → {β : Type ?u.26242} → LocalEquiv α β → LocalEquiv β αsymm.IsImage: {α : Type ?u.26249} → {β : Type ?u.26248} → LocalEquiv α β → Set α → Set β → PropIsImage t: Set βt s: Set αs ↔ e: LocalEquiv α βe.IsImage: {α : Type ?u.26264} → {β : Type ?u.26263} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt :=
⟨fun h: ?m.26284h => h: ?m.26284h.symm: ∀ {α : Type ?u.26286} {β : Type ?u.26287} {e : LocalEquiv α β} {s : Set α} {t : Set β},
IsImage e s t → IsImage (LocalEquiv.symm e) t ssymm, fun h: ?m.26324h => h: ?m.26324h.symm: ∀ {α : Type ?u.26326} {β : Type ?u.26327} {e : LocalEquiv α β} {s : Set α} {t : Set β},
IsImage e s t → IsImage (LocalEquiv.symm e) t ssymm⟩
#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 tLocalEquiv.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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.26411} → {β : Type ?u.26410} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt) : MapsTo: {α : Type ?u.26428} → {β : Type ?u.26427} → (α → β) → Set α → Set β → PropMapsTo 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.26513hx => ⟨e: LocalEquiv α βe.mapsTo: ∀ {α : Type ?u.26523} {β : Type ?u.26524} (e : LocalEquiv α β), MapsTo e.toFun e.source e.targetmapsTo hx: ?m.26513hx.1: ∀ {a b : Prop}, a ∧ b → a1, (h: IsImage e s th hx: ?m.26513hx.1: ∀ {a b : Prop}, a ∧ b → a1).2: ∀ {a b : Prop}, (a ↔ b) → b → a2 hx: ?m.26513hx.2: ∀ {a b : Prop}, a ∧ b → b2⟩
#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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.26604} → {β : Type ?u.26603} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt) : MapsTo: {α : Type ?u.26621} → {β : Type ?u.26620} → (α → β) → Set α → Set β → PropMapsTo 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 th.symm: ∀ {α : Type ?u.26711} {β : Type ?u.26712} {e : LocalEquiv α β} {s : Set α} {t : Set β},
IsImage e s t → IsImage (LocalEquiv.symm e) t ssymm.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 ∩ tsimps (config := { fullyApplied := false: Boolfalse })]
def restr: {α : Type u_1} → {β : Type u_2} → {e : LocalEquiv α β} → {s : Set α} → {t : Set β} → IsImage e s t → LocalEquiv α βrestr (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.26809} → {β : Type ?u.26808} → LocalEquiv α β → Set α → Set β → PropIsImage 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 th.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 th.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.sourceleftInvOn.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 ⊆ sinter_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.targetrightInvOn.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 ⊆ sinter_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.toFunLocalEquiv.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 ∩ sLocalEquiv.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 ∩ tLocalEquiv.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).toFunLocalEquiv.IsImage.restr_symm_apply

theorem image_eq: IsImage e s t → e.toFun '' (e.source ∩ s) = e.target ∩ timage_eq (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.27499} → {β : Type ?u.27498} → LocalEquiv α β → Set α → Set β → PropIsImage 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 th.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.targetimage_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 ∩ tLocalEquiv.IsImage.image_eq

theorem symm_image_eq: IsImage e s t → (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ ssymm_image_eq (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.27666} → {β : Type ?u.27665} → LocalEquiv α β → Set α → Set β → PropIsImage 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 th.symm: ∀ {α : Type ?u.27770} {β : Type ?u.27771} {e : LocalEquiv α β} {s : Set α} {t : Set β},
IsImage e s t → IsImage (LocalEquiv.symm e) t ssymm.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 ∩ timage_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 ∩ sLocalEquiv.IsImage.symm_image_eq

theorem iff_preimage_eq: IsImage e s t ↔ e.source ∩ e.toFun ⁻¹' t = e.source ∩ siff_preimage_eq : e: LocalEquiv α βe.IsImage: {α : Type ?u.27867} → {β : Type ?u.27866} → LocalEquiv α β → Set α → Set β → PropIsImage 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 := byGoals accomplished! 🐙
α: Type u_1β: Type u_2γ: Type ?u.27842δ: Type ?u.27845e: 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 β → PropIsImage, ext_iff: ∀ {α : Type ?u.27964} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ text_iff, mem_inter_iff: ∀ {α : Type ?u.27982} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ bmem_inter_iff, mem_preimage: ∀ {α : Type ?u.28010} {β : Type ?u.28009} {f : α → β} {s : Set β} {a : α}, a ∈ f ⁻¹' s ↔ f a ∈ smem_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 ∩ sLocalEquiv.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 ∩ siff_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 ∩ spreimage_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 tof_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 tLocalEquiv.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 ∩ sLocalEquiv.IsImage.preimage_eq

theorem iff_symm_preimage_eq: IsImage e s t ↔ e.target ∩ (LocalEquiv.symm e).toFun ⁻¹' s = e.target ∩ tiff_symm_preimage_eq : e: LocalEquiv α βe.IsImage: {α : Type ?u.28325} → {β : Type ?u.28324} → LocalEquiv α β → Set α → Set β → PropIsImage 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 tsymm_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 ∩ siff_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 ∩ tLocalEquiv.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 ∩ tiff_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 ∩ tsymm_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 tof_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 tLocalEquiv.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 ∩ tLocalEquiv.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 tof_image_eq (h: e.toFun '' (e.source ∩ s) = e.target ∩ th : 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 β → PropIsImage 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 tof_symm_preimage_eq <| Eq.trans: ∀ {α : Sort ?u.28643} {a b c : α}, a = b → b = c → a = cEq.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 tof_symm_preimage_eq rfl: ∀ {α : Sort ?u.28658} {a : α}, a = arfl).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 ∩ timage_eq.symm: ∀ {α : Sort ?u.28685} {a b : α}, a = b → b = asymm h: e.toFun '' (e.source ∩ s) = e.target ∩ th
#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 tLocalEquiv.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 tof_symm_image_eq (h: (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ sh : 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 β → PropIsImage 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 tof_preimage_eq <| Eq.trans: ∀ {α : Sort ?u.28873} {a b c : α}, a = b → b = c → a = cEq.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 ∩ siff_preimage_eq.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 rfl: ∀ {α : Sort ?u.28892} {a : α}, a = arfl).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 ∩ ssymm_image_eq.symm: ∀ {α : Sort ?u.28919} {a b : α}, a = b → b = asymm h: (LocalEquiv.symm e).toFun '' (e.target ∩ t) = e.source ∩ sh
#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 tLocalEquiv.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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.28982} → {β : Type ?u.28981} → LocalEquiv α β → Set α → Set β → PropIsImage s: Set αs t: Set βt) : e: LocalEquiv α βe.IsImage: {α : Type ?u.28999} → {β : Type ?u.28998} → LocalEquiv α β → Set α → Set β → PropIsImage (s: Set αsᶜ) (t: Set βtᶜ) := fun _: ?m.29069_ hx: ?m.29072hx => not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr (h: IsImage e s th hx: ?m.29072hx)
#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.29133s' t': ?m.29136t'} (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.29140} → {β : Type ?u.29139} → LocalEquiv α β → Set α → Set β → PropIsImage 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 β → PropIsImage s': ?m.29133s' t': ?m.29136t') :
e: LocalEquiv α βe.IsImage: {α : Type ?u.29168} → {β : Type ?u.29167} → LocalEquiv α β → Set α → Set β → PropIsImage (s: Set αs ∩ s': ?m.29133s') (t: Set βt ∩ t': ?m.29136t') := fun _: ?m.29220_ hx: ?m.29223hx => and_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)and_congr (h: IsImage e s th hx: ?m.29223hx) (h': IsImage e s' t'h' hx: ?m.29223hx)
#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 th : e: LocalEquiv α βe.IsImage: {α : Type ?u.29297} → {β : Type ?u.29296} → LocalEquiv α β → Set α → Set β → PropIsImage 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 β → PropIsImage s': ?m.29290s' t': ?m.29293t') :
e: LocalEquiv α βe.IsImage: {α : Type ?u.29325} → {β : Type ?u.29324} → LocalEquiv α β → Set α → Set β → PropIsImage (s: Set αs ∪ s': ?m.29290s') (t: Set βt ∪ t': ?m.29293t') := fun _: ?m.29377_ hx: ?m.29380hx => or_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)or_congr (h: IsImage e s th hx: ?m.29380hx) (h': IsImage e s' t'h' hx: ?m.29380hx)
#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.29447s' t': Set βt'} (h: IsImage e s th : e: LocalEquiv α βe.IsImage: {α : Type ?u.29454} → {β : Type ?u.29453} → LocalEquiv α β → Set α → Set β → PropIsImage 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 β → PropIsImage s': ?m.29447s' t': ?m.29450t') :
e: LocalEquiv α βe.IsImage: {α : Type ?u.29482} → {β : Type ?u.29481} → LocalEquiv α β → Set α → Set β → PropIsImage (s: Set αs \ s': ?m.29447s') (t: Set βt \ t': ?m.29450t') :=
h: IsImage e s th.inter: ∀ {α : Type ?u.29555} {```