awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
x : H
⊢ UniqueDiffWithinAt 𝕜 (range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
I.uniqueDiffOn _ (mem_range_self _)

Premises used: Set.mem_range_self, ModelWithCorners.uniqueDiffOn
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x) ↔
    ContinuousWithinAt f s x

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
refine_1 :
  ∀ (h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)),
    ContinuousWithinAt f s x
refine_2 :
  ∀ (h : ContinuousWithinAt f s x),
    ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x) ↔
    ContinuousWithinAt f s x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
⊢ ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E))
    ((↑I : H → E) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))) x

Tactic:
have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E))
    ((↑I : H → E) ⁻¹' ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))) x
⊢ ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E)) s x

Tactic:
simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
      inter_univ] at this

Premises used: Set.preimage_inter, Set.preimage_preimage, Set.inter_univ, Set.preimage_id', Set.preimage_range, ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)
this : ContinuousWithinAt ((f ∘ (↑I.symm : E → H)) ∘ (↑I : H → E)) s x
refine_1 : ∀ (this : ContinuousWithinAt (f ∘ (↑I.symm : E → H) ∘ (↑I : H → E)) s x), ContinuousWithinAt f s x
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (this : ContinuousWithinAt (f ∘ id) s x), ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Tactic:
rwa [Function.comp_assoc, I.symm_comp_self] at this

Premises used: ModelWithCorners.symm_comp_self, Function.comp_assoc
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s ((↑I.symm : E → H) ((↑I : H → E) x))

Tactic:
rw [← I.left_inv x] at h

Premises used: ModelWithCorners.left_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s ((↑I.symm : E → H) ((↑I : H → E) x))
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
h.comp I.continuousWithinAt_symm inter_subset_left

Premises used: Set.inter_subset_left, ModelWithCorners.continuousWithinAt_symm, ContinuousWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
X : Type u_4
inst_4 : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s ((↑I.symm : E → H) ((↑I : H → E) x))
⊢ ContinuousWithinAt (f ∘ (↑I.symm : E → H)) ((↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) x)

Tactic:
exact h.comp I.continuousWithinAt_symm inter_subset_left

Premises used: Set.inter_subset_left, ModelWithCorners.continuousWithinAt_symm, ContinuousWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
rw :
  (map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x)).HasBasis
    (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
⊢ (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))

Tactic:
rw [← I.symm_map_nhdsWithin_range]

Premises used: ModelWithCorners.symm_map_nhdsWithin_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x)).HasBasis
    (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))

Tactic:
((compact_basis_nhds (I x)).inf_principal _).map _

Premises used: nhdsWithin, Filter.HasBasis.map, ModelWithCorners.toFun', compact_basis_nhds, Filter.HasBasis.inf_principal
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (map (↑I.symm : E → H) (𝓝[range (↑I : H → E)] (↑I : H → E) x)).HasBasis
    (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
    (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))

Tactic:
exact ((compact_basis_nhds (I x)).inf_principal _).map _

Premises used: Filter.HasBasis.map, ModelWithCorners.toFun', compact_basis_nhds, Filter.HasBasis.inf_principal
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
⊢ ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))

Tactic:
have : ∀ x : H, (𝓝 x).HasBasis (fun s => s ∈ 𝓝 (I x) ∧ IsCompact s)
      fun s => I.symm '' (s ∩ range I) := fun x ↦ by
    rw [← I.symm_map_nhdsWithin_range]
    exact ((compact_basis_nhds (I x)).inf_principal _).map _
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
⊢ LocallyCompactSpace H

Tactic:
.of_hasBasis this ?_

Premises used: LocallyCompactSpace.of_hasBasis
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
refine :
  ∀ (x : H) (i : Set E),
    i ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact i → IsCompact ((↑I.symm : E → H) '' (i ∩ range (↑I : H → E)))
⊢ LocallyCompactSpace H

Tactic:
refine .of_hasBasis this ?_
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact ((↑I.symm : E → H) '' (s ∩ range (↑I : H → E)))

Tactic:
(hsc.inter_right I.isClosed_range).image I.continuous_symm

Premises used: ModelWithCorners.continuous_symm, IsCompact.inter_right, ModelWithCorners.isClosed_range, IsCompact.image
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
this :
  ∀ (x : H),
    (𝓝 x).HasBasis (fun (s : Set E) ↦ s ∈ 𝓝 ((↑I : H → E) x) ∧ IsCompact s) fun (s : Set E) ↦
      (↑I.symm : E → H) '' (s ∩ range (↑I : H → E))
x : H
s : Set E
hsc : IsCompact s
⊢ IsCompact ((↑I.symm : E → H) '' (s ∩ range (↑I : H → E)))

Tactic:
exact (hsc.inter_right I.isClosed_range).image I.continuous_symm

Premises used: ModelWithCorners.continuous_symm, IsCompact.inter_right, ModelWithCorners.isClosed_range, IsCompact.image
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
inst_4 : SecondCountableTopology E
I : ModelWithCorners 𝕜 E H
⊢ SecondCountableTopology H

Tactic:
I.isClosedEmbedding.isEmbedding.secondCountableTopology

Premises used: Topology.IsEmbedding.secondCountableTopology, Topology.IsClosedEmbedding.isEmbedding, ModelWithCorners.isClosedEmbedding
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ T2Space H

Tactic:
have : T2Space H := I.isClosedEmbedding.toIsEmbedding.t2Space
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
this : T2Space H
⊢ T1Space M

Tactic:
ChartedSpace.t1Space H M

Premises used: ChartedSpace.t1Space
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
this : T2Space H
⊢ T1Space M

Tactic:
exact ChartedSpace.t1Space H M

Premises used: ChartedSpace.t1Space
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ ModelWithCorners.toPartialEquiv 𝓘(𝕜, E) = PartialEquiv.refl E

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Equiv.toPartialEquiv, PartialEquiv.refl, rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ (↑𝓘(𝕜, E) : E → E) = id

Tactic:
rfl

Premises used: ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ (↑(ModelWithCorners.symm 𝓘(𝕜, E)) : E → E) = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'
⊢ Eq (α := Set (ModelProd H H')) {x : ModelProd H H' | x.1 ∈ I.source ∧ x.2 ∈ I'.source} univ

Tactic:
simp only [setOf_true, mfld_simps]

Premises used: Set.setOf_true
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'
⊢ (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
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'))
rw :
  if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
  else range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
⊢ 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

Tactic:
rw [this, Set.range_prodMap]

Premises used: Set.range_prodMap
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'))
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
  else range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ

Tactic:
split_ifs with h
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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_1 :
  (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'))
h : IsRCLikeNormedField 𝕜
this_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))

Tactic:
I.convex_range.prod I'.convex_range

Premises used: ModelWithCorners.convex_range, Convex.prod
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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_1 :
  (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'))
h : IsRCLikeNormedField 𝕜
this_2 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_3 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ Convex ℝ (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))

Tactic:
exact I.convex_range.prod I'.convex_range

Premises used: ModelWithCorners.convex_range, Convex.prod
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'))
h : ¬IsRCLikeNormedField 𝕜
⊢ range (↑I : H → E) ×ˢ range (↑I' : H' → E') = univ

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField, h]

Premises used: ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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'))
⊢ Set.Nonempty (α := E × E') (interior (range fun (x : ModelProd H H') ↦ ((↑I : H → E) x.1, (↑I' : H' → E') x.2)))

Tactic:
simp [this, interior_prod_eq, nonempty_interior]

Premises used: interior_prod_eq, ModelWithCorners.nonempty_interior
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)
⊢ Eq (α := Set (ModelPi H))
    (source (β := (i : ι) → E i) (PartialEquiv.pi (αi := H) (βi := E) fun (i : ι) ↦ (I i).toPartialEquiv)) univ

Tactic:
simp only [pi_univ, mfld_simps]

Premises used: Set.pi_univ
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)
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
⊢ 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

Tactic:
rw [PartialEquiv.pi_apply, Set.range_piMap]

Premises used: Set.range_piMap, PartialEquiv.pi_apply
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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))
neg :
  ∀ (h : ¬IsRCLikeNormedField 𝕜),
    Eq (α := Set ((i : ι) → E i)) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i)) univ
⊢ 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:
split_ifs with h
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : (i : ι) → NormedSpace ℝ (E i) := fun (i : ι) ↦ NormedSpace.restrictScalars ℝ 𝕜 (E i)
⊢ Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))

Tactic:
convex_pi fun i _hi ↦ (I i).convex_range

Premises used: convex_pi, ModelWithCorners.convex_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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)
h : IsRCLikeNormedField 𝕜
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : (i : ι) → NormedSpace ℝ (E i) := fun (i : ι) ↦ NormedSpace.restrictScalars ℝ 𝕜 (E i)
⊢ Convex ℝ (E := (i : ι) → E i) (Set.pi (α := E) univ fun (i : ι) ↦ range (↑(I i).toPartialEquiv : H i → E i))

Tactic:
exact convex_pi fun i _hi ↦ (I i).convex_range

Premises used: convex_pi, ModelWithCorners.convex_range