awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I 1 G
a b : G
⊢ (MDiffAt fun (x : G) ↦ x * a) b

Tactic:
contMDiffAt_mul_right.mdifferentiableAt one_ne_zero

Premises used: ContMDiffAt.mdifferentiableAt, contMDiffAt_mul_right, one_ne_zero
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
g h : G
inst_7 : ContMDiffMul I ∞ G
⊢ (𝑳 I g : (a : G) → G) h = g * h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_4
inst_4 : Mul G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
g h : G
inst_7 : ContMDiffMul I ∞ G
⊢ (𝑹 I g : (a : G) → G) h = h * g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h : G
h₁ :
  ∀ (x : G), Eq (α := G) ((𝑳 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) x : G)
⊢ Eq (α := C^∞⟮I, G; I, G⟯) (𝑳 I (g * h)) (ContMDiffMap.comp (𝑳 I g) (𝑳 I h))

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h x : G
⊢ Eq (α := G) ((𝑳 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑳 I g) (𝑳 I h) : (a : G) → G) x : G)

Tactic:
simp only [ContMDiffMap.comp_apply, L_apply, mul_assoc]

Premises used: mul_assoc, L_apply, ContMDiffMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h : G
h₁ :
  ∀ (x : G), Eq (α := G) ((𝑹 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑹 I h) (𝑹 I g) : (a : G) → G) x : G)
⊢ Eq (α := C^∞⟮I, G; I, G⟯) (𝑹 I (g * h)) (ContMDiffMap.comp (𝑹 I h) (𝑹 I g))

Tactic:
ext
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G : Type u_8
inst_4 : Semigroup G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I ∞ G
g h x : G
⊢ Eq (α := G) ((𝑹 I (g * h) : (a : G) → G) x : G) ((ContMDiffMap.comp (𝑹 I h) (𝑹 I g) : (a : G) → G) x : G)

Tactic:
simp only [ContMDiffMap.comp_apply, R_apply, mul_assoc]

Premises used: mul_assoc, R_apply, ContMDiffMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G' : Type u_8
inst_4 : Monoid G'
inst_5 : TopologicalSpace G'
inst_6 : ChartedSpace H G'
inst_7 : ContMDiffMul I ∞ G'
g' : G'
⊢ (𝑳 I g' : (a : G') → G') 1 = g'

Tactic:
mul_one g'

Premises used: mul_one
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
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
G' : Type u_8
inst_4 : Monoid G'
inst_5 : TopologicalSpace G'
inst_6 : ChartedSpace H G'
inst_7 : ContMDiffMul I ∞ G'
g' : G'
⊢ (𝑹 I g' : (a : G') → G') 1 = g'

Tactic:
one_mul g'

Premises used: one_mul
-- Module: Mathlib.Geometry.Manifold.Algebra.Monoid
Goal:
𝕜_1 : Type u_1
inst : NontriviallyNormedField 𝕜_1
H_1 : Type u_2
inst_1 : TopologicalSpace H_1
E_1 : Type u_3
inst_2 : NormedAddCommGroup E_1
inst_3 : NormedSpace 𝕜_1 E_1
I_1 : ModelWithCorners 𝕜_1 E_1 H_1
n : ℕ∞ω
G_1 : Type u_4
inst_4 : Mul G_1
inst_5 : TopologicalSpace G_1
inst_6 : ChartedSpace H_1 G_1
E'_1 : Type u_5
inst_7 : NormedAddCommGroup E'_1
inst_8 : NormedSpace 𝕜_1 E'_1
H'_1 : Type u_6
inst_9 : TopologicalSpace H'_1
I'_1 : ModelWithCorners 𝕜_1 E'_1 H'_1
M : Type u_7
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H'_1 M
g h : G_1
inst_12 : ContMDiffMul I_1 ∞ G_1
𝕜 : Type u_8
inst_13 : NontriviallyNormedField 𝕜
E : Type u_9
inst_14 : NormedAddCommGroup E
inst_15 : NormedSpace 𝕜 E
H : Type u_10
inst_16 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_11
inst_17 : TopologicalSpace G
inst_18 : ChartedSpace H G
inst_19 : Mul G
inst_20 : ContMDiffMul I n G
E' : Type u_12
inst_21 : NormedAddCommGroup E'
inst_22 : NormedSpace 𝕜 E'
H' : Type u_13
inst_23 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_14
inst_24 : TopologicalSpace G'
inst_25 : ChartedSpace H' G'
inst_26 : Mul G'
inst_27 : ContMDiffMul I' n G'
⊢ ContMDiffMul (I.prod I') n (G × G')

Tactic:
{ IsManifold.prod G G' with
    contMDiff_mul :=
      ((contMDiff_fst.comp contMDiff_fst).mul (contMDiff_fst.comp contMDiff_snd)).prodMk
        ((contMDiff_snd.comp contMDiff_fst).mul (contMDiff_snd.comp contMDiff_snd)) }

Premises used: ContMDiff.comp, ContMDiff.mul, contMDiff_snd, ContMDiffMul.mk, IsManifold.prod, contMDiff_fst, ContMDiff.prodMk
-- 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 : Monoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
⊢ ContMDiff I I (M' := G) n fun (a : G) ↦ HPow.hPow (β := ℕ) a 0

Tactic:
simp only [pow_zero, contMDiff_const]

Premises used: contMDiff_const, pow_zero
-- 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 : Monoid G
inst_5 : TopologicalSpace G
inst_6 : ChartedSpace H G
inst_7 : ContMDiffMul I n G
k : ℕ
⊢ ContMDiff I I (M' := G) n fun (a : G) ↦ a ^ (k + 1)

Tactic:
simpa [pow_succ] using (contMDiff_pow _).mul contMDiff_id

Premises used: pow_succ, ContMDiff.mul, contMDiff_id
-- 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 : 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'
f g : ContMDiffMonoidMorphism I I' n G G'
h :
  Eq (α := (a : G) → G') ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) f)
    ((fun (a : ContMDiffMonoidMorphism I I' n G G') ↦ (↑a.toMonoidHom : OneHom G G').toFun) g)
mk :
  ∀ (toMonoidHom : G →* G') (contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom : 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) g)),
    { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } = g
⊢ f = g

Tactic:
cases f
-- 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 : 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'
g : ContMDiffMonoidMorphism I I' n G G'
toMonoidHom : G →* G'
contMDiff_toFun : ContMDiff I I' n (↑toMonoidHom : 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) g)
mk :
  ∀ (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 }
⊢ { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } = g

Tactic:
cases g
-- 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 : 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 })
mk : toMonoidHom = toMonoidHom_1
⊢ { toMonoidHom := toMonoidHom, contMDiff_toFun := contMDiff_toFun : ContMDiffMonoidMorphism I I' n G G' } =
    { toMonoidHom := toMonoidHom_1, contMDiff_toFun := contMDiff_toFun_1 }

Tactic:
congr
-- 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 : 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_1

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- 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 : 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_1

Tactic:
exact DFunLike.ext' h

Premises used: DFunLike.ext'
-- 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 : ι), 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:
simp [contMDiffWithinAt_const]

Premises used: contMDiffWithinAt_const
-- 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
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.insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
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₀
⊢ 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.insert i K, f i x)
    s x₀

Tactic:
simp only [iK, Finset.prod_insert, not_false_iff]

Premises used: Finset.prod_insert, not_false_iff
-- 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
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) ↦ f i x * ∏ i ∈ K, f i x) s x₀

Tactic:
(h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, 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
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) ↦ f i x * ∏ i ∈ K, f i x) s x₀

Tactic:
exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, 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₀
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₀
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.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.insert i K, 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₀

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)

Premises used: Finset.prod_insert, contMDiffWithinAt_const, Insert.insert, not_false_iff
-- 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₀
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₀
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.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.insert i K, 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₀

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)

Premises used: Finset.prod_insert, contMDiffWithinAt_const, Insert.insert, not_false_iff
-- 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)
x₀ : M
h : ∀ (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:
let ⟨_I, hI⟩ := finprod_eventually_eq_prod lf x₀
  (ContMDiffWithinAt.prod fun i _hi ↦ h i).congr_of_eventuallyEq
    (eventually_nhdsWithin_of_eventually_nhds hI) hI.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, ContMDiffWithinAt, finprod_eventually_eq_prod, ContMDiffWithinAt.prod, eventually_nhdsWithin_of_eventually_nhds, _private.0.contMDiffWithinAt_finprod.match_1, finprod, ContMDiffWithinAt.congr_of_eventuallyEq