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

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
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂

Tactic:
by
  classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]

Goal state after:
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✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (p '' s')

Tactic:
rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]

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
b : AffineBasis ι k P
i j : ι
h : i ≠ j
⊢ 1 - (b.basisOf i).sumCoords (b ↑⟨j, ⋯⟩ -ᵥ b i) = 0

Tactic:
← b.basisOf_apply,

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i j : ι
h : i ≠ j
⊢ 1 - (b.basisOf i).sumCoords ((b.basisOf i) ⟨j, ⋯⟩) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun j' ↦ if j' = i then x else 1 - x
⊢ s.sum w = 1

Tactic:
simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]

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
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (affineCombination k s p) w₁ = (affineCombination k s p) w₂ ↔ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ s.affineCombination_congr h fun _ _ ↦ rfl⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : (affineCombination k s p) w₁ = (affineCombination k s p) w₂
⊢ ∀ i ∈ s, w₁ i = w₂ i
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent k (p ∘ ⇑f)

Tactic:
intro fs

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
⊢ ∀ (w : ι2 → k), ∑ i ∈ fs, w i = 0 → (fs.weightedVSub (p ∘ ⇑f)) w = 0 → ∀ i ∈ fs, w i = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : 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)‖
⊢ p (c ^ (-(n + 1)) • x) < ε

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)

pp: case refine_4
𝕜 : 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 ^ (-(n + 1))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Tactic:
· show p ((c ^ (-(n + 1))) • x) < ε
    rw [map_smul_eq_mul, zpow_neg, norm_inv, ← div_eq_inv_mul, div_lt_iff₀ cnpos, mul_comm,
        norm_zpow]
    exact (div_lt_iff₀ εpos).1 (hn.2)

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)

case refine_4
𝕜 : 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 ^ (-(n + 1))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * 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 : ℕ
inst✝ : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
⊢ s.points j ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ j ≠ i

Tactic:
faceOpposite,

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 : ℕ
inst✝ : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
⊢ s.points j ∈ affineSpan k (Set.range (s.face ⋯).points) ↔ j ≠ i
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
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ IsPathConnected (↑q)ᶜ

Tactic:
convert (hpc.image continuous_subtype_val).add q.isPathConnected
  trans Submodule.prodEquivOfIsCompl p q hpq '' ({0}ᶜ ×ˢ univ)
  · rw [prod_univ, LinearEquiv.image_eq_preimage_symm]
    ext
    simp
  · ext
    simp [mem_add, and_assoc]

Goal state after:
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
i : Fin (n + 1)
j : Fin (n - 1 + 1)
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))

Tactic:
faceOpposite,

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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
j : Fin (n - 1 + 1)
⊢ (s.face ⋯).points j = s.points (i.succAbove (Fin.cast ⋯ j))
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ Set.range ((s.reindex e).faceOpposite i).points = Set.range (s.faceOpposite (e.symm i)).points

Tactic:
faceOpposite,

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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ Set.range ((s.reindex e).face ⋯).points = Set.range (s.faceOpposite (e.symm i)).points
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
x y : X
h : vertex x = vertex y
⊢ x = y

Tactic:
replace h := DFunLike.congr_fun h x

Goal state after:
S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
inst✝³ : Fintype X
inst✝² : IsOrderedRing S
inst✝¹ : Nontrivial S
inst✝ : DecidableEq X
x y : X
h : (vertex x) x = (vertex y) x
⊢ x = y
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: X : Type u_2
inst✝⁵ : Fintype X
𝕜 : Type u_5
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : Nonempty X
inst✝ : DecidableEq X
x : X
⊢ ↑barycenter x = ((Fintype.card X • 1)⁻¹ • ∑ x, 1 • Pi.single x 1) x

Tactic:
simp [barycenter, Pi.smul_apply, Finset.sum_apply, Pi.single_apply]

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

Goal state before:
pp: case h₁
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
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
⊢ (affineCombination k univ s.points) w ∈ (s.faceOpposite j).closedInterior

Tactic:
faceOpposite,

Goal state after:
case h₁
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
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
⊢ (affineCombination k univ s.points) w ∈ (s.face ⋯).closedInterior
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ nhdsKer {(x, y)} = nhdsKer {x} ×ˢ nhdsKer {y}

Tactic:
by
  simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
a : α
⊢ 𝓟 (nhdsKer {a}) = 𝓝 a

Tactic:
by
  rw [principal_nhdsKer, nhdsSet_singleton]

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
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ AffineIndependent k ![p₁, p₂]

Tactic:
affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0

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
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h
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
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V

Tactic:
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₂]

Goal state after:
case h
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
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂) ⊆ (⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
w : Fin (n + 1) → 𝕜
hw1 : ∑ i, w i = 1
h : ∀ (i : Fin (n + 1)), w i ∈ Icc 0 1
⊢ ∃ s_1 w_1,
    (∀ i ∈ s_1, 0 ≤ w_1 i) ∧
      s_1.sum w_1 = 1 ∧
        (Finset.affineCombination 𝕜 s_1 s.points) w_1 = (Finset.affineCombination 𝕜 Finset.univ s.points) w

Tactic:
exact ⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩

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
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₃ : ∀ S ∈ 𝔖, IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
φ : (E →SLᵤ[σ, 𝔖] F) →ₗ[𝕜₂] E → F := { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContinuousSMul 𝕜₂ (E →SLᵤ[σ, 𝔖] F)

Tactic:
exact UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (E →SLᵤ[σ, 𝔖] F) φ
    ⟨rfl⟩ fun u s hs => (h𝔖₃ s hs).image u

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 : ∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ⇑f

Tactic:
← Seminorm.const_isBounded (Fin 1)

Goal state after:
𝕝 : 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
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
x : E
hx : ‖x‖ ≠ 0
⊢ ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖ = 1

Tactic:
simp [norm_smul, inv_mul_cancel₀ hx]

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

Goal state before:
pp: 𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕜₂
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
𝕜 : Type u_11
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
hp : Continuous[inst✝¹, _] ⇑p
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
hf : IsInducing ⇑f
⊢ ∃ s C, C ≠ 0 ∧ p ≤ (C • s.sup q).comp f

Tactic:
obtain ⟨s, C, hC, hqC⟩ := Seminorm.bound_of_continuous (hf.withSeminorms hq) p hp
  rw [← SeminormFamily.finset_sup_comp, ← Seminorm.smul_comp] at hqC
  exact ⟨s, C, hC, hqC⟩

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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : l.Germ M
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f

Tactic:
simp [add_smul]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ ∀ t ∈ {t₁, t₂}, PolynormableSpace 𝕜 E

Tactic:
by simp [ht₁, ht₂]

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✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : l.Germ R
f✝ : l.Germ M
c₁ c₂ : α → R
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f

Tactic:
simp [add_smul]

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:
by
  simp [← NNReal.coe_inj]

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

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

Tactic:
obtain rfl | hf := f.eq_or_neBot

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

case inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
⊢ liminf (fun x ↦ u x * a) f = a * liminf u f

Tactic:
by
  simpa [mul_comm] using liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

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

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

Tactic:
obtain rfl | hf := f.eq_or_neBot

Goal state after:
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) ⊥

case inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
⊢ (limsup u f).toReal = limsup (fun a ↦ (u a).toReal) f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace δ
inst✝ : MeasurableSpace β
ν : Measure β
γ : Type u_5
mγ : MeasurableSpace γ
ξ : Measure γ
g : γ →ₘ[ξ] δ
f : β → γ
hf : QuasiMeasurePreserving f ν ξ
f' : α → β
hf' : QuasiMeasurePreserving f' μ ν
⊢ g.compQuasiMeasurePreserving (f ∘ f') ⋯ = (g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf'

Tactic:
by
  ext
  grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
    coeFn_compQuasiMeasurePreserving, comp_assoc]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → α → ℝ≥0∞
⊢ limsup (fun x ↦ liminf (fun n ↦ f n x) atTop) (ae μ) ≤ liminf (fun n ↦ limsup (fun x ↦ f n x) (ae μ)) atTop

Tactic:
exact ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a

Goal state after:
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:
classical
  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.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ (Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)

Tactic:
classical simp [← Set.univ_pi_ite, pi_pi, apply_ite]

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

Goal state before:
pp: case h₁
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
exact mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const _) ε

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ ‖c‖ₑ * μ s ^ (1 / p.toReal) ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
← ofReal_norm,

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖
⊢ ENNReal.ofReal ‖c‖ * μ s ^ (1 / p.toReal) ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hp0_lt : 0 < q
⊢ eLpNorm' 0 q μ = 0

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hp0_lt]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
by
  simp_rw [le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg (norm_nonneg _) hc (norm_nonneg _),
    norm_eq_zero, eventually_and] at h
  change f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0 at h
  simp [eLpNorm_congr_ae h.1, eLpNorm_congr_ae h.2]

Goal state after: