awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
  (he'f' : e' = f'.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
inr :
  ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr₁ : ∀ (f' : OpenPartialHomeomorph M' H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f')
  (he'f' : e' = f'.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : f.symm ≫ₕ f' ∈ contDiffGroupoid n I
Tactic: rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry ∈ contDiffGroupoid n I
Tactic: rw [hef, he'f']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I
have inr : (OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry).source = ∅
Tactic: apply ContDiffGroupoid.mem_of_source_eq_empty
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅
have inr : ∀ (x : H),
  x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry).source ↔
    Membership.mem (γ := Set H) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
  (he'f' : e' = f'.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
inr :
  ∀ (f' : OpenPartialHomeomorph M H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f')
    (he'f' : e' = f'.lift_openEmbedding ⋯), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr₁ : ∀ (f' : OpenPartialHomeomorph M' H) (hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f')
  (he'f' : e' = f'.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry ∈ contDiffGroupoid n I
Tactic: rw [hef, he'f']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯ ∈ contDiffGroupoid n I
have inr : (OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry).source = ∅
Tactic: apply ContDiffGroupoid.mem_of_source_eq_empty
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ (OpenPartialHomeomorph.symm (f.lift_openEmbedding ⋯) ≫ₕ f'.lift_openEmbedding ⋯).source = ∅
have inr : ∀ (x : H),
  x ∈ (OpenPartialHomeomorph.symm (f.lift_openEmbedding sorry) ≫ₕ f'.lift_openEmbedding sorry).source ↔
    Membership.mem (γ := Set H) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (M ⊕ M') H)) (atlas H (M ⊕ M')) e'
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : f.symm ≫ₕ f' ∈ contDiffGroupoid n I
Tactic: rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inr]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).source = f.source
have rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
Tactic: rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
⊢ (f.extend I).source = f.source
have rw₁ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' I.source = f.source
Tactic: rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
rw₁ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' I.source = f.source
⊢ (f.extend I).source = f.source
have rw₂ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' univ = f.source
Tactic: rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
rw₁ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' I.source = f.source
rw₂ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' univ = f.source
⊢ (f.extend I).source = f.source
have rw₃ : f.source ∩ univ = f.source
Tactic: rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).source = f.source
rw₁ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' I.source = f.source
rw₂ : f.source ∩ (↑f.toPartialEquiv : M → H) ⁻¹' univ = f.source
rw₃ : f.source ∩ univ = f.source
⊢ (f.extend I).source = f.source
have rw₄ : f.source = f.source
Tactic: rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst_4] (f.extend I).source
have rw : IsOpen[inst_4] f.source
Tactic: rw [extend_source]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
have simp_rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
Tactic: simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
⊢ (f.extend I).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
have simp_rw₁ : I.target ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
Tactic: simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₁ : I.target ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
⊢ (f.extend I).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
have simp_rw₂ : range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
Tactic: simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
simp_rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₁ : I.target ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
simp_rw₂ : range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
⊢ (f.extend I).target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
have simp_rw₃ : range (↑I : H → E) ∩ (↑I.symm : E → H) ⁻¹' f.target = (↑I.symm : E → H) ⁻¹' f.target ∩ range (↑I : H → E)
Tactic: simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target = (↑I : H → E) '' f.target
have rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
Tactic: rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
⊢ (f.extend I).target = (↑I : H → E) '' f.target
have rw₁ : (↑I.toPartialEquiv : H → E) '' (I.source ∩ f.target) = (↑I : H → E) '' f.target
Tactic: rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
rw₁ : (↑I.toPartialEquiv : H → E) '' (I.source ∩ f.target) = (↑I : H → E) '' f.target
⊢ (f.extend I).target = (↑I : H → E) '' f.target
have rw₂ : (↑I.toPartialEquiv : H → E) '' (univ ∩ f.target) = (↑I : H → E) '' f.target
Tactic: rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.ExtChartAt (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (f.toPartialEquiv ≫ I.toPartialEquiv).target = (↑I : H → E) '' f.target
rw₁ : (↑I.toPartialEquiv : H → E) '' (I.source ∩ f.target) = (↑I : H → E) '' f.target
rw₂ : (↑I.toPartialEquiv : H → E) '' (univ ∩ f.target) = (↑I : H → E) '' f.target
⊢ (f.extend I).target = (↑I : H → E) '' f.target
have rw₃ : (↑I.toPartialEquiv : H → E) '' f.target = (↑I : H → E) '' f.target
Tactic: rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]