mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t u : Set α
⊢ Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u

Tactic:
by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_inter, eventually_and]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝³ : Monoid M
inst✝² : AddGroup E
inst✝¹ : DistribMulAction M E
inst✝ : Bornology M
s₁ s₂ t₁ t₂ : Set E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
⊢ Absorbs M (s₁ - s₂) (t₁ - t₂)

Tactic:
by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_neg

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})

Tactic:
exact .biUnion ht fun _ _ => hs.absorbs

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

Goal state before:
pp: case right
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
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₂ + ((v₁ +ᵥ p₁) -ᵥ p₂) = 0
⊢ False

Tactic:
← neg_neg v₂,

Goal state after:
case right
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
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : - -v₂ + ((v₁ +ᵥ p₁) -ᵥ p₂) = 0
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
⊢ affineSpan k s = ⊥ ↔ s = ∅

Tactic:
← not_iff_not,

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
⊢ ¬affineSpan k s = ⊥ ↔ ¬s = ∅
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ affineSpan k s
⊢ x ∈ Submodule.span k s

Tactic:
induction hx using affineSpan_induction' with

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ x, 1 < ‖x‖
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
have : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ x, 1 < ‖x‖
this : BoundedSpace 𝕜
⊢ Bornology.IsVonNBounded 𝕜 s
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
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
⊢ (affineCombination k s p₁) w₁ = (affineCombination k s p₂) w₂

Tactic:
by
  simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case empty
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = ↑(∅.sup fun i ↦ NNReal.mk ((p i) x) ⋯)

Tactic:
rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]
    norm_cast

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ 0 ∈ lowerBounds (range fun u ↦ p u + q (x - u))

Tactic:
rintro _ ⟨x, rfl⟩
    dsimp; positivity

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
⊢ (⨆ p, ⇑↑p) 0 = 0

Tactic:
iSup_apply,

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
⊢ ⨆ i, ↑i 0 = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
this : SeminormedAddCommGroup E := p.toSeminormedAddCommGroup
⊢ x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r

Tactic:
simp [closedBall_eq_metric]

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

Goal state before:
pp: case refine_2
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₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
← Submodule.map_le_iff_le_comap,

Goal state after:
case refine_2
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₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ Submodule.map φ.linear E.direction ≤ F.direction
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
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : s.sum (Function.const ι 1) = 1
hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) (Function.const ι 1)) = 1

Tactic:
b.coord_apply_combination_of_mem hi hw,

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
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : s.sum (Function.const ι 1) = 1
hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)
⊢ Function.const ι 1 i = 1
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₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
← Submodule.map_le_iff_le_comap,

Goal state after:
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₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ Submodule.map φ.linear E.direction ≤ F.direction
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
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
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w2 i0 - w1 i0 = 0

Tactic:
← Set.indicator_of_mem hi0 w2,

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
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
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ (↑s).indicator w2 i0 - w1 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
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : (affineCombination k s p) w₁ = (affineCombination k s p) w₂
hi : (↑s).indicator w₁ = (↑s).indicator w₂
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
intro i 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
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : (affineCombination k s p) w₁ = (affineCombination k s p) w₂
hi : (↑s).indicator w₁ = (↑s).indicator w₂
i : ι
hs : i ∈ s
⊢ w₁ i = w₂ 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
ι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
hw's : ∑ i ∈ fs', w' i = 0
hs' : (fs'.weightedVSub p) w' = 0
⊢ w i0 = w' (f i0)

Tactic:
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
ι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
hw's : ∑ i ∈ fs', w' i = 0
hs' : (fs'.weightedVSub p) w' = 0
⊢ w i0 = w i0
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b c d : E
⊢ (Path.segment a b).add (Path.segment c d) = Path.segment (a + c) (b + d)

Tactic:
by
  ext
  simp [lineMap_apply_module, add_add_add_comm]

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

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

Tactic:
simp only [h₁, h₂, false_and]

Goal state after:
case neg
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₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2
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
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I (s.face h)

Tactic:
let w' : Fin (m + 1) → k := w ∘ fs.orderEmbOfFin h
    have hw' : ∑ i, w' i = 1 := by
      rw [Fintype.sum_of_injective _ (fs.orderEmbOfFin h).injective w' w
        (fun i hi ↦ hi0 _ (by simpa using hi)) (fun _ ↦ rfl), hw]
    have hw'01 (i) : w' i ∈ I := hii (fs.orderEmbOfFin h i) (by simp)
    rw [← (s.face h).affineCombination_mem_setInterior_iff hw'] at hw'01
    convert! hw'01
    convert! Finset.univ.affineCombination_map (fs.orderEmbOfFin h).toEmbedding w s.points using 1
    simp only [map_orderEmbOfFin_univ, Finset.affineCombination_indicator_subset _ _ fs.subset_univ]
    congr
    grind [Set.indicator_eq_self, mem_support]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ (𝓝 (x, y)).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker

Tactic:
nhds_prod_eq,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker
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✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α) (b : β), 𝓝 (a, b) = 𝓟 (nhdsKer {(a, b)})

Tactic:
nhds_prod_eq,

Goal state after:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α) (b : β), 𝓝 a ×ˢ 𝓝 b = 𝓟 (nhdsKer {(a, b)})
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mpr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
⊢ (interior s).Nonempty → s.Nontrivial

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
⊢ s.Nontrivial
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst✝¹⁴ : Field 𝕜
inst✝¹³ : LinearOrder 𝕜
inst✝¹² : IsStrictOrderedRing 𝕜
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : OrderClosedTopology 𝕜
inst✝⁹ : CompactIccSpace 𝕜
inst✝⁸ : ContinuousAdd 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : ContinuousSMul 𝕜 V
inst✝² : AffineSpace V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact ((convexHull 𝕜) (range (s.map ↑(AffineEquiv.vaddConst 𝕜 (s.points 0)).symm ⋯).points))

Tactic:
exact (Set.finite_range _).isCompact_convexHull 𝕜

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

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
⊢ IsPathConnected (K.pi fun i ↦ pathComponentIn (t i) (x i))

Tactic:
rw [← univ_pi_piecewise_univ]

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
⊢ IsPathConnected (univ.pi (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) fun x ↦ univ))
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 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
⊢ ∑ i, w i.1 * v i.2 = 1

Tactic:
rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]

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
s t : Set E
⊢ (convexHull R) (s + t) = (convexHull R) s + (convexHull R) t

Tactic:
← add_image_prod,

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
s t : Set E
⊢ (convexHull R) ((fun x ↦ x.1 + x.2) '' s ×ˢ t) = (fun x ↦ x.1 + x.2) '' (convexHull R) s ×ˢ (convexHull R) t
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: 𝕜 : 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✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
𝔖 : Set (Set α)
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)
s : Set α
hs : s ∈ 𝔖
this : TopologicalSpace H :=
  TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)
x y : H
⊢ (s.domRestrict ∘ ⇑φ) (x + y) = (s.domRestrict ∘ ⇑φ) x + (s.domRestrict ∘ ⇑φ) y

Tactic:
exact congr_arg s.domRestrict (map_add φ x y)

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 → β
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
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
exact hf.map_sum_eq_iff h₀ h₁ hmem

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

Goal state before:
pp: case h
𝕜 : 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
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
⊢ (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
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)

Goal state after:
case h
𝕜 : 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
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
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
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range ⇑f
⊢ Function.Surjective ⇑f

Tactic:
rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe]

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
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range ⇑f
⊢ ball 0 r ⊆ Set.range ⇑↑f
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_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k ↦ (q i).comp (f k))
x : E
hx : ∀ (k : κ), (q i) ((f k) x) ≤ 1
⊢ x ∈ (⨆ i_1, (q i).comp (f i_1)).closedBall 0 1

Tactic:
simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using! hx

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

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (f (x - x')) y = (f x) y - (f x') y

Tactic:
by rw [map_sub, sub_apply]

Goal state after: