awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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 : DivInvMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
x : M
c : G
hf : ContMDiffAt I' I n f x
⊢ ContMDiffAt.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x / c) x

Tactic:
hf.div_const c

Premises used: ContMDiffAt, ContMDiffWithinAt.div_const
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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 : DivInvMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
s : Set M
c : G
hf : ContMDiffOn I' I n f s
⊢ ContMDiffOn.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n (fun (x : M) ↦ f x / c) s

Tactic:
fun x hx ↦ (hf x hx).div_const c

Premises used: ContMDiffWithinAt.div_const, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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 : DivInvMonoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
E' : Type u_5
inst_8 : NormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
H' : Type u_6
inst_10 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H' M
f : M → G
c : G
hf : ContMDiff I' I n f
⊢ ContMDiff.{u_1, u_5, u_6, u_7, u_3, u_2, u_4} I' I (M' := G) n fun (x : M) ↦ f x / c

Tactic:
fun x ↦ (hf x).div_const c

Premises used: ContMDiffAt.div_const, ContMDiff
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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'
G : Type u_8
inst_7 : TopologicalSpace G
inst_8 : ChartedSpace H G
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H' M
inst_11 : SMul G M
n m : ℕ∞ω
h : n ≤ m
inst_12 : ContMDiffSMul I I' m G M
⊢ ContMDiffSMul I I' n G M

Tactic:
⟨contMDiff_smul.of_le h⟩

Premises used: ContMDiffSMul.contMDiff_smul, ContMDiff.of_le, ContMDiffSMul.mk
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' ∞ G M
inst_18 : ENat.LEInfty n
⊢ ContMDiffSMul I I' n G M

Tactic:
.of_le ENat.LEInfty.out

Premises used: ContMDiffSMul.of_le, ENat.LEInfty.out
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' ω G M
⊢ ContMDiffSMul I I' n G M

Tactic:
.of_le le_top

Premises used: ContMDiffSMul.of_le, le_top
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
inst_17 : ContinuousSMul G M
⊢ ContMDiffSMul I I' 0 G M

Tactic:
⟨contMDiff_zero_iff.2 continuous_smul⟩

Premises used: Iff.mpr, contMDiff_zero_iff, ContMDiffSMul.mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
inst_17 : ContMDiffSMul I I' 2 G M
⊢ ContMDiffSMul I I' 1 G M

Tactic:
.of_le one_le_two

Premises used: ContMDiffSMul.of_le, one_le_two
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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'
G : Type u_8
inst_7 : TopologicalSpace G
inst_8 : ChartedSpace H G
M : Type u_9
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace H' M
inst_11 : SMul G M
n : ℕ∞ω
inst_12 : ContMDiffSMul I I' n G M
⊢ ContinuousSMul G M

Tactic:
⟨(contMDiff_smul (I := I) (I' := I') (n := n)).continuous⟩

Premises used: ContMDiff.continuous, ContMDiffSMul.contMDiff_smul, ContinuousSMul.mk
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' n G M
f : N → G
g : N → M
s : Set N
x : N
hf : ContMDiffWithinAt I'' I n f s x
hg : ContMDiffWithinAt I'' I' n g s x
⊢ ContMDiffWithinAt I'' I' n (f • g) s x

Tactic:
(contMDiff_smul (I := I) (I' := I')).contMDiffAt.comp_contMDiffWithinAt x (hf.prodMk hg)

Premises used: ContMDiffWithinAt.prodMk, ContMDiffSMul.contMDiff_smul, ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' n G M
f : N → G
g : N → M
x : N
hf : ContMDiffAt I'' I n f x
hg : ContMDiffAt I'' I' n g x
⊢ ContMDiffAt I'' I' n (f • g) x

Tactic:
hf.smul hg

Premises used: ContMDiffWithinAt.smul, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' n G M
f : N → G
g : N → M
s : Set N
hf : ContMDiffOn I'' I n f s
hg : ContMDiffOn I'' I' n g s
⊢ ContMDiffOn I'' I' n (f • g) s

Tactic:
fun x hx ↦ (hf x hx).smul (hg x hx)

Premises used: ContMDiffWithinAt.smul, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : SMul G M
n : ℕ∞ω
inst_17 : ContMDiffSMul I I' n G M
f : N → G
g : N → M
hf : ContMDiff I'' I n f
hg : ContMDiff I'' I' n g
⊢ ContMDiff I'' I' n (f • g)

Tactic:
fun x ↦ (hf x).smul (hg x)

Premises used: ContMDiff, ContMDiffAt.smul
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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
this : ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ HSMul.hSMul (β := G') p.1 1 • p.2
⊢ ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ p.1 • p.2

Tactic:
simpa
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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
suffices : ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ HSMul.hSMul (β := G') p.1 1 • p.2
⊢ ContMDiff (I.prod I') I' (M' := M) n fun (p : G × M) ↦ p.1 • p.2

Tactic:
suffices CMDiff n (fun p : G × M ↦ (p.1 • (1 : G')) • p.2) by simpa
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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) ↦ HSMul.hSMul (β := G') p.1 1 • p.2

Tactic:
(contMDiff_fst.smul contMDiff_const).smul (I := I'') contMDiff_snd

Premises used: ContMDiff.smul, contMDiff_snd, contMDiff_const, contMDiff_fst
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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) ↦ HSMul.hSMul (β := G') p.1 1 • p.2

Tactic:
exact (contMDiff_fst.smul contMDiff_const).smul (I := I'') contMDiff_snd

Premises used: ContMDiff.smul, contMDiff_snd, contMDiff_const, contMDiff_fst
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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
inst_14 : Monoid G
inst_15 : MulAction G M
n : ℕ∞ω
inst_16 : ContMDiffSMul I I' n G M
G' : Type u_11
inst_17 : TopologicalSpace G'
inst_18 : ChartedSpace H'' G'
inst_19 : Monoid G'
f : G' →* G
hf : ContMDiff.{u_1, u_7, u_6, u_11, u_3, u_2, u_8} I'' (M := G') I (M' := G) n (⇑f : (a : G') → G)
x : MulAction G' M := compHom M f
⊢ ContMDiffSMul I'' I' n G' M

Tactic:
⟨(hf.comp contMDiff_fst).smul contMDiff_snd⟩

Premises used: ContMDiff.comp, ContMDiff.smul, contMDiff_snd, ContMDiffSMul.mk, contMDiff_fst
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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
inst_14 : Monoid G
inst_15 : MulAction G M
n : ℕ∞ω
inst_16 : ContMDiffSMul I I' n G M
G' : Type u_11
inst_17 : TopologicalSpace G'
inst_18 : ChartedSpace H'' G'
inst_19 : Monoid G'
f : G' →* G
hf : ContMDiff.{u_1, u_7, u_6, u_11, u_3, u_2, u_8} I'' (M := G') I (M' := G) n (⇑f : (a : G') → G)
x : MulAction G' M := compHom M f
⊢ ContMDiffSMul I'' I' n G' M

Tactic:
exact ⟨(hf.comp contMDiff_fst).smul contMDiff_snd⟩
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : ℕ∞ω
rw : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) n id
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (E' := 𝕜 × E) 𝓘(𝕜, 𝕜 × E) n id

Tactic:
rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]

Premises used: contMDiff_prod_iff, contMDiff_prod_module_iff
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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) (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) n id

Tactic:
contMDiff_id

Premises used: contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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) (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) n id

Tactic:
exact contMDiff_id

Premises used: contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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

Tactic:
have h : ContMDiff (𝓘(𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, 𝕜 × E) n (@id (𝕜 × E)) := by
      rw [contMDiff_prod_module_iff, ← contMDiff_prod_iff]; exact contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Algebra.SMul
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 : ℕ∞ω
h : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) (M := 𝕜 × E) (E' := 𝕜 × E) 𝓘(𝕜, 𝕜 × E) n id
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : 𝕜 × E) ↦ p.1 • p.2

Tactic:
contDiff_smul.contMDiff.comp h

Premises used: ContMDiff.comp, ContDiff.contMDiff, contDiff_smul