awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
⊢ ContMDiffAt.{u_1, u_3, u_5, u_7, u_2, u_4, u_6} J I (M' := M) n
    (⇑{ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : M ≃ N }.symm : (a : N) → M) y
have hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
Tactic: obtain ⟨hx, hfx⟩ := hyp x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
⊢ ContMDiffAt.{u_1, u_3, u_5, u_7, u_2, u_4, u_6} J I (M' := M) n
    (⇑{ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : M ≃ N }.symm : (a : N) → M) y
have apply : y ∈ (Φ x).target
Tactic: apply ((Φ x).symm.contMDiffOn.congr (aux x)).contMDiffAt (((Φ x).open_target).mem_nhds ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x_1 : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : (x : M) → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv : N → M) (Φ x).target
y : N
x : M := g y
hx : x ∈ (Φ x).source
hfx : EqOn f (↑(Φ x).toPartialEquiv : M → N) (Φ x).source
⊢ y ∈ (Φ x).target
have this : y = (↑(Φ x).toPartialEquiv : M → N) x
Tactic: have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Function.LeftInverse.{u_2 + 1, u_3 + 1} (α := TangentSpace I x) (β := TangentSpace J (f x))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace J (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace J (f x))
have hinv : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
  (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
    (mfderiv% f x))
  (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
Tactic: apply ContinuousLinearMap.leftInverse_of_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
    (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
      (mfderiv% f x))
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
have hinv : Eq (α := TangentSpace I x →L[𝕜] TangentSpace I x)
  (ContinuousLinearMap.comp (M₂ := TangentSpace J (f x)) (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x))
    (mfderiv% f x))
  (mfderiv% ((↑hf.localInverse.toPartialEquiv : N → M) ∘ f) x)
Tactic: rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_left.mfderiv_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Function.RightInverse.{u_2 + 1, u_3 + 1} (α := TangentSpace I x) (β := TangentSpace J (f x))
    (⇑(mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)) :
      (a : TangentSpace J (f x)) → TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (⇑(mfderiv% f x) : (a : TangentSpace I x) → TangentSpace J (f x))
have hinv : Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
  (ContinuousLinearMap.id 𝕜 (TangentSpace J (f x)))
Tactic: apply ContinuousLinearMap.rightInverse_of_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.id 𝕜 (TangentSpace J (f x)))
have hinv : Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
  (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))
Tactic: rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_right.mfderiv_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))
have hf' : MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
Tactic: have hf' : MDifferentiableAt I J f (hf.localInverse (f x)) := by
      rw [hf.localInverse_left_inv hf.localInverse_mem_target]
      exact hf.mdifferentiableAt hn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hf' : MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))
have hinv : Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% f ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
Tactic: rw [mfderiv_comp _ hf' (hf.localInverse_mdifferentiableAt hn),
      hf.localInverse_left_inv hf.localInverse_mem_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalDiffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_4
inst_5 : TopologicalSpace H
G : Type u_5
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.17
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
hf' : MDiffAt f ((↑hf.localInverse.toPartialEquiv : N → M) (f x))
hinv :
  Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
      (mfderiv% f ((↑hf.localInverse.toPartialEquiv : N → M) (f x)))
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
⊢ Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
      (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
    (mfderiv% (f ∘ (↑hf.localInverse.toPartialEquiv : N → M)) (f x))
have hinv₁ : Eq (α := TangentSpace J (f x) →L[𝕜] TangentSpace J (f x))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
  (ContinuousLinearMap.comp (M₂ := TangentSpace I x) (mfderiv% f x)
    (mfderiv% (↑hf.localInverse.toPartialEquiv : N → M) (f x)))
Tactic: rw [mfderiv_comp _ hf' (hf.localInverse_mdifferentiableAt hn),
      hf.localInverse_left_inv hf.localInverse_mem_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
⊢ P f s x ↔ P f t x
have obtain : ∀ (o : Set H) (host : o ⊆ {x : H | (fun (x : H) ↦ x ∈ s ↔ x ∈ t) x}) (ho : IsOpen[inst] o) (hxo : x ∈ o),
  P f s x ↔ P f t x
Tactic: obtain ⟨o, host, ho, hxo⟩ := mem_nhds_iff.mp hu.mem_iff
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x : H | (fun (x : H) ↦ x ∈ s ↔ x ∈ t) x}
ho : IsOpen[inst] o
hxo : x ∈ o
⊢ P f s x ↔ P f t x
have host₁ : s ∩ o = t ∩ o
Tactic: simp_rw [subset_def, mem_setOf, ← and_congr_left_iff, ← mem_inter_iff, ← Set.ext_iff] at host
Cleared hypotheses: host
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f s x ↔ P f t x
have rw : P f (s ∩ o) x ↔ P f t x
Tactic: rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
rw : P f (s ∩ o) x ↔ P f t x
⊢ P f s x ↔ P f t x
have rw₁ : P f (t ∩ o) x ↔ P f t x
Tactic: rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
rw : P f (s ∩ o) x ↔ P f t x
rw₁ : P f (t ∩ o) x ↔ P f t x
⊢ P f s x ↔ P f t x
have rw₂ : P f t x ↔ P f t x
Tactic: rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f g : H → H'
h1 : f =ᶠ[𝓝[s] x] g
h2 : f x = g x
⊢ P f s x ↔ P g s x
have simp_rw : P f (s ∩ {x : H | f x = g x}) x ↔ P g (s ∩ {x : H | f x = g x}) x
Tactic: simp_rw [hG.is_local_nhds h1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
⊢ P ((↑e' : H' → H') ∘ f) s x ↔ P f s x
have h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
Tactic: have h2f := hfs.preimage_mem_nhdsWithin (e'.open_source.mem_nhds hxe')
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
⊢ P ((↑e' : H' → H') ∘ f) s x ↔ P f s x
have h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
Tactic: have h3f :=
    ((e'.continuousAt hxe').comp_continuousWithinAt hfs).preimage_mem_nhdsWithin <|
      e'.symm.open_source.mem_nhds <| e'.mapsTo hxe'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P ((↑e' : H' → H') ∘ f) s x ↔ P f s x
have mp : P ((↑e' : H' → H') ∘ f) s x → P f s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
mp : P ((↑e' : H' → H') ∘ f) s x → P f s x
⊢ P ((↑e' : H' → H') ∘ f) s x ↔ P f s x
have mpr : P f s x → P ((↑e' : H' → H') ∘ f) s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) s x
⊢ P f s x
have h₁ : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
Tactic: rw [hG.is_local_nhds h3f] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
⊢ P f s x
have mp : ∀ (h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x), P f s x
Tactic: have h2 := hG.left_invariance' (G'.symm he') inter_subset_right (e'.mapsTo hxe') h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (hypothesis)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
⊢ P f s x
have h2₁ : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
Tactic: rw [← hG.is_local_nhds h3f] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P ((↑e' : H' → H') ∘ f) (s ∩ (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source) x
h2 : P ((↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f) s x
⊢ P f s x
have mp : (↑e'.symm : H' → H') ∘ (↑e' : H' → H') ∘ f =ᶠ[𝓝[s] x] f
Tactic: refine hG.congr_nhdsWithin ?_ (e'.left_inv hxe') h2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : (↑e' : H' → H') ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f s x → P ((↑e' : H' → H') ∘ f) s x
have mpr : P f (s ∩ f ⁻¹' e'.source) x → P ((↑e' : H' → H') ∘ f) (s ∩ f ⁻¹' e'.source) x
Tactic: simp_rw [hG.is_local_nhds h2f]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
⊢ P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x) ↔ P f s x
have refine : ∀ (h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)), P f s x
Tactic: refine ⟨fun h ↦ ?_, hG.right_invariance' he hxe⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.LocalInvariantProperties (goal)
Goal:
H : Type u_1
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ G
hxe : x ∈ e.source
h : P (f ∘ (↑e.symm : H → H)) ((↑e.symm : H → H) ⁻¹' s) ((↑e : H → H) x)
⊢ P f s x
have have : ∀
  (this :
    P ((f ∘ (↑e.symm : H → H)) ∘ (↑e.symm.symm : H → H)) ((↑e.symm.symm : H → H) ⁻¹' (↑e.symm : H → H) ⁻¹' s)
      ((↑e.symm : H → H) ((↑e : H → H) x))),
  P f s x
Tactic: have := hG.right_invariance' (G.symm he) (e.mapsTo hxe) h