awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
s : Set H
hs : IsOpen[inst_3] s
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
have this : ContDiffOn.{u_1, u_2, u_2} 𝕜 (E := E) n id univ
Tactic: have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : e ∈ contDiffGroupoid n I
he' : e' ∈ contDiffGroupoid n I'
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have he₁ : (contDiffPregroupoid n I).property (↑e : H → H) e.source
Tactic: obtain ⟨he, he_symm⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : e ∈ contDiffGroupoid n I
he' : e' ∈ contDiffGroupoid n I'
he₁ : (contDiffPregroupoid n I).property (↑e : H → H) e.source
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
Tactic: obtain ⟨he, he_symm⟩ := he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have he'₁ : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
Tactic: obtain ⟨he', he'_symm⟩ := he'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid n I'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he'₁ : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
Tactic: obtain ⟨he', he'_symm⟩ := he'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have left : (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e') : ModelProd H H' → ModelProd H H') (e.prod e').source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
left : (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e') : ModelProd H H' → ModelProd H H') (e.prod e').source
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')
have right : (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') (e.prod e').target
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' e.source ×ˢ e'.source ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have h3 : ContDiffOn 𝕜 n
  (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
  (((↑I.symm : E → H) ⁻¹' e.source ∩ range (↑I : H → E)) ×ˢ
    ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')))
Tactic: have h3 := ContDiffOn.prodMap he he'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.source ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.source ∩ range (↑I' : H' → E')))
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' e.source ×ˢ e'.source ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have h3₁ : ContDiffOn 𝕜 n
  (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
    ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
  ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)
Tactic: rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e' : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.source ×ˢ e'.source)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' e.source ×ˢ e'.source ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have left : ContDiffOn 𝕜 n
  ((↑(I.prod I') : ModelProd H H' → E × E') ∘
    (↑(e.prod e') : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
  ((↑(I.prod I') : ModelProd H H' → E × E') '' e.source ×ˢ e'.source)
Tactic: rw [← (I.prod I').image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' (e.prod e'.toPartialEquiv).target ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have h3 : ContDiffOn 𝕜 n
  (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
  (((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ×ˢ
    ((↑I'.symm : E' → H') ⁻¹' e'.target ∩ range (↑I' : H' → E')))
Tactic: have h3 := ContDiffOn.prodMap he_symm he'_symm
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    (((↑I.symm : E → H) ⁻¹' e.target ∩ range (↑I : H → E)) ×ˢ
      ((↑I'.symm : E' → H') ⁻¹' e'.target ∩ range (↑I' : H' → E')))
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' (e.prod e'.toPartialEquiv).target ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have h3₁ : ContDiffOn 𝕜 n
  (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
    ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
  ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)
Tactic: rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e : H → H) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm : H → H) e.target
he' : (contDiffPregroupoid n I').property (↑e' : H' → H') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm : H' → H') e'.target
h3 :
  ContDiffOn 𝕜 n
    (Prod.map ((↑I : H → E) ∘ (↑e.symm : H → H) ∘ (↑I.symm : E → H))
      ((↑I' : H' → E') ∘ (↑e'.symm : H' → H') ∘ (↑I'.symm : E' → H')))
    ((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) '' e.target ×ˢ e'.target)
⊢ ContDiffOn 𝕜 n
    ((↑(I.prod I') : ModelProd H H' → E × E') ∘
      (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
    ((↑(I.prod I').symm : E × E' → ModelProd H H') ⁻¹' (e.prod e'.toPartialEquiv).target ∩
      range (↑(I.prod I') : ModelProd H H' → E × E'))
have right : ContDiffOn 𝕜 n
  ((↑(I.prod I') : ModelProd H H' → E × E') ∘
    (↑(e.prod e').symm : ModelProd H H' → ModelProd H H') ∘ (↑(I.prod I').symm : E × E' → ModelProd H H'))
  ((↑(I.prod I') : ModelProd H H' → E × E') '' (e.prod e'.toPartialEquiv).target)
Tactic: rw [← (I.prod I').image_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
m n : ℕ∞ω
𝕜 : 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
E' : Type u_5
H' : Type u_6
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst_3] s
hes : e ≈ OpenPartialHomeomorph.ofSet s hs
⊢ e ∈ contDiffGroupoid n I
have apply : OpenPartialHomeomorph.ofSet s hs ∈ (contDiffGroupoid n I).members
Tactic: apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes
-- 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
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
        ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
          ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
⊢ ∀ {e e' : OpenPartialHomeomorph M H},
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
      Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' → e.symm ≫ₕ e' ∈ contDiffGroupoid n I
have this : HasGroupoid M (contDiffGroupoid n I)
Tactic: haveI : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (h _ _)
-- 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
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
m n : ℕ∞ω
hmn : m ≤ n
inst_6 : IsManifold I n M
⊢ IsManifold I m M
have this : HasGroupoid M (contDiffGroupoid m I)
Tactic: have : HasGroupoid M (contDiffGroupoid m I) :=
    hasGroupoid_of_le (G₁ := contDiffGroupoid n I) (by infer_instance)
      (contDiffGroupoid_le hmn)
-- 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
⊢ IsManifold I 0 M
have suffices : HasGroupoid M (contDiffGroupoid 0 I)
Tactic: suffices HasGroupoid M (contDiffGroupoid 0 I) from mk' I 0 M
-- 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
⊢ HasGroupoid M (contDiffGroupoid 0 I)
have compatible : ∀ {e e' : OpenPartialHomeomorph M H},
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' → e.symm ≫ₕ e' ∈ contDiffGroupoid 0 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
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid 0 I
have compatible : Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
Tactic: rw [contDiffGroupoid_zero_eq]
-- 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
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
⊢ Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
have compatible : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
Tactic: trivial
-- 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
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
compatible : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e') : H → H) (e.symm ≫ₕ e').source
⊢ Membership.mem (γ := StructureGroupoid H) (continuousGroupoid H) (e.symm ≫ₕ e')
have compatible₁ : Pregroupoid.property (continuousPregroupoid H) (↑(e.symm ≫ₕ e').symm : H → H) (e.symm ≫ₕ e').target
Tactic: trivial
-- 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 : IsManifold I 3 M
⊢ LE.le (α := ℕ∞ω) 2 3
have norm_cast : LE.le (α := ℕ) 2 3
Tactic: norm_cast
-- 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
⊢ IsManifold I n M
have h : ∀ (e e' : OpenPartialHomeomorph M H),
  Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e →
    Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e' →
      ContDiffOn 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E))
Tactic: apply isManifold_of_contDiffOn
-- 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
hx : x ∈ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)) x
have h : let t := (↑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
Tactic: set t := I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I
Cleared hypotheses: hx
-- 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 ≫ₕ e').source = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' e'.source
have rw : (e.symm ≫ₕ e').source = (e.symm ≫ₕ e').source
Tactic: rw [← OpenPartialHomeomorph.trans_source]