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

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)

Tactic:
simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
    smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
    ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • f x + b • f y) < a • (g ∘ f) x + b • (g ∘ f) y

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (g ∘ f) (a • x + b • y) ≤ g (a • f x + b • f y)

Tactic:
· exact hg.right (mem_image_of_mem f hx) (mem_image_of_mem f hy) (hf'.ne hx hy hxy) ha hb hab

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (g ∘ f) (a • x + b • y) ≤ g (a • f x + b • f y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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 : AffineSubspace k P
inst✝ : Nonempty ↥s
a b : ↥s.direction
c : ↥s
⊢ (a + b) +ᵥ c = a +ᵥ b +ᵥ c

Tactic:
by
    ext
    apply add_vadd

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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
| vectorSpan k s

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_sdiff_singleton, Set.image_insert_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
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
| Submodule.span k (insert (p -ᵥ p) ((fun x ↦ x -ᵥ p) '' (s \ {p})))
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
ext y

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ
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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ x ∈ insert i0 l.support, (l x - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i) x) = 0

Tactic:
Finset.sum_sub_distrib,

Goal state after:
ι : 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, l i -
      ∑ x ∈ insert i0 l.support, Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i) x =
    0
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✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i, (↑s).indicator w i = 1

Tactic:
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]

Goal state after:
ι : 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✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ (∑ x, if x ∈ s then w x else 0) = ∑ i ∈ s, w i
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case mpr
ι : 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✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ ((insert j s).weightedVSubOfPoint p (p j)) w' +ᵥ p j ∈ affineSpan k (Set.range p)

Tactic:
←
        (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)

Goal state after:
case mpr
ι : 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✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (Finset.affineCombination k (insert j s) p) w' ∈ affineSpan k (Set.range p)
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
⊢ ∑ i ∈ s, w1 i = 1

Tactic:
rw [Finset.sum_update_of_mem hi0]

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 :
  ∀ (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
⊢ 1 + ∑ x ∈ s \ {i0}, const ι 0 x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
⊢ ∀ (p : (ι → P) × P) (v : (ι → V) × V),
    (s.weightedVSubOfPoint (v +ᵥ p).1 (v +ᵥ p).2) w =
      (∑ i ∈ s, w i • (LinearMap.proj i ∘ₗ LinearMap.fst k (ι → V) V - LinearMap.snd k (ι → V) V)) v +ᵥ
        (s.weightedVSubOfPoint p.1 p.2) w

Tactic:
rintro ⟨p, b⟩ ⟨v, b'⟩
    simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub,
     vadd_vsub_assoc, ← sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib]

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 : ℝ
⊢ p.ball x r = {x_1 | x_1 ∈ (fun z ↦ -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}

Tactic:
ext y

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 ∈ (fun z ↦ -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
this : (s.sup p) x ≠ 0
y : E
hle : ε / ‖c‖ ≤ (s.sup p) y
hlt : (s.sup p) y < ε
i : ι
hi : i ∈ s
hiy : (s.sup p) y = (p i) y
⊢ q y ≤ C • (s.sup p) y

Tactic:
hiy

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
this : (s.sup p) x ≠ 0
y : E
hle : ε / ‖c‖ ≤ (s.sup p) y
hlt : (s.sup p) y < ε
i : ι
hi : i ∈ s
hiy : (s.sup p) y = (p i) y
⊢ q y ≤ C • (p i) y
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
hac : c = a
hbd : d = b
⊢ (Path.segment a b).cast hac hbd = Path.segment c d

Tactic:
subst_vars

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
c d : E
⊢ (Path.segment c d).cast ⋯ ⋯ = Path.segment c d
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2.inl
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)

Tactic:
have : Subsingleton V := Module.subsingleton k _
      have : Subsingleton P := (AddTorsor.subsingleton_iff V P).1 inferInstance
      rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (by simp)]
      simp

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

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝² : Semiring 𝕜
inst✝¹ : PartialOrder 𝕜
inst✝ : Fintype ι
⊢ stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1}

Tactic:
ext f

Goal state after:
𝕜 : Type u_2
ι : Type u_1
inst✝² : Semiring 𝕜
inst✝¹ : PartialOrder 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x, f x = 1}
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
ι : Type u_5
α : Type u_7
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : Module R α
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid α
inst✝ : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ ∑ i ∈ s, w i • f i ≤ ∑ i ∈ s, w i • s.sup' ⋯ f

Tactic:
exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

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
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 := w ∘ ⇑(fs.orderEmbOfFin h)
⊢ ∑ i, w' i = 1

Tactic:
rw [Fintype.sum_of_injective _ (fs.orderEmbOfFin h).injective w' w
        (fun i hi ↦ hi0 _ (by simpa using hi)) (fun _ ↦ rfl), hw]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
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
⊢ ∑ x ∈ s, (r • w₁ x - r • w₂ x - w x) = 0

Tactic:
Finset.sum_sub_distrib,

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
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
⊢ ∑ x ∈ s, r • w₁ x - ∑ x ∈ s, r • w₂ x - ∑ x ∈ s, w x = 0
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
⊢ s.closedInterior \ s.interior = ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
simpa [closedInterior_eq_interior_union] using
    fun i ↦ (s.disjoint_interior_closedInterior_faceOpposite i).symm

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}

Tactic:
conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
U_op : IsOpen[inst✝¹] U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U

Tactic:
have := U_op.locallyPathConnectedSpace

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
U_op : IsOpen[inst✝¹] U
this : LocallyPathConnectedSpace ↑U
⊢ ConnectedSpace ↑U ↔ PathConnectedSpace ↑U
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine .iInf fun b => ?_

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * ‖x‖) • x ∈ U
⊢ x ∈ U

Tactic:
inv_mul_cancel₀ (by simp_all),

Goal state after:
case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : 1 • x ∈ U
⊢ x ∈ U
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 : Set E
⊢ (convexHull R) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t

Tactic:
refine Subset.antisymm ?_ ?_

Goal state after:
case refine_1
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 : Set E
⊢ (convexHull R) s ⊆ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t

case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
⊢ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t ⊆ (convexHull R) s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
⊢ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t ⊆ (convexHull R) s

Tactic:
· exact iUnion_subset fun i => iUnion_subset convexHull_mono

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
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} ↔
    x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Tactic:
refine ⟨?_, fun hx => ?_⟩

Goal state after:
case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} →
    x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x}
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
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Tactic:
refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩

Goal state after:
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
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ W ∈ p.addGroupFilterBasis.sets, Metric.ball 0 √r • W ⊆ U
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
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ (∑ i ∈ s', q i).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
← pullback_apply,

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
⊢ (pullback f) (∑ i ∈ s', q i) ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
by
  rw [← p.filter_eq_iInf]
  refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩
  rw [h.topology_eq_withSeminorms]
  exact AddGroupFilterBasis.nhds_zero_eq _

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
i : ι
hi : i ∈ I
⊢ 0 < I.sup' ⋯ r

Tactic:
exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)

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
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x y : E
⊢ dist (f x) (f y) ≤ ‖f‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, ← map_sub, f.le_opNorm]

Goal state after: