awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
refine_1 :
  ∀ (y : E)
    (hy :
      y ∈
        (extChartAt I x).target ∩
          (↑(extChartAt I x).symm : E → M) ⁻¹'
            (univ ∩
              preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
                (PartialEquiv.source.{u_9, u_4} (β := F)
                    (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
                  Set M))),
    comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
        ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M) y =
      (e : (a : E) → F) y
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) : M → F) : M → F)
      ((⇑(Equiv.refl M) : (a : M) → M) ∘ (↑(extChartAt I x).symm : E → M) : E → M))
    ((extChartAt I x).target ∩
      (↑(extChartAt I x).symm : E → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_4} (β := F)
                (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
              Set M)))
    ((↑(extChartAt I x) : M → E) x)
have refine_2 : (↑(extChartAt I x) : M → E) x ∈
  (extChartAt I x).target ∩
    (↑(extChartAt I x).symm : E → M) ⁻¹'
      (univ ∩
        preimage (β := M) ((⇑(Equiv.refl M) : (a : M) → M) : (a : M) → M)
          (PartialEquiv.source.{u_9, u_4} (β := F)
              (extChartAt (I.transContinuousLinearEquiv e) ((Equiv.refl M : (a : M) → M) x)) :
            Set M))
Tactic: refine e.contDiff.contDiffWithinAt.congr_of_mem (fun y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
⊢ ContMDiffAt (I.transContinuousLinearEquiv e) I (M' := M) n (⇑(Equiv.refl M).symm : (a : M) → M) x
have refine : ContDiffWithinAt 𝕜 n
  (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
    ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
  ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
    (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
      (univ ∩
        preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
          (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
  ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)
Tactic: refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
    ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)
have refine_1 : ∀ (y : F)
  (hy :
    y ∈
      (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
        (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
          (univ ∩
            preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
              (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) :
                Set M))),
  comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M)
      y =
    (e.symm : (a : F) → E) y
Tactic: refine e.symm.contDiff.contDiffWithinAt.congr_of_mem (fun y hy => ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
refine_1 :
  ∀ (y : F)
    (hy :
      y ∈
        (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
          (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
            (univ ∩
              preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
                (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) :
                  Set M))),
    comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
        ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M)
        y =
      (e.symm : (a : F) → E) y
⊢ ContDiffWithinAt 𝕜 n
    (comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M))
    ((extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M)))
    ((↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x)
have refine_2 : (↑(extChartAt (I.transContinuousLinearEquiv e) x) : M → F) x ∈
  (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
    (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
      (univ ∩
        preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
          (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
Tactic: refine e.symm.contDiff.contDiffWithinAt.congr_of_mem (fun y hy => ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M' : Type u_10
inst_13 : TopologicalSpace M'
inst_14 : ChartedSpace H' M'
N : Type u_11
inst_15 : TopologicalSpace N
inst_16 : ChartedSpace G N
N' : Type u_12
inst_17 : TopologicalSpace N'
inst_18 : ChartedSpace G' N'
n : ℕ∞ω
e_1 e : E ≃L[𝕜] F
x : M
y : F
hy :
  y ∈
    (extChartAt (I.transContinuousLinearEquiv e) x).target ∩
      (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
        (univ ∩
          preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
            (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
⊢ comp (β := M) ((↑(extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : M → E) : M → E)
      ((⇑(Equiv.refl M).symm : (a : M) → M) ∘ (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) : F → M)
      y =
    (e.symm : (a : F) → E) y
have hy₁ : Membership.mem (γ := Set F) ((⇑e.symm : (a : F) → E) ⁻¹' (extChartAt I x).target) y ∧
  y ∈
    (↑(extChartAt (I.transContinuousLinearEquiv e) x).symm : F → M) ⁻¹'
      (univ ∩
        preimage (β := M) ((⇑(Equiv.refl M).symm : (a : M) → M) : (a : M) → M)
          (PartialEquiv.source.{u_9, u_2} (β := E) (extChartAt I (((Equiv.refl M).symm : (a : M) → M) x)) : Set M))
Tactic: simp only [mem_inter_iff, I.extChartAt_transContinuousLinearEquiv_target] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ Eq (α := M → M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl) Sum.inr
have h : ∀ (x : M), Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inl x) (Sum.inr x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
⊢ Eq (α := M' → M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr) Sum.inl
have h : ∀ (x : M'), Eq (α := M' ⊕ M) (comp (β := M ⊕ M') (⇑(sumComm I M n M') : (a : M ⊕ M') → M' ⊕ M) Sum.inr x) (Sum.inl x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := (M ⊕ M') ⊕ M'') I (M' := M ⊕ M' ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'') : (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'')
have hf : ContMDiff I (M := M ⊕ M') I (M' := M ⊕ M' ⊕ M'') n (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))
Tactic: apply ContMDiff.sumElim
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
hf : ContMDiff I (M := M ⊕ M') I (M' := M ⊕ M' ⊕ M'') n (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))
⊢ ContMDiff I (M := (M ⊕ M') ⊕ M'') I (M' := M ⊕ M' ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'') : (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'')
have hg : ContMDiff I (M := M'') I (M' := M ⊕ M' ⊕ M'') n (Sum.inr ∘ Sum.inr)
Tactic: apply ContMDiff.sumElim
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M ⊕ M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'').symm : (a : M ⊕ M' ⊕ M'') → (M ⊕ M') ⊕ M'')
have hf : ContMDiff I (M := M) I (M' := (M ⊕ M') ⊕ M'') n (Sum.inl ∘ Sum.inl)
Tactic: apply ContMDiff.sumElim
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
hf : ContMDiff I (M := M) I (M' := (M ⊕ M') ⊕ M'') n (Sum.inl ∘ Sum.inl)
⊢ ContMDiff I (M := M ⊕ M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'').symm : (a : M ⊕ M' ⊕ M'') → (M ⊕ M') ⊕ M'')
have hg : ContMDiff I (M := M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)
Tactic: apply ContMDiff.sumElim
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
⊢ (Opens.map α.hom.base).op = (Opens.map β.hom.base).op
have rw : (Opens.map β.hom.base).op = (Opens.map β.hom.base).op
Tactic: rw [w]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ (Opens.map β.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U
have subst : (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U
Tactic: subst h
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ α.hom = β.hom
have rw : β.hom = β.hom
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f g : X ⟶ Y
h : f.hom.base = g.hom.base
h' :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Eq (α :=
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x) ⟶
        X.presheaf.stalk x)
      (PresheafedSpace.Hom.stalkMap f.hom x) (Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ PresheafedSpace.Hom.stalkMap g.hom x)
⊢ f = g
have obtain : ∀ (f : (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat))
  (fc : Y.presheaf ⟶ obj (pushforward C f) X.presheaf)
  (h : PresheafedSpace.Hom.base (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) = g.hom.base)
  (h' :
    ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
      Eq (α :=
        Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom
                      { hom := { base := f, c := fc : X.Hom Y.toPresheafedSpace } :
                        InducedCategory.Hom (D := PresheafedSpace.{v, u, v} C) (F := toPresheafedSpace) X Y })) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
              x) ⟶
          X.presheaf.stalk x)
        (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) x)
        (Iso.hom (Y.presheaf.stalkCongr sorry) ≫ PresheafedSpace.Hom.stalkMap g.hom x)),
  { hom := { base := f, c := fc } } = g
Tactic: obtain ⟨f, fc⟩ := f
Cleared hypotheses: f, h, h'