awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
p : M ⊕ M'
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g p)) : N → E') ∘ Sum.elim f g ∘ (↑(extChartAt I p).symm : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
have inl : ∀ (x : M),
  ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g (Sum.inl x))) : N → E') ∘
      Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inl x))) : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))
Tactic: cases p with
  | inl x =>
    -- In charts around x : M, the map f ⊔ g looks like f.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
      let hf' := hf x
      rw [contMDiffAt_iff] at hf'
      simpa using hf'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
      congr
  | inr x =>
    -- In charts around x : M, the map f ⊔ g looks like g.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
      let hg' := hg x
      rw [contMDiffAt_iff] at hg'
      simpa using hg'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]
      congr
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
M' : Type u_16
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_18
inst_10 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
inst_11 : TopologicalSpace N
inst_12 : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
p : M ⊕ M'
inl :
  ∀ (x : M),
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt J (Sum.elim f g (Sum.inl x))) : N → E') ∘
        Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inl x))) : E → M ⊕ M'))
      (range (↑I : H → E)) ((↑(extChartAt I (Sum.inl x)) : M ⊕ M' → E) (Sum.inl x))
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g p)) : N → E') ∘ Sum.elim f g ∘ (↑(extChartAt I p).symm : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I p) : M ⊕ M' → E) p)
have inr : ∀ (x : M'),
  ContDiffWithinAt 𝕜 n
    ((↑(extChartAt J (Sum.elim f g (Sum.inr x))) : N → E') ∘
      Sum.elim f g ∘ (↑(PartialEquiv.symm (extChartAt I (Sum.inr x))) : E → M ⊕ M'))
    (range (↑I : H → E)) ((↑(extChartAt I (Sum.inr x)) : M ⊕ M' → E) (Sum.inr x))
Tactic: cases p with
  | inl x =>
    -- In charts around x : M, the map f ⊔ g looks like f.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
      let hf' := hf x
      rw [contMDiffAt_iff] at hf'
      simpa using hf'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
      congr
  | inr x =>
    -- In charts around x : M, the map f ⊔ g looks like g.
    -- This is how they both look like in extended charts.
    have : ContDiffWithinAt 𝕜 n ((extChartAt J (g x)) ∘ g ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) := by
      let hg' := hg x
      rw [contMDiffAt_iff] at hg'
      simpa using hg'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inr, ChartedSpace.sum_chartAt_inr]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inr, Sum.elim_inr]
      congr
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
⊢ ContMDiff I J n f
have a : Nontrivial N
Tactic: nontriviality N
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
⊢ ContMDiff I J n f
have inhabit : ∀ (inhabited_h : Inhabited N), ContMDiff I J n f
Tactic: inhabit N
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
⊢ aux ∘ Sum.inl ∘ f = f
have h₁ : ∀ (x : M), (aux ∘ Sum.inl ∘ f) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
⊢ ContMDiff I J n f
have this : aux ∘ Sum.inl ∘ f = f
Tactic: have : aux ∘ (@Sum.inl N N') ∘ f = f := by ext; simp [aux]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
⊢ ContMDiff I J n f
have rw : ContMDiff I J n (aux ∘ Sum.inl ∘ f)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inl ∘ f)
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
⊢ ContMDiff I J n (aux ∘ Sum.inl ∘ f)
have rw : ∀ (h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ),
  Nontrivial N →
    ∀ (inhabited_h : Inhabited N),
      let aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default;
      ∀ (this : aux ∘ Sum.inl ∘ f = f), ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ
Tactic: rw [← contMDiffOn_univ] at h ⊢
Cleared hypotheses: h, h_1, inhabited_h, aux, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
⊢ ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ
have apply : univ ⊆ preimage (β := N ⊕ N') (Sum.inl ∘ f) (Sum.inl '' univ)
Tactic: apply (contMDiff_id.sumElim contMDiff_const).contMDiffOn (s := @Sum.inl N N' '' univ).comp h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : Membership.mem (γ := Set M) univ x
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inl '' univ) (Sum.inl (f x))
have w : N
Tactic: use f x, trivial
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : Membership.mem (γ := Set M) univ x
w : N
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inl '' univ) (Sum.inl (f x))
have left : Membership.mem (γ := Set N) univ (f x)
Tactic: use f x, trivial
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inl ∘ f) univ
h_1 : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun (x : N') ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : Membership.mem (γ := Set M) univ x
w : N
left : Membership.mem (γ := Set N) univ (f x)
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inl '' univ) (Sum.inl (f x))
have right : Eq (α := N ⊕ N') (Sum.inl (f x)) (Sum.inl (f x))
Tactic: use f x, trivial
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
⊢ ContMDiff I J n g
have a : Nontrivial N'
Tactic: nontriviality N'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
⊢ ContMDiff I J n g
have inhabit : ∀ (inhabited_h : Inhabited N'), ContMDiff I J n g
Tactic: inhabit N'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
⊢ aux ∘ Sum.inr ∘ g = g
have h₁ : ∀ (x : M'), (aux ∘ Sum.inr ∘ g) x = g x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
⊢ ContMDiff I J n g
have this : aux ∘ Sum.inr ∘ g = g
Tactic: have : aux ∘ (@Sum.inr N N') ∘ g = g := by ext; simp [aux]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
⊢ ContMDiff I J n g
have rw : ContMDiff I J n (aux ∘ Sum.inr ∘ g)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J (M' := N ⊕ N') n (Sum.inr ∘ g)
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
⊢ ContMDiff I J n (aux ∘ Sum.inr ∘ g)
have rw : ∀ (h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ),
  Nontrivial N' →
    ∀ (inhabited_h : Inhabited N'),
      let aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id;
      ∀ (this : aux ∘ Sum.inr ∘ g = g), ContMDiffOn I J n (aux ∘ Sum.inr ∘ g) univ
Tactic: rw [← contMDiffOn_univ] at h ⊢
Cleared hypotheses: h, h_1, inhabited_h, aux, this
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
⊢ ContMDiffOn I J n (aux ∘ Sum.inr ∘ g) univ
have apply : univ ⊆ preimage (β := N ⊕ N') (Sum.inr ∘ g) (Sum.inr '' univ)
Tactic: apply ((contMDiff_const.sumElim contMDiff_id).contMDiffOn (s := Sum.inr '' univ)).comp h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : Membership.mem (γ := Set M') univ x
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inr '' univ) (Sum.inr (g x))
have w : N'
Tactic: use g x, trivial
-- Lean 4 proof step from Mathlib.Geometry.Manifold.ContMDiff.Constructions (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_18
inst_8 : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst_9 : TopologicalSpace N
inst_10 : TopologicalSpace N'
inst_11 : ChartedSpace H' N
inst_12 : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J (M' := N ⊕ N') n (Sum.inr ∘ g) univ
h_1 : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun (x : N) ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : Membership.mem (γ := Set M') univ x
w : N'
⊢ Membership.mem (γ := Set (N ⊕ N')) (Sum.inr '' univ) (Sum.inr (g x))
have left : Membership.mem (γ := Set N') univ (g x)
Tactic: use g x, trivial