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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h✝ : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ x + y = x + 0

Tactic:
rw [← h, add_zero]

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

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
S : AffineSpace V P
ι : Type u_4
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i ↦ p ↑i) w

Tactic:
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]

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
S : AffineSpace V P
ι : Type u_4
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs,
      ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯)) w) ↔
    ∃ fs w,
      ∑ i ∈ fs, w i = 1 ∧ p0 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) (Classical.choice ⋯)) w
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: ι : Type u_1
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
inst✝ : Nonempty ι
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
rcases subsingleton_or_nontrivial k with hs | hn
  · have hnv := Module.subsingleton k V
    rw [AddTorsor.subsingleton_iff V P] at hnv
    rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (Set.range_nonempty p)]
    simp
  · exact affineCombination_mem_affineSpan h p

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
by
  simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]
  refine fun a ha b hb ↦ mul_lt_mul' ha hb (apply_nonneg _ _) ?_
  exact hr₁.lt_or_gt.resolve_left <| ((norm_nonneg a).trans ha).not_gt

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

Goal state before:
pp: ι : Type u_1
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
p : ι → P
s : Set ι
fs' : Finset ↑s
w' : ↑s → k
hw' : ∑ i ∈ fs', w' i = 1
h : (Finset.affineCombination k fs' fun x ↦ p ↑x) w' ∈ affineSpan k (Set.range fun x ↦ p ↑x)
⊢ (Finset.affineCombination k fs' fun x ↦ p ↑x) w' =
    (Finset.affineCombination k fs' (p ∘ Subtype.val)) ((fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0) ∘ Subtype.val)

Tactic:
exact fs'.affineCombination_congr (by simp) (by simp)

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 : ι
⊢ (range fun j ↦ b ↑j -ᵥ b i) = (fun x ↦ x -ᵥ b i) '' ⇑b '' (univ \ {i})

Tactic:
ext v

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 : ι
v : V
⊢ (v ∈ range fun j ↦ b ↑j -ᵥ b i) ↔ v ∈ (fun x ↦ x -ᵥ b i) '' ⇑b '' (univ \ {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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x ↦ ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
⊢ Subtype.val = (fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f

Tactic:
ext v

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
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x ↦ ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
x✝ : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
v : { x // x ∈ (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) }
⊢ ↑v = ((fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩) ∘ f) v
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).coord i = (b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap

Tactic:
ext v

Goal state after:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
v : V
⊢ ((a • b).coord i) v = ((b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap) v
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
i j : ι
ha : LinearIndependent k fun i ↦ p ↑i -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ p ↑⟨i, hij'⟩ = p j

Tactic:
simp_all only [ne_eq]

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (p '' s1)
hp0s2 : p0 ∈ affineSpan k (p '' s2)
hp0' : p0 ∈ affineSpan k (p '' (s1 ∩ s2))
he : ¬(s1 ∩ s2).Nonempty
⊢ False

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at he

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
p0 : P
hp0s1 : p0 ∈ affineSpan k (p '' s1)
hp0s2 : p0 ∈ affineSpan k (p '' s2)
hp0' : p0 ∈ affineSpan k (p '' (s1 ∩ s2))
he : s1 ∩ s2 = ∅
⊢ False
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 ι
hs₁₂ : affineSpan k (p '' s₁) = affineSpan k (p '' s₂)
hne : s₁ ≠ s₂
i : ι
⊢ p i ∈ affineSpan k (p '' s₁) ↔ p i ∈ affineSpan k (p '' s₂)

Tactic:
hs₁₂

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : OrderClosedTopology 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ IsClosed (stdSimplex 𝕜 ι)

Tactic:
rw [stdSimplex_eq_inter]
  apply IsClosed.inter
  · apply isClosed_iInter
    exact fun i ↦ isClosed_le continuous_const (continuous_apply i)
  · exact isClosed_eq (by fun_prop) continuous_const

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
h : IsEmpty ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
⊢ ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)

Tactic:
ext v

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
v : V
⊢ f.linear v = (⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)) v
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this : ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)
⊢ Continuous (⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)) ↔ Continuous ⇑f

Tactic:
simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
by
  refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi) <;>
    simpa [sub_mul, sub_smul, sub_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
inst✝ : PartialOrder k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
⊢ Disjoint s.interior (s.face h).closedInterior

Tactic:
by
  refine Set.disjoint_left.mpr fun p hleft hright ↦ ?_
  have hp : p ∈ affineSpan k (Set.range s.points) :=
    Set.mem_of_mem_of_subset hleft <| s.interior_subset_closedInterior.trans <|
      s.closedInterior_subset_affineSpan
  grind [affineCombination_mem_interior_iff, affineCombination_mem_closedInterior_face_iff_mem_Icc,
    eq_affineCombination_of_mem_affineSpan_of_fintype]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ i, U i → ∃ t, nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
peel with ι U hUo

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen (U i)
⊢ (nhdsKer s ⊆ ⋃ i, U i → ∃ t, nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔ s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : IndiscreteTopology α
⊢ ∀ (S : Set (Set α)), (∀ s ∈ S, IsOpen[inst✝²] s) → IsOpen[inst✝²] (⋂₀ S)

Tactic:
by grind [isOpen_iff]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : ConnectedSpace X
⊢ ∀ (x y : X), Joined x y

Tactic:
simp [← mem_pathComponent_iff, IsClopen.pathComponent _ |>.eq_univ]

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

Goal state before:
pp: case inr.refine_2.hn
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ (↑(affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b)) ∩ ↑(affineSpan k s)).Nonempty

Tactic:
use p

Goal state after:
case h
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ p ∈ ↑(affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b)) ∩ ↑(affineSpan k s)
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : LocallyConvexSpace 𝕜 E
s : Set E
hs : Convex 𝕜 s
x₀ : E
hx₀s : x₀ ∈ s
p : E → Prop
u : Set E
h : ∀ ⦃x : E⦄, x ∈ id u → x ∈ s → p x
hu_nhds : u ∈ 𝓝 x₀
hu_convex : Convex 𝕜 u
x : E
hxu : x ∈ id u
hxs : x ∈ s
y : E
hy : y ∈ [x₀ -[𝕜] x]
⊢ [x₀ -[𝕜] x] ⊆ u

Tactic:
exact hu_convex.segment_subset (mem_of_mem_nhds hu_nhds) hxu

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

Goal state before:
pp: case coe
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : NNReal
⊢ Convex ℝ (eball a ↑r)

Tactic:
simp [eball_coe, convex_ball]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : ℝ
⊢ Convex ℝ (closedBall a r)

Tactic:
simpa only [closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r

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

Goal state before:
pp: case refine_2
𝕜 : 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 → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)

Tactic:
grind [hf.map_sum_eq_iff_of_pos h₀ h₁ hmem]

Goal state after:
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 ∈ (convexHull 𝕜) (range s.points) ↔ p ∈ s.closedInterior

Tactic:
convexHull_range_eq_exists_affineCombination,

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
⊢ 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
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_def, neg_apply, norm_neg]

Goal state after:
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_9
ι' : Type u_10
inst✝⁶ : AddCommGroup E
inst✝⁵ : NormedField 𝕝
inst✝⁴ : Module 𝕝 E
inst✝³ : AddCommGroup F
inst✝² : NormedField 𝕝₂
inst✝¹ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝ : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ C • s.sup p
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)

Tactic:
rw [← finset_sup_smul] at hC

Goal state after:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : AddCommGroup E
inst✝⁵ : NormedField 𝕝
inst✝⁴ : Module 𝕝 E
inst✝³ : AddCommGroup F
inst✝² : NormedField 𝕝₂
inst✝¹ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝ : RingHomIsometric τ₁₂
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous[x✝¹, _] ⇑((q i).comp f)
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case pos.refine_1
𝕜 : 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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : c = 0
x : E
hx : x ∈ ball 0 ε
⊢ ε * ‖c‖ ≤ ‖x‖

Tactic:
simp [h0]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ p.moduleFilterBasis.topology ≤ q.moduleFilterBasis.topology

Tactic:
rw [← continuous_id_iff_le]

Goal state after:
case refine_1
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Continuous[p.moduleFilterBasis.topology, q.moduleFilterBasis.topology] id
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ q.moduleFilterBasis.topology ≤ p.moduleFilterBasis.topology

Tactic:
rw [← continuous_id_iff_le]

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Continuous[q.moduleFilterBasis.topology, p.moduleFilterBasis.topology] id
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h✝ : Nontrivial E
this : NormedSpace ℝ E
⊢ ∀ a ∈ (fun x ↦ ‖f x‖₊) '' sphere 0 1, a ≤ ‖f‖₊

pp: case inr.refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h✝ : Nontrivial E
this : NormedSpace ℝ E
ub : ℝ≥0
hub : ub < ‖f‖₊
⊢ ∃ a ∈ (fun x ↦ ‖f x‖₊) '' sphere 0 1, ub < a

Tactic:
· rintro - ⟨x, hx, rfl⟩
    simpa only [mul_one] using! f.le_opNorm_of_le (mem_sphere_zero_iff_norm.1 hx).le

Goal state after:
case inr.refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h✝ : Nontrivial E
this : NormedSpace ℝ E
ub : ℝ≥0
hub : ub < ‖f‖₊
⊢ ∃ a ∈ (fun x ↦ ‖f x‖₊) '' sphere 0 1, ub < a
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: 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

Tactic:
exact liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose h))

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Tactic:
· exact stronglyMeasurable_const

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
⊢ s₁ = s₂

Tactic:
by
    cases isEmpty_or_nonempty α
    · have : Subsingleton C(α, R) := DFunLike.coe_injective.subsingleton
      subsingleton
    · inhabit α
      ext f
      have h : f = algebraMap R C(α, R) (f default) := by
        ext x'
        simp only [mul_one, smul_eq_mul, algebraMap_apply]
        congr
        simp [eq_iff_true_of_subsingleton]
      rw [h]
      simp only [Subalgebra.algebraMap_mem]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
    Measure.count t * ((Measure.count t)⁻¹ * Measure.count (t ∩ u)) * (Measure.count (s ∪ t))⁻¹

Tactic:
← mul_assoc

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ +
    Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹