awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
H' : Type u_5
inst_8 : TopologicalSpace H'
E' : Type u_6
inst_9 : NormedAddCommGroup E'
inst_10 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst_11 : Monoid G'
inst_12 : TopologicalSpace G'
inst_13 : ChartedSpace H' G'
inst_14 : ContMDiffMul I' n G'
toMonoidHom : G →* G'
contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom : OneHom G G').toFun
toMonoidHom_1 : G →* G'
contMDiff_toFun_1 : ContMDiff I I' n (↑toMonoidHom_1 : OneHom G G').toFun
h :
  Eq (α := (a : G) → G')
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
      { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun })
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun)
      { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 })
⊢ { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } =
    { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 }
have mk : toMonoidHom = toMonoidHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
i : ι
K : Finset ι
iK : i ∉ K
IH :
  ∀ (h : ∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀),
    ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ K, f i x) s x₀
h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ insert i K, f i x) s x₀
have insert : ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ f i x * ∏ i ∈ K, f i x) s x₀
Tactic: simp only [iK, Finset.prod_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) s x₀
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContMDiffWithinAt I' I n (f i) s x₀),
  ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ ∅, f i x) s x₀
Tactic: induction t using Finset.induction_on with
  | empty => simp [contMDiffWithinAt_const]
  | insert i K iK IH =>
    simp only [iK, Finset.prod_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContMDiffWithinAt I' I n (f i) s x₀),
    ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ ∅, f i x) s x₀
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) s x₀
have insert : ∀ (i : ι) (K : Finset ι) (iK : i ∉ K)
  (IH :
    ∀ (h : ∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀),
      ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ K, f i x) s x₀)
  (h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀),
  ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ insert i K, f i x) s x₀
Tactic: induction t using Finset.induction_on with
  | empty => simp [contMDiffWithinAt_const]
  | insert i K iK IH =>
    simp only [iK, Finset.prod_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) s x₀
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContMDiffWithinAt I' I n (f i) s x₀),
  ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ ∅, f i x) s x₀
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp [contMDiffWithinAt_const]
  | insert i K iK IH =>
    simp only [iK, Finset.prod_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContMDiffWithinAt I' I n (f i) s x₀),
    ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ ∅, f i x) s x₀
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) s x₀
have insert : ∀ (i : ι) (K : Finset ι) (iK : i ∉ K)
  (IH :
    ∀ (h : ∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀),
      ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ K, f i x) s x₀)
  (h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀),
  ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ insert i K, f i x) s x₀
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp [contMDiffWithinAt_const]
  | insert i K iK IH =>
    simp only [iK, Finset.prod_insert, not_false_iff]
    exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
s : Set M
x : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) s x
have simp : ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ (∏ c ∈ t, f c) x) s x
Tactic: simp only [← Finset.prod_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀
⊢ ContMDiffAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ ∏ i ∈ t, f i x) x₀
have h₁ : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀
Tactic: simp only [← contMDiffWithinAt_univ] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst_1 : TopologicalSpace H
E : Type u_4
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst_4 : CommMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_6
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_7
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite.{u_1, u_8} (X := M) fun (i : ι) ↦ mulSupport (f i)
⊢ ContMDiff.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n fun (x : M) ↦ ∏ᶠ (i : ι) (_ : p i), f i x
have simp : ContMDiff.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n fun (x : M) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x
Tactic: simp only [← finprod_subtype_eq_finprod_cond]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiffAdd 𝓘(𝕜, E) n E
have contMDiff_add : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Monoid (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2
have contMDiff_add : ContMDiff (E := E × E) 𝓘(𝕜, E × E) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2
Tactic: rw [← modelWithCornersSelf_prod, chartedSpaceSelf_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SMul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
G' : Type u_11
inst_14 : TopologicalSpace G'
inst_15 : ChartedSpace H'' G'
inst_16 : Monoid G'
inst_17 : SMul G G'
inst_18 : MulAction G' M
inst_19 : SMul G M
inst_20 : IsScalarTower G G' M
n : ℕ∞ω
inst_21 : ContMDiffSMul I I'' n G G'
inst_22 : ContMDiffSMul I'' I' n G' M
⊢ ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ p.1 • p.2
have suffices : ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ HSMul.hSMul (β := G') p.1 1 • p.2
Tactic: suffices CMDiff n (fun p : G × M ↦ (p.1 • (1 : G')) • p.2) by simpa
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SMul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (E' := 𝕜 × E) 𝓘(𝕜, 𝕜 × E) n id
have rw : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) n id
Tactic: rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SMul (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : 𝕜 × E) ↦ p.1 • p.2
have h : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (E' := 𝕜 × E) 𝓘(𝕜, 𝕜 × E) n id
Tactic: have h : ContMDiff (𝓘(𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, 𝕜 × E) n (@id (𝕜 × E)) := by
      rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]; exact contMDiff_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SMul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
    (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id
have rw : ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
  (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) n id
Tactic: rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SMul (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst_4 : TopologicalSpace H'
E' : Type u_5
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst_7 : TopologicalSpace H''
E'' : Type u_7
inst_8 : NormedAddCommGroup E''
inst_9 : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst_10 : TopologicalSpace G
inst_11 : ChartedSpace H G
M : Type u_9
inst_12 : TopologicalSpace M
inst_13 : ChartedSpace H' M
N : Type u_10
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace H'' N
inst_16 : CompleteSpace E
n : ℕ∞ω
⊢ ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n
    fun (p : (E →L[𝕜] E) × E) ↦ p.1 • p.2
have h : ContMDiff (E := (E →L[𝕜] E) × E) (ModelWithCorners.prod 𝓘(𝕜, E →L[𝕜] E) 𝓘(𝕜, E)) (M := (E →L[𝕜] E) × E) (E' :=
  (E →L[𝕜] E) × E) 𝓘(𝕜, (E →L[𝕜] E) × E) n id
Tactic: have h : ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, (E →L[𝕜] E) × E) n
        (@id ((E →L[𝕜] E) × E)) := by
      rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]; exact contMDiff_id
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (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'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst_14 : Monoid G'
inst_15 : TopologicalSpace G'
inst_16 : ChartedSpace H' G'
inst_17 : ContMDiffMul I' n G'
G'' : Type u_11
inst_18 : Monoid G''
inst_19 : TopologicalSpace G''
inst_20 : ChartedSpace H'' G''
inst_21 : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff.{u_1, u_3, u_5, u_10, u_7, u_8, u_11} I' (M := G') I'' (M' := G'') n (⇑φ : (a : G') → G'')
⊢ Eq (α := C^n⟮I, N; I'', G''⟯)
    (Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
      (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑1 : (a : N) → G')) ⋯)
    1
have h : ∀ (x : N),
  Eq.{u_11 + 1} (α := G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
            (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑1 : (a : N) → G')) sorry :
          (a : N) → G'')
        x :
      G'')
    ((1 : (a : N) → G'') x : G'')
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (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'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst_14 : Monoid G'
inst_15 : TopologicalSpace G'
inst_16 : ChartedSpace H' G'
inst_17 : ContMDiffMul I' n G'
G'' : Type u_11
inst_18 : Monoid G''
inst_19 : TopologicalSpace G''
inst_20 : ChartedSpace H'' G''
inst_21 : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff.{u_1, u_3, u_5, u_10, u_7, u_8, u_11} I' (M := G') I'' (M' := G'') n (⇑φ : (a : G') → G'')
x : N
⊢ Eq.{u_11 + 1} (α := G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
            (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑1 : (a : N) → G')) ⋯ :
          (a : N) → G'')
        x :
      G'')
    ((1 : (a : N) → G'') x : G'')
have h : Eq.{u_11 + 1} (α := G'') ((φ : (a : G') → G'') 1 : G'') (1 : G'')
Tactic: change φ 1 = 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.SmoothFunctions (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'
H : Type u_4
inst_5 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst_7 : TopologicalSpace N
inst_8 : ChartedSpace H N
E'' : Type u_7
inst_9 : NormedAddCommGroup E''
inst_10 : NormedSpace 𝕜 E''
H'' : Type u_8
inst_11 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst_12 : TopologicalSpace N'
inst_13 : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst_14 : Monoid G'
inst_15 : TopologicalSpace G'
inst_16 : ChartedSpace H' G'
inst_17 : ContMDiffMul I' n G'
G'' : Type u_11
inst_18 : Monoid G''
inst_19 : TopologicalSpace G''
inst_20 : ChartedSpace H'' G''
inst_21 : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff.{u_1, u_3, u_5, u_10, u_7, u_8, u_11} I' (M := G') I'' (M' := G'') n (⇑φ : (a : G') → G'')
f g : C^n⟮I, N; I', G'⟯
⊢ Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
      (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑(f * g) : (a : N) → G')) ⋯ =
    Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
        (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑f : (a : N) → G')) ⋯ *
      Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
        (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑g : (a : N) → G')) ⋯
have h : ∀ (x : N),
  Eq.{u_11 + 1} (α := G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
            (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑(f * g) : (a : N) → G')) sorry :
          (a : N) → G'')
        x :
      G'')
    ((Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
              (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑f : (a : N) → G')) sorry *
            Subtype.mk (p := fun (f : N → G'') ↦ ContMDiff I I'' n f)
              (Function.comp.{u_6 + 1, u_10 + 1, u_11 + 1} (β := G') (⇑φ : (a : G') → G'') (⇑g : (a : N) → G')) sorry :
          (a : N) → G'')
        x :
      G'')
Tactic: ext x