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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this : (a • 1) • x + (b • 1) • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
simpa using this

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • (y - x) ∈ s

Tactic:
by
  rw [add_comm]
  exact h.lineMap_mem hx hy ht

Goal state after:
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
S : AffineSpace V P
p : P
v : V
⊢ v ∈ ⊤.direction ↔ v ∈ ⊤

Tactic:
refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩

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
p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ ⊤.direction
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
S : AffineSpace V P
⊢ ⊥ ≠ ⊤

Tactic:
intro contra

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
contra : ⊥ = ⊤
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Balanced ℝ s
x✝ : E
hx : x✝ ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ ‖a‖ ≤ 1

Tactic:
by rwa [Real.norm_of_nonneg ha₀]

Goal state after:
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
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k (insert 0 s))

Tactic:
refine affineSpan_subset_span.antisymm ?_

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(affineSpan k (insert 0 s))
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ 𝓝[range ⇑σ] σ 0 = 𝓝 0

Tactic:
σ.surjective.range_eq,

Goal state after:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ 𝓝[univ] σ 0 = 𝓝 0
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
p : ι → P
⊢ (affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂ = (s.weightedVSub p) (w₁ - w₂)

Tactic:
rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]

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
p q : Seminorm 𝕜 E
⊢ ∀ (a : 𝕜) (x : E), ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)

Tactic:
by
        intro a x
        obtain rfl | ha := eq_or_ne a 0
        · rw [norm_zero, zero_mul, zero_smul]
          refine
            ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
              (fun i => by positivity)
              fun x hx => ⟨0, by rwa [map_zero, sub_zero, map_zero, add_zero]⟩
        simp_rw [Real.mul_iInf_of_nonneg (norm_nonneg a), mul_add, ← map_smul_eq_mul p, ←
          map_smul_eq_mul q, smul_sub]
        refine
          Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E)
            (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_
        rw [smul_inv_smul₀ ha]

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
V₂ : 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₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
hf : Function.Surjective ⇑f
h : affineSpan k s = ⊤
⊢ affineSpan k (⇑f '' s) = ⊤

Tactic:
by
  rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j j = -1

Tactic:
simp [weightedVSubVSubWeights, h.symm]

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

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : #s = n + 1
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : AffineSubspace k P
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)

Tactic:
refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
  · rintro rfl
    exact bot_parallel_iff_eq_bot.1 h
  · rintro rfl
    exact parallel_bot_iff_eq_bot.1 h
  · rcases h with ⟨hd, hb⟩
    by_cases hs₁ : s₁ = ⊥
    · rw [hs₁, bot_parallel_iff_eq_bot]
      exact hb.1 hs₁
    · have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
      rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
      rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
      refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
      · rw [mem_map]
        refine ⟨p₁, hp₁, ?_⟩
        simp
      · simpa using hd.symm

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ {y | max (p (y - e)) (q (y - e)) ≤ r} = {a | p (a - e) ≤ r ∧ q (a - e) ≤ r}

Tactic:
sup_le_iff

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).ball e r = s.inf' H fun i ↦ (p i).ball e r

Tactic:
induction H using Finset.Nonempty.cons_induction with

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
H : s.Nonempty
e : E
r : ℝ
⊢ (s.sup' H p).closedBall e r = s.inf' H fun i ↦ (p i).closedBall e r

Tactic:
induction H using Finset.Nonempty.cons_induction with

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
p₁ q₁ p₂ q₂ : P
⊢ line[k, p₁, q₁].direction ≤ line[k, p₂, q₂].direction ↔ ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁

Tactic:
by
  rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]

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 : 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‖
⊢ 0 < ‖c ^ (n + 1)‖

Tactic:
rw [norm_zpow]

Goal state after:
𝕜 : 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‖
⊢ 0 < ‖c‖ ^ (n + 1)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case pos
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₂
hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hw : p = (affineCombination k univ (s.map f hf).points) w
⊢ (∀ (i : Fin (n + 1)), w i ∈ I) ↔
    ∃ x ∈ Simplex.setInterior I s, f x = f ((affineCombination k univ s.points) fun i ↦ w i)

Tactic:
hf.eq_iff

Goal state after:
case pos
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₂
hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hw : p = (affineCombination k univ (s.map f hf).points) w
⊢ (∀ (i : Fin (n + 1)), w i ∈ I) ↔ ∃ x ∈ Simplex.setInterior I s, x = (affineCombination k univ s.points) fun i ↦ w i
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)

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

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
| ⋃ i ∈ s ×ˢ t, nhdsKer {i}
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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
have ha : AffineIndependent k fun x : { x : Fin 3 // x ≠ 2 } => ![p₁, p₂, p₃] x := by
    rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]
    convert! affineIndependent_of_ne k hp₁p₂
    ext x
    fin_cases x <;> rfl

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
⊢ AffineIndependent k ![p₁, p₂, p₃]
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_2.inl
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
he : IsEmpty ((i : ι) → Z i)
⊢ LocallyPathConnectedSpace ((i : ι) → Z i)

Tactic:
exact ⟨he.elim⟩

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
⊢ ∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x + ∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i ∈ s, w i • v i + b • ∑ i ∈ s', w' i • v i

Tactic:
rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]

Goal state after:
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
⊢ ∑ x ∈ s, (if x ∈ s then a * w x else 0) • v x + ∑ x ∈ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i ∈ s, w i • v i + b • ∑ i ∈ s', w' i • v i

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
⊢ ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0

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
⊢ ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) • v x = 0
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
⊢ (convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Tactic:
rw [convexHull_range_eq_exists_affineCombination]

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

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

Tactic:
intro h I

Goal state after:
case mp
𝕜 : 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
h : ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s
I : Finset ι
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

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

Tactic:
exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩

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
𝓕 : 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:
← ball_zero_subset_range_iff_surjective hr,

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.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✝⁷ : AddCommGroup G
inst✝⁶ : UniformSpace G
inst✝⁵ : IsUniformAddGroup G
𝕜₃ : Type u_6
inst✝⁴ : NormedField 𝕜₃
inst✝³ : Module 𝕜₃ G
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝² : RingHomCompTriple σ τ ρ
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
g : F →SL[τ] G
hg : IsUniformInducing ⇑g
𝔖 : Set (Set E)
⊢ IsUniformInducing g.comp

Tactic:
rw [← (isUniformInducing_coeFn _ _ _).of_comp_iff]
  exact (UniformOnFun.postcomp_isUniformInducing hg).comp (isUniformInducing_coeFn _ _ _)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : SeminormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖ContinuousLinearMap.id 𝕜 E‖

Tactic:
have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x

Goal state after:
𝕜 : Type u_1
E : Type u_4
inst✝³ : SeminormedAddCommGroup E
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NontrivialTopology E
x : E
hx : ‖x‖ ≠ 0
this : ‖(ContinuousLinearMap.id 𝕜 E) x‖ / ‖x‖ ≤ ‖ContinuousLinearMap.id 𝕜 E‖
⊢ 1 ≤ ‖ContinuousLinearMap.id 𝕜 E‖
Module: Mathlib.Analysis.Normed.Operator.NNNorm

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

Tactic:
· obtain ⟨x, hx, hxf⟩ := f.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm hub
    exact ⟨_, ⟨x, by simpa using! congrArg NNReal.toReal hx, rfl⟩, hxf⟩

Goal state after:
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 : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
⊢ c • 0 = 0

Tactic:
by simp only [← coe_zero, ← coe_smul, smul_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ₑ = ‖f‖ₑ

Tactic:
simp [enorm_eq_nnnorm]

Goal state after:
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 σ₁₂
c : 𝕜₂
f : F →SL[σ₂₃] G
g : E →SL[σ₁₂] F
⊢ f ∘SL (c • g) = σ₂₃ c • f ∘SL g

Tactic:
ext
      simp only [map_smulₛₗ, comp_apply, smul_apply]

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

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : ‖f‖ = 0
⊢ ‖c‖ * ‖f‖ ≤ ‖smulRight c f‖

Tactic:
simp [hf]

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f fun i ↦ ↑(u i)) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨b.toNNReal, by simp, by simpa⟩
  · rintro ⟨b, -, hb⟩
    exact ⟨b, hb⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLinearOrder β
f : α → β
h : ∀ ⦃x : α⦄ ⦃a : β⦄, a < f x → μ {y | a < f y} ≠ 0
⊢ ⨆ x, f x = essSup f μ

Tactic:
by
  apply le_antisymm (iSup_le _) essSup_le_iSup
  intro i
  rw [essSup_eq_sInf]
  apply le_sInf
  intro b hb
  exact not_lt.mp fun a ↦ h a hb

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))

Tactic:
by
  simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
⊢ Measure.pi μ = μν

Tactic:
have h4C : ∀ (i) (s : Set (α i)), s ∈ C i → MeasurableSet s := by
    intro i s hs; rw [← hC]; exact measurableSet_generateFrom hs
  refine
    (FiniteSpanningSetsIn.pi h3C).ext
      (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm (IsPiSystem.pi h2C) ?_
  rintro _ ⟨s, hs, rfl⟩
  rw [mem_univ_pi] at hs
  have := fun i => (h3C i).sigmaFinite
  simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]

Goal state after: