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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
⊢ e.symm.source ∩ (↑e.symm : H → M) ⁻¹' e'.source = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅
have rw : e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅ = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅
Tactic: rw [eq_empty_of_isEmpty (e'.source)]
-- 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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
⊢ e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅ = e.symm.source ∩ ∅
have rw : e.symm.source ∩ ∅ = e.symm.source ∩ ∅
Tactic: rw [preimage_empty]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H)) t x
have this : (e.symm ≫ₕ e').source = ∅
Tactic: have : (e.symm ≫ₕ e').source = ∅ := calc (e.symm ≫ₕ e').source
    _ = (e.symm.source) ∩ e.symm ⁻¹' e'.source := by rw [← OpenPartialHomeomorph.trans_source]
    _ = (e.symm.source) ∩ e.symm ⁻¹' ∅ := by rw [eq_empty_of_isEmpty (e'.source)]
    _ = (e.symm.source) ∩ ∅ := by rw [preimage_empty]
    _ = ∅ := inter_empty e.symm.source
-- 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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ t = (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
have rw : Eq (α := Set { x : E // x ∈ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source })
  (Subtype.val (p := fun (x : E) ↦ x ∈ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source) ⁻¹' range (↑I : H → E))
  (Subtype.val (p := fun (x : E) ↦ x ∈ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source) ⁻¹' range (↑I : H → E))
Tactic: rw [← Subtype.preimage_val_eq_preimage_val_iff]
-- 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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
have rw : (↑I.symm : E → H) ⁻¹' ∅ ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
Tactic: rw [this, preimage_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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
rw : (↑I.symm : E → H) ⁻¹' ∅ ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
⊢ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
have rw₁ : ∅ ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
Tactic: rw [this, preimage_empty]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
x : E
t : Set E := (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
hx : x ∈ t
this : (e.symm ≫ₕ e').source = ∅
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H)) t x
have this₁ : t = ∅
Tactic: have : t = ∅ := calc t
    _ = I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I := by
      rw [← Subtype.preimage_val_eq_preimage_val_iff]
    _ = ∅ ∩ range I := by rw [this, preimage_empty]
    _ = ∅ := empty_inter (range I)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
n : ℕ∞ω
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
𝕜 : Type u_5
inst_6 : NontriviallyNormedField 𝕜
E : Type u_6
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
E' : Type u_7
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H : Type u_8
inst_11 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst_12 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : IsManifold I n M
M' : Type u_11
inst_16 : TopologicalSpace M'
inst_17 : ChartedSpace H' M'
inst_18 : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f1
f2 : OpenPartialHomeomorph M' H'
hf2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f2
g1 : OpenPartialHomeomorph M H
hg1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) g1
g2 : OpenPartialHomeomorph M' H'
hg2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') g2
⊢ (f1.prod f2).symm ≫ₕ g1.prod g2 ∈ contDiffGroupoid n (I.prod I')
have rw : (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')
Tactic: rw [OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.prod_trans]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
n : ℕ∞ω
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
𝕜 : Type u_5
inst_6 : NontriviallyNormedField 𝕜
E : Type u_6
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
E' : Type u_7
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H : Type u_8
inst_11 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst_12 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : IsManifold I n M
M' : Type u_11
inst_16 : TopologicalSpace M'
inst_17 : ChartedSpace H' M'
inst_18 : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f1
f2 : OpenPartialHomeomorph M' H'
hf2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f2
g1 : OpenPartialHomeomorph M H
hg1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) g1
g2 : OpenPartialHomeomorph M' H'
hg2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') g2
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')
have h1 : f1.symm ≫ₕ g1 ∈ contDiffGroupoid n I
Tactic: have h1 := (contDiffGroupoid n I).compatible hf1 hg1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
E_1 : Type u_2
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace 𝕜_1 E_1
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
n : ℕ∞ω
M_1 : Type u_4
inst_4 : TopologicalSpace M_1
inst_5 : ChartedSpace H_1 M_1
𝕜 : Type u_5
inst_6 : NontriviallyNormedField 𝕜
E : Type u_6
inst_7 : NormedAddCommGroup E
inst_8 : NormedSpace 𝕜 E
E' : Type u_7
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
H : Type u_8
inst_11 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst_12 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst_13 : TopologicalSpace M
inst_14 : ChartedSpace H M
inst_15 : IsManifold I n M
M' : Type u_11
inst_16 : TopologicalSpace M'
inst_17 : ChartedSpace H' M'
inst_18 : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f1
f2 : OpenPartialHomeomorph M' H'
hf2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f2
g1 : OpenPartialHomeomorph M H
hg1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) g1
g2 : OpenPartialHomeomorph M' H'
hg2 : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') g2
h1 : f1.symm ≫ₕ g1 ∈ contDiffGroupoid n I
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')
have h2 : f2.symm ≫ₕ g2 ∈ contDiffGroupoid n I'
Tactic: have h2 := (contDiffGroupoid n I').compatible hf2 hg2
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ (e.prod e').symm ≫ₕ f.prod f' ∈ contDiffGroupoid n (I.prod I') ∧
    (f.prod f').symm ≫ₕ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have rw : (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I') ∧
  (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
Tactic: rw [OpenPartialHomeomorph.prod_symm_trans_prod,
    OpenPartialHomeomorph.prod_symm_trans_prod]
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I') ∧
    (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
have left : (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')
Tactic: constructor
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
left : (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I') ∧
    (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
have right : (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
Tactic: constructor
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')
have left : e.symm ≫ₕ f ∈ contDiffGroupoid n I
Tactic: apply contDiffGroupoid_prod
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
left : e.symm ≫ₕ f ∈ contDiffGroupoid n I
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')
have left₁ : e'.symm ≫ₕ f' ∈ contDiffGroupoid n I'
Tactic: apply contDiffGroupoid_prod
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
⊢ (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
have right : f.symm ≫ₕ e ∈ contDiffGroupoid n I
Tactic: apply contDiffGroupoid_prod
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
e' : OpenPartialHomeomorph M' H'
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
f : OpenPartialHomeomorph M H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f
f' : OpenPartialHomeomorph M' H'
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (atlas H' M') f'
right : f.symm ≫ₕ e ∈ contDiffGroupoid n I
⊢ (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')
have right₁ : f'.symm ≫ₕ e' ∈ contDiffGroupoid n I'
Tactic: apply contDiffGroupoid_prod
-- 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'
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inl : ∀ (h : IsEmpty H), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (h | h) := isEmpty_or_nonempty H
-- 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'
inl : ∀ (h : IsEmpty H), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : ∀ (h : Nonempty H), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (h | h) := isEmpty_or_nonempty H
-- 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
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr : ∀ (f : OpenPartialHomeomorph M H) (hf : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) f)
  (hef : e = f.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := 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
inr :
  ∀ (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
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have inr₁ : ∀ (f : OpenPartialHomeomorph M' H) (hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H)) (atlas H M') f)
  (hef : e = f.lift_openEmbedding sorry), e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Tactic: obtain (⟨f, hf, hef⟩ | ⟨f, hf, hef⟩) := ChartedSpace.mem_atlas_sum he