awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
h :
  ∀ (a : E),
    f ((↑e.symm : E → M) a) ∈ t ∧ f ((↑e.symm : E → M) a) ∈ e'.source →
      a ∈ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))
⊢ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) ∈
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x

Tactic:
filter_upwards [A]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
x' : E
ht : f ((↑e.symm : E → M) x') ∈ t
hfx' : f ((↑e.symm : E → M) x') ∈ e'.source
h : (↑(extChartAt I' (f x)) : M' → E') (f ((↑(extChartAt I x).symm : E → M) x')) ∈ range (↑I' : H' → E')
⊢ x' ∈ writtenInExtChartAt I I' x f ⁻¹' ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E'))

Tactic:
simp only [*, e, e', mem_preimage, writtenInExtChartAt, (· ∘ ·), mem_inter_iff, e'.left_inv,
      true_and]

Premises used: Set.mem_inter_iff, Function.comp, writtenInExtChartAt, PartialEquiv.left_inv, Set.mem_preimage, true_and
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
x' : E
ht : f ((↑e.symm : E → M) x') ∈ t
hfx' : f ((↑e.symm : E → M) x') ∈ e'.source
⊢ (↑(extChartAt I' (f x)) : M' → E') (f ((↑(extChartAt I x).symm : E → M) x')) ∈ range (↑I' : H' → E')

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, ModelWithCorners.toFun'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
x' : E
ht : f ((↑e.symm : E → M) x') ∈ t
hfx' : f ((↑e.symm : E → M) x') ∈ e'.source
⊢ (↑(extChartAt I' (f x)) : M' → E') (f ((↑(extChartAt I x).symm : E → M) x')) ∈ range (↑I' : H' → E')

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
h :
  ∀ (a : E),
    f ((↑e.symm : E → M) a) ∈ t ∧ f ((↑e.symm : E → M) a) ∈ e'.source →
      ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) a =
        (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f) a
⊢ (↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘
      (g ∘ f) ∘ (↑e.symm : E → M) =ᶠ[𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x]
    ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f

Tactic:
filter_upwards [A]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
x' : E
hfx' : f ((↑e.symm : E → M) x') ∈ e'.source
⊢ ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) x' =
    (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f) x'

Tactic:
simp only [*, e, e', (· ∘ ·), writtenInExtChartAt, e'.left_inv]

Premises used: Function.comp, writtenInExtChartAt, PartialEquiv.left_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n ((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M'))
      ((↑e'.symm : E' → M') ⁻¹' t ∩ range (↑I' : H' → E')) (writtenInExtChartAt I I' x f ((↑e : M → E) x))
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n ((↑e' : M' → E') ∘ f ∘ (↑e.symm : E → M)) ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑e : M → E) x)
this : (↑e' : M' → E') (f x) = writtenInExtChartAt I I' x f ((↑e : M → E) x)
A :
  ∀ᶠ (y : E) in 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x,
    f ((↑e.symm : E → M) y) ∈ t ∧ f ((↑e.symm : E → M) y) ∈ e'.source
⊢ ((↑(extChartAt I'' ((g ∘ f) x)) : M'' → E'') ∘ (g ∘ f) ∘ (↑e.symm : E → M)) ((↑e : M → E) x) =
    (((↑(extChartAt I'' (g (f x))) : M'' → E'') ∘ g ∘ (↑e'.symm : E' → M')) ∘ writtenInExtChartAt I I' x f)
      ((↑e : M → E) x)

Tactic:
simp only [e, e', writtenInExtChartAt, (· ∘ ·), mem_extChartAt_source,
      e.left_inv, e'.left_inv]

Premises used: Function.comp, mem_extChartAt_source, writtenInExtChartAt, PartialEquiv.left_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
y : M'
hg : ContMDiffWithinAt I' I'' n g t y
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hx : f x = y
⊢ ContMDiffWithinAt I' I'' n g t (f x)

Tactic:
subst hx
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hg : ContMDiffWithinAt I' I'' n g t (f x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
hg.comp x hf st

Premises used: ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hg : ContMDiffWithinAt I' I'' n g t (f x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
exact hg.comp x hf st

Premises used: ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
hg : ContMDiffOn I' I'' n g t
hf : ContMDiffOn I I' n f s
st : s ⊆ f ⁻¹' t
⊢ ContMDiffOn I I'' n (g ∘ f) s

Tactic:
fun x hx =>
  (hg _ (st hx)).comp x (hf x hx) st

Premises used: ContMDiffWithinAt.comp, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
hg : ContMDiffOn I' I'' n g t
hf : ContMDiffOn I I' n f s
⊢ ContMDiffOn I I'' n (g ∘ f) (s ∩ f ⁻¹' t)

Tactic:
hg.comp (hf.mono inter_subset_left) inter_subset_right

Premises used: Set.inter_subset_left, ContMDiffOn.mono, Set.inter_subset_right, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
hg : ContMDiff I' I'' n g
hf : ContMDiff I I' n f
rw : ∀ (hg : ContMDiffOn I' I'' n g univ) (hf : ContMDiffOn I I' n f univ), ContMDiffOn I I'' n (g ∘ f) univ
⊢ ContMDiff I I'' n (g ∘ f)

Tactic:
rw [← contMDiffOn_univ] at hf hg ⊢

Premises used: contMDiffOn_univ
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
hg : ContMDiffOn I' I'' n g univ
hf : ContMDiffOn I I' n f univ
⊢ ContMDiffOn I I'' n (g ∘ f) univ

Tactic:
hg.comp hf subset_preimage_univ

Premises used: Set.subset_preimage_univ, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
hg : ContMDiffOn I' I'' n g univ
hf : ContMDiffOn I I' n f univ
⊢ ContMDiffOn I I'' n (g ∘ f) univ

Tactic:
exact hg.comp hf subset_preimage_univ

Premises used: Set.subset_preimage_univ, ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
hg : ContMDiffWithinAt I' I'' n g t (f x)
hf : ContMDiffWithinAt I I' n f s x
⊢ ContMDiffWithinAt I I'' n (g ∘ f) (s ∩ f ⁻¹' t) x

Tactic:
hg.comp x (hf.mono inter_subset_left) inter_subset_right

Premises used: ContMDiffWithinAt.mono, Set.inter_subset_left, Set.inter_subset_right, ContMDiffWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_8 : TopologicalSpace M'
E'' : Type u_8
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_12 : TopologicalSpace M''
inst_13 : ChartedSpace H M
inst_14 : ChartedSpace H' M'
inst_15 : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
g : M' → M''
x : M
hg : ContMDiffAt I' I'' n g (f x)
hf : ContMDiffWithinAt I I' n f s x
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
hg.comp x hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, ContMDiffWithinAt.comp