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
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsEmpty M
e e' : OpenPartialHomeomorph M H
h_1 : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
h_2 : 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)
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
⊢ 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

Tactic:
set t := I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range I

Premises used: OpenPartialHomeomorph.trans, ModelWithCorners.toFun', ModelWithCorners.symm, PartialEquiv.source, Set.range, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- 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
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
rw rw₁ : (e.symm ≫ₕ e').source = (e.symm ≫ₕ e').source
⊢ (e.symm ≫ₕ e').source = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' e'.source

Tactic:
rw [← OpenPartialHomeomorph.trans_source]

Premises used: OpenPartialHomeomorph.trans_source
-- 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
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
rw rw₁ : e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅ = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅
⊢ e.symm.source ∩ (↑e.symm : H → M) ⁻¹' e'.source = e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅

Tactic:
rw [eq_empty_of_isEmpty (e'.source)]

Premises used: PartialEquiv.source, OpenPartialHomeomorph.toPartialEquiv, Set.eq_empty_of_isEmpty
-- 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
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
rw rw₁ : e.symm.source ∩ ∅ = e.symm.source ∩ ∅
⊢ e.symm.source ∩ (↑e.symm : H → M) ⁻¹' ∅ = e.symm.source ∩ ∅

Tactic:
rw [preimage_empty]

Premises used: Set.preimage_empty
-- 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
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 = ∅

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
-- 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
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 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))
⊢ t = (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E)

Tactic:
rw [← Subtype.preimage_val_eq_preimage_val_iff]

Premises used: Subtype.preimage_val_eq_preimage_val_iff
-- 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
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)
rw₁ rw₂ : ∅ ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)
⊢ (↑I.symm : E → H) ⁻¹' (e.symm ≫ₕ e').source ∩ range (↑I : H → E) = ∅ ∩ range (↑I : H → E)

Tactic:
rw [this, preimage_empty]

Premises used: Set.preimage_empty
-- 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
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 = ∅

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)
-- 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
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_1 : (e.symm ≫ₕ e').source = ∅
this : t = ∅
⊢ ContDiffWithinAt 𝕜 n ((↑I : H → E) ∘ (↑(e.symm ≫ₕ e') : H → H) ∘ (↑I.symm : E → H)) t x

Tactic:
apply (this ▸ hx).elim
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
M : Type u_4
inst_3 : TopologicalSpace M
inst_4 : DiscreteTopology M
inst_5 : Unique E
⊢ IsManifold 𝓘(𝕜, E) n M

Tactic:
apply isManifold_of_contDiffOn _ _ _ (fun _ _ _ _ ↦ contDiff_of_subsingleton.contDiffOn)

Premises used: ContDiff.contDiffOn, contDiff_of_subsingleton, isManifold_of_contDiffOn
-- 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
n : ℕ∞ω
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : Unique E
⊢ IsManifold 𝓘(𝕜, E) n (Fin 2)

Tactic:
of_discreteTopology _

Premises used: IsManifold.of_discreteTopology
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
rw : (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')
⊢ (f1.prod f2).symm ≫ₕ g1.prod g2 ∈ contDiffGroupoid n (I.prod I')

Tactic:
rw [OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.prod_trans]

Premises used: OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.prod_trans
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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 ∈ contDiffGroupoid n I

Tactic:
have h1 := (contDiffGroupoid n I).compatible hf1 hg1
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
⊢ f2.symm ≫ₕ g2 ∈ contDiffGroupoid n I'

Tactic:
have h2 := (contDiffGroupoid n I').compatible hf2 hg2
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
h2 : f2.symm ≫ₕ g2 ∈ contDiffGroupoid n I'
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')

Tactic:
contDiffGroupoid_prod h1 h2

Premises used: contDiffGroupoid_prod
-- Module: Mathlib.Geometry.Manifold.IsManifold.Basic
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
h2 : f2.symm ≫ₕ g2 ∈ contDiffGroupoid n I'
⊢ (f1.symm ≫ₕ g1).prod (f2.symm ≫ₕ g2) ∈ contDiffGroupoid n (I.prod I')

Tactic:
exact contDiffGroupoid_prod h1 h2

Premises used: contDiffGroupoid_prod
-- 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
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'
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')
⊢ (e.prod e').symm ≫ₕ f.prod f' ∈ contDiffGroupoid n (I.prod I') ∧
    (f.prod f').symm ≫ₕ e.prod e' ∈ contDiffGroupoid n (I.prod I')

Tactic:
rw [OpenPartialHomeomorph.prod_symm_trans_prod,
    OpenPartialHomeomorph.prod_symm_trans_prod]

Premises used: OpenPartialHomeomorph.prod_symm_trans_prod
-- 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
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')
right : (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ 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')

Tactic:
constructor
-- 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
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
left₁ : e'.symm ≫ₕ f' ∈ contDiffGroupoid n I'
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')

Tactic:
apply contDiffGroupoid_prod

Premises used: contDiffGroupoid_prod
-- 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
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
right₁ : f'.symm ≫ₕ e' ∈ contDiffGroupoid n I'
⊢ (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')

Tactic:
apply contDiffGroupoid_prod

Premises used: contDiffGroupoid_prod
-- 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
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 ∈ contDiffGroupoid n I

Tactic:
grind [compatible_of_mem_maximalAtlas, subset_maximalAtlas]

Premises used: IsManifold.compatible_of_mem_maximalAtlas, IsManifold.subset_maximalAtlas