mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ g i = 0

Tactic:
rw [hfg]

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f ↑i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ↑r₁ = r₂
⊢ p₄ -ᵥ p₆ = ↑r₁ • (p₁ -ᵥ p₃)

Tactic:
rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
x : { x // x ≠ i1 }
⊢ f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)

Tactic:
rw [hfg]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
hι : IsEmpty ι
⊢ False

Tactic:
simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ k • p.closedBall 0 r ⊆ p.closedBall 0 (‖k‖ * r)

Tactic:
rintro x ⟨y, hy, h⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x ↦ k • x) y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r)
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty ↥E
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty ↥(map φ E)

Tactic:
exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹

Tactic:
Finset.centroid,

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) (Finset.centroidWeights k s)) = (↑s.card)⁻¹
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : Continuous[inst✝, _] ⇑p
r : ℝ
hr : 0 < r
⊢ p.ball 0 r ∈ 𝓝 0

Tactic:
by
  have : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
  simpa only [p.ball_zero_eq] using! this (Iio_mem_nhds hr)

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓝 0 ≤ comap norm (𝓝 0)

Tactic:
← tendsto_iff_comap

Goal state after:
case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ Tendsto norm (𝓝 0) (𝓝 0)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (affineCombination k s p) w₁ = (affineCombination k s p) w₂ ↔ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ s.affineCombination_congr h fun _ _ ↦ rfl⟩
  have hi := ha.indicator_eq_of_affineCombination_eq _ _ _ _ hw₁ hw₂ h
  intro i hs
  suffices Set.indicator s w₁ i = Set.indicator s w₂ i by simpa [hs] using this
  simp [hi]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁
hi₂ : i ∉ fs₂
⊢ w₁ i = 0

Tactic:
rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]

Goal state after:
case mp.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
i : ι
hi : i ∈ fs₁
hi₂ : i ∉ fs₂
⊢ (↑fs₂).indicator w₂ i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
he' : (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) = w
⊢ (∀ i ∈ fs,
      (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) i ∈ I) ∧
    ∀ i ∉ fs,
      (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) i = 0

Tactic:
refine ⟨fun i hi ↦ ?_, fun i hi ↦ by simp [hi]⟩

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi✝ : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
he' : (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) = w
i : Fin (n + 1)
hi : i ∈ fs
⊢ (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) i ∈ I
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ (affineCombination k s p) w = (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) c ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

Tactic:
rw [← AffineMap.apply_lineMap, ha.affineCombination_eq_iff_eq hw]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂) c i) ↔ ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c

k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
c : k
⊢ ∑ i ∈ s, (AffineMap.lineMap w₁ w₂) c i = 1
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ s = ∅ → nhdsKer s = ∅

Tactic:
rintro rfl; exact nhdsKer_empty

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑default -ᵥ ![p₁, p₂] 0 ≠ 0

Tactic:
he' default

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑i₁ -ᵥ ![p₁, p₂] 0 ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
⊢ AffineIndependent k f

Tactic:
have h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i} := Set.image_congr <| by simpa using congr_fun h₁

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i}
⊢ AffineIndependent k f
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • s.centerMass wx id + b • s.centerMass wy id ∈
    {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab

Goal state after:
case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ s.centerMass (fun i ↦ a * wx i + b * wy i) id ∈
    {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case snd
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ (∑ i, (fun p ↦ w p.1 * v p.2) i • (fun p ↦ (f p.1, g p.2)) i).2 = (x, y).2

Tactic:
simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)

pp: case neg
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∉ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)

Tactic:
· rw [b.coord_apply_combination_of_mem hi hw₁]
      exact hw₀ i hi

Goal state after:
case neg
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∉ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior

Tactic:
rw [Finset.affineCombination_indicator_subset _ _ u.subset_univ,
      affineCombination_mem_closedInterior_iff hw1']

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ ∀ (i : Fin (n + 1)), (↑u).indicator w i ∈ Icc 0 1
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
⊢ IsOpen[inst✝] U ↔ ∀ x ∈ U, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U

Tactic:
simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ WithSeminorms fun p ↦ ↑p

Tactic:
SeminormFamily.withSeminorms_iff_nhds_eq_iInf

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ 𝓝 0 = ⨅ i, comap (⇑↑i) (𝓝 0)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ ∀ (i : { p // Continuous[t, _] ⇑p }), 𝓝 0 ≤ comap (⇑↑i) (𝓝 0)

Tactic:
← tendsto_iff_comap

Goal state after:
case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] ⇑(p i)
⊢ ∀ (i : { p // Continuous[t, _] ⇑p }), Tendsto (⇑↑i) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
  congrm _ = ⨅ i, ?_
  exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
⊢ ∀ x ∈ S, ∀ y ∈ s, x y ∈ c • U

Tactic:
intro f hf x hx

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_6
inst✝⁵ : SeminormedRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : DistribMulAction R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
hS : IsVonNBounded R S
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ S
x : E
hx : x ∈ s
⊢ f x ∈ c • U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
⊢ (WithSeminorms fun x ↦ p) ↔ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms fun x ↦ p
⊢ p.ball 0 1 ∈ 𝓝 0

case refine_2
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms fun x ↦ p
⊢ IsVonNBounded 𝕜 (p.ball 0 1)

case refine_3
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
⊢ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) → WithSeminorms fun x ↦ p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ Tendsto (⇑f) (𝓝 0) (𝓝 0)

Tactic:
q.withSeminorms_iff_nhds_eq_iInf.mp hq,

Goal state after:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
⊢ Tendsto (⇑f) (𝓝 0) (⨅ i, comap (⇑(q i)) (𝓝 0))
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set E × ℝ
s : Set E
r : ℝ
x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : δ * ε < (s, r).2
f : E →SL[σ₁₂] F
x : E
hx : x ∈ (s, r).1
hf : ContinuousLinearMap.seminorm f < δ
⊢ ‖f x‖ ≤ r

Tactic:
exact le_trans (le_of_opNorm_le_of_le _ hf.le (hε _ hx)) hδ.le

Goal state after: