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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball x r = s.inf fun i ↦ (p i).ball x r

Tactic:
rw [Finset.inf_eq_iInf]
  exact ball_finset_sup_eq_iInter _ _ _ hr

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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₃ 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₄ ∈ vectorSpan k {p₁, p₃}

Tactic:
← neg_vsub_eq_vsub_rev,

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₃ 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₆) ∈ vectorSpan k {p₁, p₃}
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:
by
  rintro x ⟨y, hy, h⟩
  rw [Seminorm.mem_closedBall_zero, ← h, map_smul_eq_mul]
  rw [Seminorm.mem_closedBall_zero] at hy
  gcongr

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
⊢ ∑ i, (b.coord i) v • b i = v

Tactic:
have hb := b.affineCombination_coord_eq_self v

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
inst✝³ : AddCommGroup V
inst✝² : Ring k
inst✝¹ : Module k V
inst✝ : Fintype ι
b : AffineBasis ι k V
v : V
hb : ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) v) = v
⊢ ∑ i, (b.coord i) v • b i = v
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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (((b.basisOf i).repr (p -ᵥ (v +ᵥ b i))).sum fun x ↦ id) = ((b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)).sum fun x ↦ id

Tactic:
congr! 1

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✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ (b.basisOf i).repr (p -ᵥ (v +ᵥ b i)) = (b.basisOf i).repr ((-v +ᵥ p) -ᵥ b i)
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
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst✝¹, _] ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen[inst✝¹] (q.ball 0 r)

Tactic:
rw [ball_zero_eq]

Goal state after:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst✝¹, _] ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen[inst✝¹] {y | q y < 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
⊢ w i0 = 0

Tactic:
have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]

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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
⊢ w i0 = 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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂) = affineSpan k (p '' (s₁ ∩ s₂))

Tactic:
classical
  ext p'
  simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
  constructor
  · rintro ⟨⟨fs₁, hfs₁, w₁, hw₁, rfl⟩, ⟨fs₂, hfs₂, w₂, hw₂, hw₁₂⟩⟩
    rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
    replace ha := ha fs₁ fs₂ w₁ w₂ hw₁ hw₂ hw₁₂
    refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩
    · rw [← hw₁, ← fs₁.sum_inter_add_sum_sdiff fs₂, eq_comm]
      convert! add_zero _
      refine Finset.sum_eq_zero ?_
      intro i hi
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁, ha, Set.indicator_of_notMem (by grind)]
    · rw [affineCombination_indicator_subset w₁ p Finset.inter_subset_left]
      refine affineCombination_congr (k := k) (P := P) _ ?_ (fun _ _ ↦ rfl)
      intro i hi
      rw [coe_inter, ← Set.indicator_indicator, Set.indicator_of_mem (by simpa using hi),
        Set.indicator_apply]
      simp only [mem_coe, left_eq_ite_iff]
      intro hi₂
      rw [← Set.indicator_of_mem (s := ↑fs₁) (by simpa using hi) w₁, ha]
      simp [hi₂]
  · grind

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (convexHull R) (range fun i ↦ Pi.single i 1) = stdSimplex R ι

Tactic:
by
  convert! convexHull_basis_eq_stdSimplex R ι
  aesop

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

Goal state before:
pp: S : Type u_1
inst✝¹ : Semiring S
inst✝ : PartialOrder S
s : ↑(stdSimplex S (Fin 2))
⊢ s 0 + s 1 = 1

Tactic:
simpa only [Fin.sum_univ_two] using sum_eq_one s

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

Goal state before:
pp: case pos
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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : ⊥ = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
eq_comm,

Goal state after:
case pos
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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₂) = ⊥
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case e'_2.e_6
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
x✝ : (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, w i ∈ I
hi0 : ∀ i ∉ fs, w i = 0
w' : Fin (m + 1) → k := ⋯
hw' : ∑ i, w' i = 1
hw'01 : (affineCombination k univ (s.face h).points) w' ∈ Simplex.setInterior I (s.face h)
⊢ w = (↑fs).indicator w

Tactic:
grind [Set.indicator_eq_self, mem_support]

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

Goal state before:
pp: case refine_1
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
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
hw' : ∑ j ∈ s, (r • (w₁ - w₂) - w) j = 0
hr' : (r • (w₁ - w₂) - w) i = 0
⊢ w i = r * (w₁ i - w₂ i)

Tactic:
eq_comm,

Goal state after:
case refine_1
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
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
hw' : ∑ j ∈ s, (r • (w₁ - w₂) - w) j = 0
hr' : (r • (w₁ - w₂) - w) i = 0
⊢ r * (w₁ i - w₂ i) = w i
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case inr
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
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hw1 : ∑ x ∈ univ.erase i, w x = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ ∃ j, w j = 0

Tactic:
Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)

Goal state after:
case inr
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
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hw1 : ∀ i_1 ∈ univ.erase i, w i_1 = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ ∃ j, w j = 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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0

Tactic:
intro v hv

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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
v : V
hv : v ∈ Basis.ofVectorSpaceIndex k V
⊢ v ≠ 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
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 ⋯
⊢ ∀ v ∈ h.extend ⋯, v ≠ 0

Tactic:
intro v hv

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
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 ⋯
v : V
hv : v ∈ h.extend ⋯
⊢ v ≠ 0
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case pos
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
exact hs.openSegment_interior_self_subset_interior hx' hy

Goal state after:
Module: Mathlib.Topology.Compactness.NhdsKer

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (nhdsKer s) ↔ IsCompact s

Tactic:
simp only [isCompact_iff_finite_subcover]
  peel with ι U hUo
  simp only [(isOpen_iUnion hUo).nhdsKer_subset,
    (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).nhdsKer_subset]

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₂
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0

Tactic:
let i₁ : { x // x ≠ (0 : Fin 2) } := ⟨1, by simp⟩

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, ⋯⟩
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs : (affineCombination k s p) w ∈ line[k, p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)

Tactic:
classical
    rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs
    refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_
    · rw [Finset.sum_pi_single', if_pos h₁]
    rw [Finset.affineCombinationLineMapWeights_apply_left h₂₃,
      Finset.affineCombinationLineMapWeights_apply_right h₂₃]
    simp_all only [sub_pos, sign_pos]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}

Tactic:
rcases ((Filter.basis_sets _).prod_nhds (Filter.basis_sets _)).tendsto_left_iff.1 this U hU
      with ⟨⟨V, W⟩, ⟨hV, hW⟩, hVW⟩

Goal state after:
case hsmul
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x ↦ x.1 • x.2) (𝓝 0) (𝓝 0)
V : Set 𝕜
W : Set E
hVW : Set.MapsTo (fun x ↦ x.1 • x.2) (id (V, W).1 ×ˢ id (V, W).2) U
hV : (V, W).1 ∈ 𝓝 0
hW : (V, W).2 ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∃ j ∈ 𝓝 0, V • {u | ∀ (x : α), φ u x ∈ j} ⊆ {u | ∀ (x : α), φ u x ∈ U}
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  use (s.sup p).ball 0 (r / 2)
  refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩
  refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_
  rw [hU, add_zero, add_halves]

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
⊢ ∃ C s, (s'.sup q).comp f ≤ C • s.sup p

Tactic:
obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p := by
    intro i hi
    refine (hf i).trans (IsOrderedSMul.smul_le_smul (Finset.le_sup hi) ?_)
    exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]

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
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace

Tactic:
by
      rw [UniformConvergenceCLM.instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]; rfl

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
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
𝔖 : Set (Set E)
s : Set E
hs : s ∈ 𝔖
U : Set F
hu : U ∈ 𝓝 0
⊢ ∀ᶠ (f : E →SLᵤ[σ, 𝔖] F) in 𝓝 0, MapsTo (⇑f) s U

Tactic:
by
  rw [nhds_zero_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : E
hx : 0 ⤳ x
⊢ 0 ⤳ f x

Tactic:
← map_zero f

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : E
hx : 0 ⤳ x
⊢ f 0 ⤳ f x
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
rcases mem_uniformity_isClosed hV with ⟨W, hW, hWc, hWU⟩

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U
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
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ 𝓝 f' = 𝓝 g

Tactic:
eq_comm,

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)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ 𝓝 g = 𝓝 f'
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t

Tactic:
by
  rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
⊢ Continuous fun p ↦ p.1 * p.2

Tactic:
refine continuous_of_continuous_uncurry _ ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : LocallyCompactSpace α
inst✝¹ : Mul β
inst✝ : ContinuousMul β
⊢ Continuous (Function.uncurry fun x y ↦ (x.1 * x.2) y)