mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n = p n

Tactic:
← Nat.succ_pred_eq_of_pos h

Goal state after:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n.pred.succ = p n.pred.succ
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: case e'_2.e'_1
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
x✝ : Fin n
⊢ y x✝ = y x✝ • 1 x✝

Tactic:
simp only [Pi.one_apply, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖f ⟨k, ⟨l, ⟨s, hs⟩⟩⟩‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Tactic:
exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _

Goal state after:
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this : ↑‖y - x‖₊ < r
⊢ x + (y - x) ∈ insert x s

Tactic:
by simpa using! h.1

Goal state after:
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
v : Fin 1 → E
⊢ (id 𝕜 E x 1) v = v ⟨0, ⋯⟩

Tactic:
apply id_apply_one

Goal state after:
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.removeZero.rightInv i x = p.rightInv i x

Tactic:
ext1 n
  induction n using Nat.strong_induction_on with | _ n IH
  match n with
  | 0 => simp only [rightInv_coeff_zero]
  | 1 => simp only [rightInv_coeff_one]
  | n + 2 =>
    simp only [rightInv, neg_inj]
    rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
    congr (config := { closePost := false }) 2 with k
    by_cases hk : k < n + 2 <;> simp [hk, IH]

Goal state after:
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi : (m ≤ ⟨n, f⟩.fst ∧ ⟨n, f⟩.fst < M) ∧ ∀ (a : Fin ⟨n, f⟩.fst), 1 ≤ ⟨n, f⟩.snd a ∧ ⟨n, f⟩.snd a < N
⊢ (n : ℕ) × Composition n

Tactic:
refine ⟨∑ j, f j, ofFn fun a => f a, fun {i} hi' => ?_, by simp [sum_ofFn]⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
m M N n : ℕ
f : Fin n → ℕ
hi : (m ≤ ⟨n, f⟩.fst ∧ ⟨n, f⟩.fst < M) ∧ ∀ (a : Fin ⟨n, f⟩.fst), 1 ≤ ⟨n, f⟩.snd a ∧ ⟨n, f⟩.snd a < N
i : ℕ
hi' : i ∈ ofFn fun a ↦ f a
⊢ 0 < i
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
| c.blocks

Tactic:
rw [← List.ofFn_get c.blocks]

Goal state after:
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
| ofFn c.blocks.get
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
⊢ ∃ δ, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
exact ⟨δ, δpos, fun {z} hz => Hδ (by rwa [Set.inter_comm])⟩

Goal state after:
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k =
    I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n))

Tactic:
by
          rw [geom_sum_Ico' _ In]; exact ne_of_lt (rSn.trans_lt (by norm_num))

Goal state after:
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a = a'

Tactic:
ext1

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
a' : Composition n
b' : Composition a'.length
h : ⟨a, b⟩.fst.blocks = ⟨a', b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a', b'⟩.snd.blocks
⊢ a.blocks = a'.blocks
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b = b'

Tactic:
ext1

Goal state after:
n : ℕ
a : Composition n
b b' : Composition a.length
h : ⟨a, b⟩.fst.blocks = ⟨a, b'⟩.fst.blocks
h' : ⟨a, b⟩.snd.blocks = ⟨a, b'⟩.snd.blocks
⊢ b.blocks = b'.blocks
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ a = a'

Tactic:
ext1

Goal state after:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ a.blocks = a'.blocks
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ ⟨a, b⟩ = ⟨a, b'⟩

Tactic:
ext1

Goal state after:
case fst
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ ⟨a, b⟩.fst = ⟨a, b'⟩.fst

case snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
⊢ ⟨a, b⟩.snd ≍ ⟨a, b'⟩.snd
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i ↦ (b i).blocks) = fun i ↦ (b' i).blocks
i : Fin a.length
⊢ b i = b' i

Tactic:
ext1

Goal state after:
case snd
n : ℕ
a : Composition n
b b' : (i : Fin a.length) → Composition (a.blocksFun i)
H : (fun i ↦ (b i).blocks) = fun i ↦ (b' i).blocks
i : Fin a.length
⊢ (b i).blocks = (b' i).blocks
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) =o[𝕜; L] fun p ↦ p.1 - p.2

Tactic:
calc (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2))
    _ =o[𝕜; L] (fun p ↦ f p.1 - f p.2) :=
      hg.isLittleOTVS.comp_tendsto hL
    _ =O[𝕜; L] (fun p ↦ p.1 - p.2) := hf.isBigOTVS_sub

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
y : F
hg : HasFDerivWithinAt g g' t y
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x

Tactic:
subst y; exact hg.comp_hasFDerivAt x hf ht

Goal state after:
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
⊢ { blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
      { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } =
    c

Tactic:
ext1

Goal state after:
case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
⊢ ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).blocks =
    c.blocks
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt 𝕜 (∑ n ∈ N, f n) c

Tactic:
by
  simp_rw [← analyticWithinAt_univ] at h ⊢
  exact N.analyticWithinAt_sum h

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
c : F
⊢ HasFDerivAtFilter (fun x ↦ c + f x) f' L ↔ HasFDerivAtFilter f f' L

Tactic:
by
  simpa only [add_comm] using hasFDerivAtFilter_add_const_iff c

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
⊢ (fderiv 𝕜 fun x ↦ ↑L ∘SL f x) = fun x ↦ ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x

Tactic:
ext x : 1
  exact fderiv_continuousLinearEquiv_comp L f x

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (g₁ + g₂) = f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂

Tactic:
ext1

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
x✝ : ι → M
⊢ (f.compContinuousAlternatingMap (g₁ + g₂)) x✝ =
    (f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂) x✝
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (c • g) = c • f.compContinuousAlternatingMap g

Tactic:
ext1

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M [⋀^ι]→L[R] N
x✝ : ι → M
⊢ (f.compContinuousAlternatingMap (c • g)) x✝ = (c • f.compContinuousAlternatingMap g) x✝
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: case e'_6.e'_1.inr
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : i ≠ a
⊢ (Function.update (fun x ↦ g) b dg i) (v i) =
    ((fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) ∘ ⇑(Equiv.swap a b)) i

Tactic:
rcases eq_or_ne i b with rfl | hib

Goal state after:
case e'_6.e'_1.inr.inl
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a i : ι
hia : i ≠ a
heq : v a = v i
hne : a ≠ i
⊢ (Function.update (fun x ↦ g) i dg i) (v i) =
    ((fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) ∘ ⇑(Equiv.swap a i)) i

case e'_6.e'_1.inr.inr
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : i ≠ a
hib : i ≠ b
⊢ (Function.update (fun x ↦ g) b dg i) (v i) =
    ((fun j ↦ (Function.update (fun x ↦ g) a dg j) (v j)) ∘ ⇑(Equiv.swap a b)) i
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x y : F
⊢ (f (x + y)).mkContinuous (C * ‖x + y‖) ⋯ = (f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯

Tactic:
ext1

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x y : F
x✝ : ι → E
⊢ ((f (x + y)).mkContinuous (C * ‖x + y‖) ⋯) x✝ = ((f x).mkContinuous (C * ‖x‖) ⋯ + (f y).mkContinuous (C * ‖y‖) ⋯) x✝
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
c : 𝕜
x : F
⊢ (f (c • x)).mkContinuous (C * ‖c • x‖) ⋯ = (RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯

Tactic:
ext1

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
c : 𝕜
x : F
x✝ : ι → E
⊢ ((f (c • x)).mkContinuous (C * ‖c • x‖) ⋯) x✝ = ((RingHom.id 𝕜) c • (f x).mkContinuous (C * ‖x‖) ⋯) x✝
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
x y : E
⊢ (f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯ =
    (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯ +
      (f (Function.update m i y)).mkContinuous (C * ∏ i_1, ‖Function.update m i y i_1‖) ⋯

Tactic:
ext1

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
x y : E
x✝ : ι' → F
⊢ ((f (Function.update m i (x + y))).mkContinuous (C * ∏ i_1, ‖Function.update m i (x + y) i_1‖) ⋯) x✝ =
    ((f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯ +
        (f (Function.update m i y)).mkContinuous (C * ∏ i_1, ‖Function.update m i y i_1‖) ⋯)
      x✝
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
c : 𝕜
x : E
⊢ (f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯ =
    c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯

Tactic:
ext1

Goal state after:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
ι' : Type u_1
inst✝¹ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
inst✝ : DecidableEq ι
m : ι → E
i : ι
c : 𝕜
x : E
x✝ : ι' → F
⊢ ((f (Function.update m i (c • x))).mkContinuous (C * ∏ i_1, ‖Function.update m i (c • x) i_1‖) ⋯) x✝ =
    (c • (f (Function.update m i x)).mkContinuous (C * ∏ i_1, ‖Function.update m i x i_1‖) ⋯) x✝