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

Goal state before:
pp: 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
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)

Tactic:
← direction_affineSpan,

Goal state after:
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
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ affineSpan k s₂ = ⊥)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mpr
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✝ : Fintype ι
p : ι → P
⊢ (∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0) → AffineIndependent k p

Tactic:
intro h s w hw hs i hi

Goal state after:
case mpr
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✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₃ ∈ line[k, p₁, p₂]

pp: case refine_2
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
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ ∈ line[k, p₁, p₂]

Tactic:
· convert! smul_vsub_vadd_mem_affineSpan_pair (-r₁ * (r₂ - r₁)⁻¹) p₁ p₂
    simp [mul_smul, ← hr, hp₁]

Goal state after:
case refine_2
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
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ ∈ line[k, p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case neg
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₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₂₁ : p₃ -ᵥ p₂ ∈ vectorSpan k {p₁, p₃}
⊢ False

Tactic:
← direction_affineSpan,

Goal state after:
case neg
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₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₂₁ : p₃ -ᵥ p₂ ∈ line[k, p₁, p₃].direction
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp [pointwise_vadd_eq_map, vadd_eq_iff_eq_neg_vadd]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
this : Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = vectorSpan k (range ⇑b)
⊢ ⊤ ≤ vectorSpan k (range ⇑b)

Tactic:
← direction_affineSpan,

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
this : Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = vectorSpan k (range ⇑b)
⊢ ⊤ ≤ (affineSpan k (range ⇑b)).direction
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
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
refine .of_norm ⟨r, fun a ha x hx => ?_⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ p.ball 0 r₂
⊢ x ∈ a • p.ball 0 r₁
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 :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
⊢ (affineCombination k s p) w2 = p i0

Tactic:
simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ (fun z ↦ -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}

Tactic:
preimage_univ,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_3
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c‖ ^ n * ε ≤ p x

Tactic:
exact (le_div_iff₀ εpos).1 hn.1

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).closedBall 0 r)

Tactic:
exact (normSeminorm _ _).balanced_closedBall_zero r

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ (fun a ↦ (lineMap x y) ↑a) '' Ioc 0 1 = Ioc x y

Tactic:
← image_image _ Subtype.val (Ioc 0 1)

Goal state after:
x y : ℝ
h : x < y
⊢ ⇑(lineMap x y) '' Subtype.val '' Ioc 0 1 = Ioc x y
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : f q = p
⊢ p ∈ affineSpan k (⇑f '' Set.range s.points)

Tactic:
← AffineSubspace.map_span,

Goal state after:
case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : f q = p
⊢ p ∈ AffineSubspace.map f (affineSpan k (Set.range s.points))
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ ¬∃ x ∈ Simplex.setInterior I s, f x = p

Tactic:
contrapose hp
      obtain ⟨q, hq, hqp⟩ := hp
      rw [s.map_points, Set.range_comp, ← AffineSubspace.map_span, AffineSubspace.mem_map]
      exact ⟨q, (Set.mem_of_mem_of_subset hq s.setInterior_subset_affineSpan), hqp⟩

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

Goal state before:
pp: case inr
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
have h0 : ∀ v : V, v ∈ h.extend (Set.subset_univ _) → v ≠ 0 := by
      intro v hv
      simpa [bsv] using bsv.ne_zero ⟨v, hv⟩

Goal state after:
case inr
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_2.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
hloc : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfin : {i | ¬PathConnectedSpace (Z i)}.Finite
⊢ LocallyPathConnectedSpace ((i : ι) → Z i)

Tactic:
exact locallyPathConnectedSpace_of_finite_not_pathConnectedSpace hfin

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x)) = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x)

Tactic:
by
      congrm f ?_
      match_scalars <;> simp [field, c]

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
p₁ p₂ : E
⊢ vectorSpan R ((convexHull R) {p₁, p₂}) = R ∙ (p₂ -ᵥ p₁)

Tactic:
← direction_affineSpan,

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
p₁ p₂ : E
⊢ (affineSpan R ((convexHull R) {p₁, p₂})).direction = R ∙ (p₂ -ᵥ p₁)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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 t₁ t₂ : Finset E
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ (convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂

Tactic:
by
  classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
    simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]

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

Goal state before:
pp: case refine_1.refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ (p i).ball 0 ε ∈ p.moduleFilterBasis.toFilterBasis

Tactic:
← (Finset.sup_singleton : _ = p i)

Goal state after:
case refine_1.refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ({i}.sup p).ball 0 ε ∈ p.moduleFilterBasis.toFilterBasis
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
⊢ p ∈ {x | ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = x} ↔
    p ∈ s.closedInterior

Tactic:
Set.mem_ofPred

Goal state after:
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
⊢ (∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p) ↔
    p ∈ s.closedInterior
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ LocallyConvexSpace ℝ E

Tactic:
have := hp.topologicalAddGroup
  apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
  · rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
    exact FilterBasis.hasBasis _
  · intro s hs
    change s ∈ Set.iUnion _ at hs
    simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs
    rcases hs with ⟨I, r, _, rfl⟩
    exact convex_ball _ _ _

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
exact .iInf fun t ↦ hts t.1 t.2

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
⊢ Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p

Tactic:
refine ⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ V
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst✝ : CompactSpace ↑s
⊢ (Continuous[inst✝¹, UniformFun.topologicalSpace (↑s) β] fun x ↦
      UniformFun.ofFun ⇑{ toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    Continuous[inst✝¹, topologicalSpace α β {s}] fun x ↦ (ofFun {s}) (f x)

Tactic:
UniformOnFun.continuous_rng_iff

Goal state after:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
X : Type u_1
inst✝¹ : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst✝ : CompactSpace ↑s
⊢ (Continuous[inst✝¹, UniformFun.topologicalSpace (↑s) β] fun x ↦
      UniformFun.ofFun ⇑{ toFun := s.domRestrict (f x), continuous_toFun := ⋯ }) ↔
    ∀ s_1 ∈ {s},
      Continuous[inst✝¹, UniformFun.topologicalSpace (↑s_1) β]
        (⇑UniformFun.ofFun ∘ s_1.domRestrict ∘ ⇑(toFun {s}) ∘ fun x ↦ (ofFun {s}) (f x))
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
x : E
⊢ ‖c x‖ * ‖f‖ ≤ ‖c‖ * ‖x‖ * ‖f‖

Tactic:
gcongr; apply le_opNorm

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
⊢ ‖c‖ * ‖f‖ ≤ ‖smulRight c f‖

Tactic:
rw [← le_div_iff₀ hf]
      refine opNorm_le_bound _ (by positivity) fun x => ?_
      rw [div_mul_eq_mul_div, le_div_iff₀ hf]
      calc
        ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
        _ = ‖smulRight c f x‖ := rfl
        _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x

Tactic:
have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
⊢ IsComplete {g | EqOn (⇑g) f s}

Tactic:
intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
by_cases ha₀ : a = 0

Goal state after:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

Tactic:
by_cases ha₀ : a = 0

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

case neg
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'

Tactic:
by_cases h : i' = i

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'

case neg
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'