awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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 (∏ i ∈ t, f i) s x

Tactic:
Finset.prod_induction f (fun f ↦ CMDiffAt[s] n f x) (fun _ _ hf hg ↦ hf.mul hg)
    (contMDiffWithinAt_const (c := 1)) h

Premises used: ContMDiffWithinAt, contMDiffWithinAt_const, Finset.prod_induction, ContMDiffWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
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
⊢ 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

Tactic:
simp only [← Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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) ↦ (∏ c ∈ t, f c) x) s x

Tactic:
contMDiffWithinAt_finsetProd' h

Premises used: contMDiffWithinAt_finsetProd'
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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) ↦ (∏ c ∈ t, f c) x) s x

Tactic:
exact contMDiffWithinAt_finsetProd' h

Premises used: contMDiffWithinAt_finsetProd'
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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₀
⊢ ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀

Tactic:
simp only [← contMDiffWithinAt_univ] at *

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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, ContMDiffWithinAt I' I n (f i) Set.univ 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) Set.univ x₀

Tactic:
ContMDiffWithinAt.prod h

Premises used: ContMDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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, ContMDiffWithinAt I' I n (f i) Set.univ 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) Set.univ x₀

Tactic:
exact ContMDiffWithinAt.prod h

Premises used: ContMDiffWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
f : ι → M → G
lf : LocallyFinite.{u_1, u_8} (X := M) fun (i : ι) ↦ mulSupport (f i)
h : ∀ (i : ι), 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 : ι), f i x) x₀

Tactic:
contMDiffWithinAt_finprod lf h

Premises used: contMDiffWithinAt_finprod, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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 (∏ i ∈ t, f i) x

Tactic:
contMDiffWithinAt_finsetProd' h

Premises used: contMDiffWithinAt_finsetProd', ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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

Tactic:
contMDiffWithinAt_finsetProd h

Premises used: contMDiffWithinAt_finsetProd, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
f : ι → M → G
lf : LocallyFinite.{u_1, u_8} (X := M) fun (i : ι) ↦ mulSupport (f i)
h : ∀ (i : ι), ContMDiffOn I' I n (f i) s
⊢ ContMDiffOn.{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

Tactic:
fun x hx ↦
  contMDiffWithinAt_finprod lf fun i ↦ h i x hx

Premises used: contMDiffWithinAt_finprod, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s
⊢ ContMDiffOn.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (∏ i ∈ t, f i) s

Tactic:
fun x hx ↦ contMDiffWithinAt_finsetProd' fun i hi ↦ h i hi x hx

Premises used: contMDiffWithinAt_finsetProd', ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s
⊢ ContMDiffOn.{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

Tactic:
fun x hx ↦ contMDiffWithinAt_finsetProd fun i hi ↦ h i hi x hx

Premises used: contMDiffWithinAt_finsetProd, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiff I' I n (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 ∈ t, f i x

Tactic:
fun x ↦ ContMDiffAt.prod fun j hj ↦ h j hj x

Premises used: ContMDiff, ContMDiffAt.prod
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiff I' I n (f i)
⊢ ContMDiff.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' (M := M) I (M' := G) n (∏ i ∈ t, f i)

Tactic:
fun x ↦ contMDiffAt_finsetProd' fun i hi ↦ h i hi x

Premises used: ContMDiff, contMDiffAt_finsetProd'
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiff I' I n (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 ∈ t, f i x

Tactic:
fun x ↦ contMDiffAt_finsetProd fun i hi ↦ h i hi x

Premises used: contMDiffAt_finsetProd, ContMDiff
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
h : ∀ (i : ι), ContMDiff I' I n (f i)
hfin : 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 : ι), f i x

Tactic:
fun x ↦ contMDiffAt_finprod hfin fun i ↦ h i x

Premises used: ContMDiff, contMDiffAt_finprod
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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)
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
⊢ 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

Tactic:
simp only [← finprod_subtype_eq_finprod_cond]

Premises used: finprod_subtype_eq_finprod_cond
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x

Tactic:
contMDiff_finprod (fun i ↦ hc i i.2) (hf.comp_injective Subtype.coe_injective)

Premises used: contMDiff_finprod, Subtype.coe_injective, LocallyFinite.comp_injective, Subtype.val, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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) ↦ ∏ᶠ (j : Subtype p), f (↑j : ι) x

Tactic:
exact contMDiff_finprod (fun i ↦ hc i i.2) (hf.comp_injective Subtype.coe_injective)
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : 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
g : M → G
hg : ContMDiffWithinAt I' I n g s x
m : ℕ
⊢ ContMDiffWithinAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ g x ^ m) s x

Tactic:
(contMDiff_pow m).contMDiffAt.comp_contMDiffWithinAt x hg

Premises used: contMDiff_pow, ContMDiff.contMDiffAt, ContMDiffAt.comp_contMDiffWithinAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : 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
g : M → G
hg : ContMDiffAt I' I n g x
m : ℕ
⊢ ContMDiffAt.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ g x ^ m) x

Tactic:
hg.pow m

Premises used: ContMDiffWithinAt.pow, ContMDiffAt
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : 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
g : M → G
hg : ContMDiffOn I' I n g s
m : ℕ
⊢ ContMDiffOn.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n (fun (x : M) ↦ g x ^ m) s

Tactic:
fun x hx ↦ (hg x hx).pow m

Premises used: ContMDiffWithinAt.pow, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : 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
g : M → G
hg : ContMDiff I' I n g
m : ℕ
⊢ ContMDiff.{u_2, u_6, u_7, u_8, u_4, u_3, u_5} I' I (M' := G) n fun (x : M) ↦ g x ^ m

Tactic:
fun x ↦ (hg x).pow m

Premises used: ContMDiff, ContMDiffAt.pow
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
contMDiff_add : ContMDiff (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2
⊢ ContMDiffAdd 𝓘(𝕜, E) n E

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
contMDiff_add : ContMDiff (E := E × E) 𝓘(𝕜, E × E) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2
⊢ ContMDiff (ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, E)) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2

Tactic:
rw [← modelWithCornersSelf_prod, chartedSpaceSelf_prod]

Premises used: chartedSpaceSelf_prod, modelWithCornersSelf_prod
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff (E := E × E) 𝓘(𝕜, E × E) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2

Tactic:
contDiff_add.contMDiff

Premises used: setOf, ContDiff.contMDiff, contDiff_add, instTopologicalSpaceModelProd._aux_1, ModelProd
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff (E := E × E) 𝓘(𝕜, E × E) 𝓘(𝕜, E) (M' := E) n fun (p : E × E) ↦ p.1 + p.2

Tactic:
exact contDiff_add.contMDiff

Premises used: ContDiff.contMDiff, contDiff_add
-- 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
x : M
c : G
hf : ContMDiffWithinAt I' I n f s x
⊢ ContMDiffWithinAt.{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 x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const

Premises used: contMDiffWithinAt_const, div_eq_mul_inv, ContMDiffWithinAt.mul