awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type w'
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this :
  (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) =
    range (Prod.map (↑I : H → E) (↑I' : H' → E'))
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (E := E × E') (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2))
  else Eq (α := Set (E × E')) (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have rw : if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
else range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
Tactic: rw [this, Set.range_prodMap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type w'
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this :
  (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) =
    range (Prod.map (↑I : H → E) (↑I' : H' → E'))
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
  else range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
have pos : ∀ (h : IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type w'
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this :
  (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) =
    range (Prod.map (↑I : H → E) (↑I' : H' → E'))
pos : ∀ (h : IsRCLikeNormedField 𝕜), Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
  else range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst_4 : NormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
H' : Type w'
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ Set.Nonempty (α := E × E') (interior (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)))
have this : (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) =
  range (Prod.map (↑I : H → E) (↑I' : H' → E'))
Tactic: have : range (fun (x : ModelProd H H') ↦ (I x.1, I' x.2)) = range (Prod.map I I') := rfl
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (E := (i : ι) → E i)
      (range (ι := ModelPi H)
        (↑(PartialEquiv.pi (αi := H) (βi := E) fun (i : ι) ↦ (I i).toPartialEquiv) : ModelPi H → (i : ι) → E i))
  else
    Eq (α := Set ((i : ι) → E i))
      (range (ι := ModelPi H)
        (↑(PartialEquiv.pi (αi := H) (βi := E) fun (i : ι) ↦ (I i).toPartialEquiv) : ModelPi H → (i : ι) → E i))
      univ
have rw : if h : IsRCLikeNormedField 𝕜 then
  Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))
else Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ
Tactic: rw [PartialEquiv.pi_apply, Set.range_piMap]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))
  else Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ
have pos : ∀ (h : IsRCLikeNormedField 𝕜),
  Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
pos :
  ∀ (h : IsRCLikeNormedField 𝕜),
    Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))
⊢ if h : IsRCLikeNormedField 𝕜 then
    Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))
  else Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜),
  Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
ι : Type v
inst_1 : Fintype ι
E : ι → Type w
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, w} 𝕜 (E i)
H : ι → Type u'
inst_4 : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners.{u, w, u'} 𝕜 (E i) (H i)
⊢ Set.Nonempty (α := (i : ι) → E i)
    (interior
      (range (ι := ModelPi H)
        (↑(PartialEquiv.pi (αi := H) (βi := E) fun (i : ι) ↦ (I i).toPartialEquiv) : ModelPi H → (i : ι) → E i)))
have rw : Set.Nonempty (α := (i : ι) → E i)
  (interior (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)))
Tactic: rw [PartialEquiv.pi_apply, Set.range_piMap]
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ Eq (α := ModelWithCorners 𝕜 (E × F) (E × F)) 𝓘(𝕜, E × F) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))
have toFun : (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
  (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)
Tactic: ext1
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
toFun :
  (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
    (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)
⊢ Eq (α := ModelWithCorners 𝕜 (E × F) (E × F)) 𝓘(𝕜, E × F) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))
have invFun : PartialEquiv.invFun (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
  (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).invFun
Tactic: ext1
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
toFun :
  (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
    (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)
invFun :
  PartialEquiv.invFun (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).invFun
⊢ Eq (α := ModelWithCorners 𝕜 (E × F) (E × F)) 𝓘(𝕜, E × F) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))
have source : source (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
  (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).source
Tactic: ext1
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
toFun :
  (↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) : E × F → E × F) =
    (↑(ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))) : E × F → E × F)
invFun :
  PartialEquiv.invFun (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).invFun
source :
  PartialEquiv.source (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
    (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).source
⊢ Eq (α := ModelWithCorners 𝕜 (E × F) (E × F)) 𝓘(𝕜, E × F) (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))
have target : target (ModelWithCorners.toPartialEquiv 𝓘(𝕜, E × F)) =
  (ModelWithCorners.toPartialEquiv (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F))).target
Tactic: ext1
-- 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
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ range (↑(I.prod J) : ModelProd H G → E × F) = range (↑I : H → E) ×ˢ range (↑J : G → F)
have simp_rw : (I.prod J).target = I.target ×ˢ J.target
Tactic: simp_rw [← ModelWithCorners.target_eq]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
⊢ (I.prod I').Boundaryless
have range_eq_univ : range (↑(I.prod I') : ModelProd H H' → E × E') = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
⊢ Eq (α := Set (E × E')) (range fun (x : H × H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have range_eq_univ : range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
Tactic: rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
range_eq_univ : range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
⊢ Eq (α := Set (E × E')) (range fun (x : H × H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have range_eq_univ₁ : SProd.sprod (α := Set E) univ (range (↑I' : H' → E')) = univ
Tactic: rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
range_eq_univ : range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
range_eq_univ₁ : SProd.sprod (α := Set E) univ (range (↑I' : H' → E')) = univ
⊢ Eq (α := Set (E × E')) (range fun (x : H × H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have range_eq_univ₂ : SProd.sprod (α := Set E) (β := Set E') univ univ = univ
Tactic: rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type w
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : I.Boundaryless
E' : Type v'
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type w'
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst_8 : I'.Boundaryless
range_eq_univ : range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
range_eq_univ₁ : SProd.sprod (α := Set E) univ (range (↑I' : H' → E')) = univ
range_eq_univ₂ : SProd.sprod (α := Set E) (β := Set E') univ univ = univ
⊢ Eq (α := Set (E × E')) (range fun (x : H × H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)) univ
have range_eq_univ₃ : Eq (α := Set (E × E')) univ univ
Tactic: rw [← prod_range_range_eq, ModelWithCorners.Boundaryless.range_eq_univ,
    ModelWithCorners.Boundaryless.range_eq_univ, univ_prod_univ]
-- 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
⊢ (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
have h : ∀ (x : E),
  ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) x =
    (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.Basic (hypothesis)
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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
have this : (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
  ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
Tactic: have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
-- 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
have simp : ContDiffOn 𝕜 n (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H))
  ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
Tactic: simp only [this]
-- 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
⊢ ContDiffOn 𝕜 n (((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
have refine : MapsTo ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v) ∩ range (↑I : H → E))
  ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
Tactic: refine hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_
-- 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
f g : H → H
u v : Set H
hf : ContDiffOn 𝕜 n ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' u ∩ range (↑I : H → E))
hg : ContDiffOn 𝕜 n ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E))
h : IsOpen[inst_3] u
h_1 : IsOpen[inst_3] v
h_2 : IsOpen[inst_3] (u ∩ f ⁻¹' v)
this :
  (↑I : H → E) ∘ (g ∘ f) ∘ (↑I.symm : E → H) =
    ((↑I : H → E) ∘ g ∘ (↑I.symm : E → H)) ∘ (↑I : H → E) ∘ f ∘ (↑I.symm : E → H)
x : E
hx1 : x ∈ (↑I.symm : E → H) ⁻¹' (u ∩ f ⁻¹' v)
right : x ∈ range (↑I : H → E)
⊢ ((↑I : H → E) ∘ f ∘ (↑I.symm : E → H)) x ∈ (↑I.symm : E → H) ⁻¹' v ∩ range (↑I : H → E)
have simp : ∀ (hx1 : (↑I.symm : E → H) x ∈ u ∧ f ((↑I.symm : E → H) x) ∈ v), f ((↑I.symm : E → H) x) ∈ v
Tactic: simp only [mfld_simps] at hx1 ⊢
Cleared hypotheses: hx1
-- 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
⊢ ContDiffOn 𝕜 n ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' univ ∩ range (↑I : H → E))
have apply : ∀ x ∈ (↑I.symm : E → H) ⁻¹' univ ∩ range (↑I : H → E), ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
Tactic: apply ContDiffOn.congr contDiff_id.contDiffOn
-- 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
x : E
left : x ∈ (↑I.symm : E → H) ⁻¹' univ
hx2 : x ∈ range (↑I : H → E)
⊢ ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
have rcases : ∀ (y : H) (hy : (↑I : H → E) y = x), ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
Tactic: rcases mem_range.1 hx2 with ⟨y, hy⟩
-- 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
x : E
left : x ∈ (↑I.symm : E → H) ⁻¹' univ
hx2 : x ∈ range (↑I : H → E)
y : H
hy : (↑I : H → E) y = x
⊢ ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) x = id x
have rw : ((↑I : H → E) ∘ id ∘ (↑I.symm : E → H)) ((↑I : H → E) y) = id ((↑I : H → E) y)
Tactic: rw [← hy]
-- 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_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
f : H_1 → H_1
u : Set H_1
h : IsOpen[inst_3] u
H :
  ∀ x ∈ u,
    ∃ (v : Set H_1),
      IsOpen[inst_3] v ∧
        x ∈ v ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
⊢ ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1)) ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E))
have h : ∀ x ∈ (↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E),
  ∃ (u_1 : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      x ∈ u_1 ∧
        ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
          ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
Tactic: apply contDiffOn_of_locally_contDiffOn
-- 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_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
f : H_1 → H_1
u : Set H_1
h : IsOpen[inst_3] u
H :
  ∀ x ∈ u,
    ∃ (v : Set H_1),
      IsOpen[inst_3] v ∧
        x ∈ v ∧
          ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
            ((↑I.symm : E → H_1) ⁻¹' (u ∩ v) ∩ range (↑I : H_1 → E))
y : E
hy1 : y ∈ (↑I.symm : E → H_1) ⁻¹' u
hy2 : y ∈ range (↑I : H_1 → E)
⊢ ∃ (u_1 : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      y ∈ u_1 ∧
        ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
          ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
have h : ∀ (x : H_1) (hx : (↑I : H_1 → E) x = y),
  ∃ (u_1 : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      y ∈ u_1 ∧
        ContDiffOn 𝕜 n ((↑I : H_1 → E) ∘ f ∘ (↑I.symm : E → H_1))
          ((↑I.symm : E → H_1) ⁻¹' u ∩ range (↑I : H_1 → E) ∩ u_1)
Tactic: rcases mem_range.1 hy2 with ⟨x, hx⟩