mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mpr
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
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ w i0 = 0

Tactic:
have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]

Goal state after:
case mpr
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
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
⊢ w i0 = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: case refine_3
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
p : ↥E
v : ↥E.direction
⊢ φ (↑v +ᵥ ↑p) = ↑((φ.linear.restrict ⋯) v) +ᵥ φ ↑p

Tactic:
apply AffineMap.map_vadd

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).coord i = (b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm

Tactic:
ext p

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ ((v +ᵥ b).coord i) p = ((b.coord i).comp ↑(AffineEquiv.constVAdd k P v).symm) 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 : AffineIndependent k p
⊢ AffineIndependent k fun x ↦ ↑x

Tactic:
by
  let f : Set.range p → ι := fun x => x.property.choose
  have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
  let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
  convert! ha.comp_embedding fe
  ext
  simp [fe, hf]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x, (a • f x + b • g x) = 1

Tactic:
Finset.sum_add_distrib,

Goal state after:
case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x, a • f x + ∑ x, b • g x = 1
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ Simplex.setInterior I (s.reindex e) = Simplex.setInterior I s

Tactic:
ext p

Goal state after:
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
⊢ p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
w : ι → R
z : ι → E
⊢ ∅.centerMass w z = 0

Tactic:
simp only [centerMass, sum_empty, smul_zero]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
⊢ Simplex.setInterior I (s.map f hf) = ⇑f '' Simplex.setInterior I s

Tactic:
ext p

Goal state after:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ p ∈ ⇑f '' Simplex.setInterior I s
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
ι : Type u_5
inst✝⁹ : Field R
inst✝⁸ : Field R'
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module R E
t : Finset ι
w : ι → R
z : ι → E
c : R'
inst✝⁵ : Module R' R
inst✝⁴ : Module R' E
inst✝³ : SMulCommClass R' R R
inst✝² : IsScalarTower R' R R
inst✝¹ : SMulCommClass R R' E
inst✝ : IsScalarTower R' R E
hc : c ≠ 0
⊢ t.centerMass (c • w) z = t.centerMass w z

Tactic:
simp [centerMass, -smul_assoc, smul_assoc c, ← smul_sum, smul_inv₀, smul_smul_smul_comm, hc]

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
s : Simplex k P 0
⊢ s.interior = ∅

Tactic:
ext p

Goal state after:
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
s : Simplex k P 0
p : P
⊢ p ∈ s.interior ↔ p ∈ ∅
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
inst✝ : ZeroLEOneClass k
s : Simplex k P 0
⊢ s.closedInterior = {s.points 0}

Tactic:
ext p

Goal state after:
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
inst✝ : ZeroLEOneClass k
s : Simplex k P 0
p : P
⊢ p ∈ s.closedInterior ↔ p ∈ {s.points 0}
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ IsClosed[inst✝¹] (pathComponent x)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst✝¹] s
h' : (s ∩ Iio a).Nonempty
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a

Tactic:
by
  obtain ⟨b, hbs, hba⟩ := h'
  refine nhdsWithin_inter_of_mem (mem_nhdsLT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)
  exact hs.Ioo_subset_of_mem_closure (subset_closure hbs) has

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
⊢ AffineIndependent k p

Tactic:
classical
    intro s w hw hs
    let s' : Finset { y // y ≠ i } := s.subtype (· ≠ i)
    let p' : { y // y ≠ i } → P := fun x => p x
    by_cases his : i ∈ s ∧ w i ≠ 0
    · refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'
    · rw [not_and_or, Classical.not_not] at his
      let w' : { y // y ≠ i } → k := fun x => w x
      have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      intro j hj
      by_cases hji : j = i
      · rw [hji] at hj
        exact hji.symm ▸ his.neg_resolve_left hj
      · exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : LocallyPathConnectedSpace X
x : X
⊢ IsOpen[inst✝²] (ZerothHomotopy.mk ⁻¹' {ZerothHomotopy.mk x})

Tactic:
grind [ZerothHomotopy.preimage_singleton_eq_pathComponent, IsOpen.pathComponent]

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 : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ (convexHull R) s

Tactic:
exact t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : 0 < ∑ i ∈ t, w i
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Tactic:
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 } := fun i hi =>
    ⟨hmem i hi, le_rfl⟩
  convert! (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2 <;>
    simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]

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

Goal state before:
pp: 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
s : Set E
x : E
inst✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i, w i • z i = x
⊢ x ∈ (convexHull R) s

Tactic:
rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]
  exact centerMass_mem_convexHull _ (by simpa using hw₀) (by simp [hw₁]) (by simpa using hz)

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

Tactic:
← convexHull_neg

Goal state after:
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 V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

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
⊢ (convexHull 𝕜) (range s.points) = s.closedInterior

Tactic:
ext p

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 ∈ (convexHull 𝕜) (range s.points) ↔ p ∈ s.closedInterior
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1.refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ id ((p i).ball 0 ε) ⊆ ⇑(p i) ⁻¹' Metric.ball 0 ε

Tactic:
rw [id, (p i).ball_zero_eq_preimage_ball]

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 σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
by
  refine opNorm_le_bound' f hC fun x hx => ?_
  have H₁ : ‖algebraMap _ 𝕜 ‖x‖⁻¹ • x‖ = 1 := by simp [norm_smul, inv_mul_cancel₀ hx]
  have H₂ : ‖x‖⁻¹ * ‖f x‖ ≤ C := by simpa [norm_smul] using hf _ H₁
  rwa [← div_eq_inv_mul, div_le_iff₀] at H₂
  exact (norm_nonneg x).lt_of_ne' hx

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
i : ι
⊢ comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = comap (⇑(q.comp f i)) (𝓝 0)

Tactic:
exact Filter.comap_comap

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (𝓤 C(α, β)).HasBasis (fun p ↦ IsCompact p.1 ∧ pi p.2) fun p ↦ {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}

Tactic:
← isUniformEmbedding_toUniformOnFunIsCompact.comap_uniformity

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ (Filter.comap (fun x ↦ (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
        (𝓤 (α →ᵤ[{K | IsCompact K}] β))).HasBasis
    (fun p ↦ IsCompact p.1 ∧ pi p.2) fun p ↦ {fg | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2}
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inl
ι : Type u_1
u : ι → ℝ≥0
⊢ limsup (fun i ↦ ↑(u i)) ⊥ = ↑(limsup u ⊥)

Tactic:
simp [limsup, limsSup]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : (fun x ↦ a * u x) =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
simp only [limsup_congr hu, limsup_congr hau, Pi.zero_def, ← ENNReal.bot_eq_zero,
      limsup_const_bot]

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : (fun x ↦ a * u x) =ᶠ[f] 0
⊢ ⊥ = a * ⊥
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ IsCountablySpanning (univ.pi '' univ.pi C)

Tactic:
choose s h1s h2s using hC

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
⊢ IsCountablySpanning (univ.pi '' univ.pi C)
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

Tactic:
let f' : s :=
    ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
b : 𝕜 := v y
f' : ↥s := ((b - a) * (f x - f y)⁻¹) • ((algebraMap 𝕜 ↥s) (f x) - ⟨f, hf⟩) + (algebraMap 𝕜 ↥s) a
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inl
α : Type u_1
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ fun a ↦ (u a).toReal
⊢ (limsup u ⊥).toReal = limsup (fun a ↦ (u a).toReal) ⊥

Tactic:
simp [limsup, limsSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ comp id ⋯ f = f

Tactic:
by
  rcases f; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : γ → δ
g' : β → γ
hg : Continuous[inst✝, inst✝²] g
hg' : Continuous[inst✝¹, inst✝] g'
f : α →ₘ[μ] β
⊢ comp g hg (comp g' hg' f) = comp (g ∘ g') ⋯ f

Tactic:
by
  rcases f; rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
c : C(α, R)
f g : C(α, M)
⊢ c • (f + g) = c • f + c • g

Tactic:
ext x; exact smul_add (c x) (f x) (g x)

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst✝¹, inst✝²] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
⊢ (comp g hg f).compQuasiMeasurePreserving φ hφ = comp g hg (f.compQuasiMeasurePreserving φ hφ)

Tactic:
by
  rcases f; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ConditionallyCompleteLattice β
f : α → β
inst✝ : Nonempty α
hμ : ∀ (a : α), μ {a} ≠ 0
hf : BddAbove (range f)
⊢ limsup f ⊤ = ⨆ a, f a

Tactic:
limsup_top_eq_ciSup hf

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ConditionallyCompleteLattice β
f : α → β
inst✝ : Nonempty α
hμ : ∀ (a : α), μ {a} ≠ 0
hf : BddAbove (range f)
⊢ ⨆ i, f i = ⨆ a, f a
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ (uniformOn s) t + (uniformOn s) tᶜ = 1

Tactic:
← uniformOn_union hs disjoint_compl_right,

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ (uniformOn s) (t ∪ tᶜ) = 1
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
s : Finset ι
f : ι → α →ₘ[μ] γ
⊢ ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)

Tactic:
induction s using Finset.induction with
  | empty => simp [coeFn_one]
  | insert a s ha ih =>
    simp only [ha, not_false_eq_true, Finset.prod_insert]
    grw [coeFn_mul, ih]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * q⁻¹ = 1

Tactic:
mul_inv_cancel₀ (ne_of_lt hq_pos).symm

Goal state after:
case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ 1 = 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) * p < log (1 + p * s)

pp: case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
· rw [← lt_div_iff₀ hp1, ← div_lt_div_right_of_neg hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · gcongr
      exact lt_mul_of_lt_one_left hs' hp2

Goal state after:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) * p < log (1 + p * s)