-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem ContMDiffWithinAt.prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) :
    ContMDiffWithinAt I' I n (fun x ↦ ∏ i ∈ t, f i x) s x₀

Proof state:
case insert
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
i : ι
K : Finset ι
iK : i ∉ K
IH : (∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ K, f i x) s x₀
h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ insert i K, f i x) s x₀

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

Result:
case insert
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
i : ι
K : Finset ι
iK : i ∉ K
IH : (∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ K, f i x) s x₀
h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => f i x * ∏ i ∈ K, f i x) s x₀

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : 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 I' I n (fun x => ∏ i ∈ t, f i x) s x₀

Tactic:
induction' t using Finset.induction_on with i K iK IH

Result:
case empty
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ ∅, ContMDiffWithinAt I' I n (f i) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ ∅, f i x) s x₀

case insert
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
i : ι
K : Finset ι
iK : i ∉ K
IH : (∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ K, f i x) s x₀
h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ insert i K, f i x) s x₀

Proof state:
case insert
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
i : ι
K : Finset ι
iK : i ∉ K
IH : (∀ i ∈ K, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ K, f i x) s x₀
h : ∀ i_1 ∈ insert i K, ContMDiffWithinAt I' I n (f i_1) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => 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)

Result:
no goals

Proof state:
case empty
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
s : Set M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ ∅, ContMDiffWithinAt I' I n (f i) s x₀
⊢ ContMDiffWithinAt I' I n (fun x => ∏ i ∈ ∅, f i x) s x₀

Tactic:
simp [contMDiffWithinAt_const]

Result:
no goals