mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : k
p : ι → P
⊢ (AffineMap.lineMap ((affineCombination k s p) w₁) ((affineCombination k s p) w₂)) r =
    (affineCombination k s p) ((AffineMap.lineMap w₁ w₂) r)

Tactic:
Finset.affineCombination_apply,

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
s : Finset ι
w₁ w₂ : ι → k
r : k
p : ι → P
⊢ (AffineMap.lineMap ((s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +ᵥ Classical.choice ⋯)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯)) w₂ +ᵥ Classical.choice ⋯))
      r =
    (s.weightedVSubOfPoint p (Classical.choice ⋯)) ((AffineMap.lineMap w₁ w₂) r) +ᵥ Classical.choice ⋯
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : IsOrderedAddMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ 2⁻¹ • f z + 2⁻¹ • f z = f z

Tactic:
by rw [← _root_.add_smul]; norm_num

Goal state after:
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
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ x✝ ∈ (fun x ↦ a • x) ⁻¹' p.ball y r ↔ x✝ ∈ p.ball (a⁻¹ • y) (r / ‖a‖)

Tactic:
by
    rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Goal state after:
Module: Mathlib.Analysis.Seminorm

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

Tactic:
show ε / ‖c‖ ≤ p (c ^ (-(n + 1)) • x)

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

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

Tactic:
mul_inv_cancel₀ (ne_of_gt cpos),

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

Goal state before:
pp: 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
inst✝ : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
⊢ s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs

Tactic:
rw [range_face_points]

Goal state after:
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
inst✝ : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
⊢ s.points i ∈ affineSpan k (s.points '' ↑fs) ↔ i ∈ fs
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: 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)
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ w i = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [range_faceOpposite_points] at h
    exact s.independent.eq_zero_of_affineCombination_mem_affineSpan hw h (Finset.mem_univ i)
      (by simp)
  · rw [range_faceOpposite_points]
    rcases subsingleton_or_nontrivial k with hk | hk
    · 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
    · exact affineCombination_mem_affineSpan_image hw (by simpa using h) s.points

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : ∑ x, f x = 1
⊢ f ∈ [Pi.single 0 1 -[𝕜] Pi.single 1 1]

Tactic:
rw [Fin.sum_univ_two] at hf₁

Goal state after:
𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ f ∈ [Pi.single 0 1 -[𝕜] Pi.single 1 1]
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
v : V
| v⁻¹

Tactic:
equals p /ₛ (v • p) => rw [sdiv_smul_eq_sdiv_div, sdiv_self, one_div]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen[inst✝] U → s ⊆ U → x ∈ U

Tactic:
by simp [nhdsKer_def]

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

Goal state before:
pp: E : Type u_3
𝕜 : Type u_4
inst✝¹¹ : Field 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : OrderClosedTopology 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact ((convexHull 𝕜) s)

Tactic:
hs.convexHull_eq_image

Goal state after:
E : Type u_3
𝕜 : Type u_4
inst✝¹¹ : Field 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : OrderClosedTopology 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) '' stdSimplex 𝕜 ↑s)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: E : Type u_3
𝕜 : Type u_4
inst✝¹¹ : Field 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : OrderClosedTopology 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact ((convexHull 𝕜) s)

Tactic:
rw [hs.convexHull_eq_image]
  let := hs.fintype
  exact (isCompact_stdSimplex 𝕜 s).image (LinearMap.continuous_on_pi _)

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ (affineCombination R (s ∪ s') v) W = a • (affineCombination R s v) w + b • (affineCombination R s' v) w'

Tactic:
· simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']

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✝⁴ : 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:
by
  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.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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y = 1

Tactic:
· rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]

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

Goal state before:
pp: case refine_3
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x

Tactic:
· rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)},
    (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → s = Set.univ → x ∈ (convexHull 𝕜) (s.pi t)
hs : ¬s = Set.univ
i : ι
x✝ : i ∈ Set.univ
hi : i ∈ s
⊢ x i ∈ (convexHull 𝕜) (t i)

pp: case neg
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)},
    (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → s = Set.univ → x ∈ (convexHull 𝕜) (s.pi t)
hs : ¬s = Set.univ
i : ι
x✝ : i ∈ Set.univ
hi : i ∉ s
⊢ x i ∈ (convexHull 𝕜) Set.univ

Tactic:
· exact h i hi

Goal state after:
case neg
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)},
    (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → s = Set.univ → x ∈ (convexHull 𝕜) (s.pi t)
hs : ¬s = Set.univ
i : ι
x✝ : i ∈ Set.univ
hi : i ∉ s
⊢ x i ∈ (convexHull 𝕜) Set.univ
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ p.moduleFilterBasis.filter = ⨅ i, comap (⇑(p i)) (𝓝 0)

Tactic:
refine le_antisymm (le_iInf fun i => ?_) ?_
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]
    intro ε hε
    refine ⟨(p i).ball 0 ε, ?_, ?_⟩
    · rw [← (Finset.sup_singleton : _ = p i)]
      exact p.basisSets_mem {i} hε
    · rw [id, (p i).ball_zero_eq_preimage_ball]
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
    rintro U (hU : U ∈ p.basisSets)
    rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
    rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
    exact fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

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

Goal state before:
pp: case mp
𝕜 : 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
h : ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p
⊢ p ∈ s.closedInterior

Tactic:
obtain ⟨u, w, hw, hw1, rfl⟩ := h
    have hw' : ∀ i ∈ u, w i ≤ 1 := by
      intro i hi
      rw [← hw1]
      apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi
    have hw1' : ∑ i, (u : Set (Fin (n + 1))).indicator w i = 1 := by
      simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1
    rw [Finset.affineCombination_indicator_subset _ _ u.subset_univ,
      affineCombination_mem_closedInterior_iff hw1']
    intro i
    by_cases hi : i ∈ (u : Set (Fin (n + 1))) <;> aesop

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:
UniformConvergenceCLM.instTopologicalSpace,

Goal state after:
𝕜₁ : 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)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : 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
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
by_cases! hI : I.Nonempty

Goal state after:
case pos
𝕜 : 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
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : I.Nonempty
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

case neg
𝕜 : 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
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : I = ∅
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
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
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
⊢ IsVonNBounded R S ↔ ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)

Tactic:
refine ⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩
  simp_rw [isVonNBounded_iff_absorbing_le, nhds_zero_eq, le_iInf_iff, le_principal_iff]
  intro s hs U hU
  rw [Filter.mem_absorbing, Absorbs]
  filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf
  rw [mem_smul_set_iff_inv_smul_mem₀ hc₀]
  intro x hx
  simpa only [mem_smul_set_iff_inv_smul_mem₀ hc₀] using! hc (mem_image2_of_mem hf hx)

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

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕝
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
E : Type u_11
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕝 E
inst✝ : TopologicalSpace F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : Seminorm.IsBounded (fun x ↦ normSeminorm 𝕝 E) q f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ⇑f

Tactic:
exact continuous_of_isBounded (norm_withSeminorms 𝕝 E) hq f hf

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
hM : ∀ (x : E), ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
h'M : ↑M < ∞
x : E
⊢ ‖f x‖ ≤ ↑M * ‖x‖

Tactic:
specialize hM x

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
M : ℝ≥0
h'M : ↑M < ∞
x : E
hM : ‖f x‖ₑ ≤ ↑M * ‖x‖ₑ
⊢ ‖f x‖ ≤ ↑M * ‖x‖
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c

Tactic:
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ c, ↑g = ↑f * c
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup Eₗ
inst✝¹⁷ : SeminormedAddCommGroup F
inst✝¹⁶ : SeminormedAddCommGroup Fₗ
inst✝¹⁵ : SeminormedAddCommGroup G
inst✝¹⁴ : SeminormedAddCommGroup Gₗ
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : NontriviallyNormedField 𝕜₃
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace 𝕜 Eₗ
inst✝⁸ : NormedSpace 𝕜₂ F
inst✝⁷ : NormedSpace 𝕜 Fₗ
inst✝⁶ : NormedSpace 𝕜₃ G
inst✝⁵ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : FunLike 𝓕 E F
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃
inst✝ : RingHomIsometric σ₁₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
⊢ ‖((LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp ⋯ ⋯ ⋯ ⋯) f) g‖ ≤ 1 * ‖f‖ * ‖g‖

Tactic:
simpa only [one_mul] using! opNorm_comp_le f g

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
have hg_mk_co : IsCoboundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsCoboundedUnder, ← map_congr hg.ae_eq_mk]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #⋯.toFinset = #hsf.toFinset
⊢ s ∩ t = s

Tactic:
← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #⋯.toFinset = #hsf.toFinset
⊢ ⋯.toFinset = hsf.toFinset