mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
⊢ vectorSpan k (p '' s₁) ≠ vectorSpan k (p '' s₂)

Tactic:
intro he

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) → s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
intro h

Goal state after:
case mp
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case pos
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩

Goal state after:
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton → vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)

Tactic:
intro h

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s.attach, w ↑x = 0
hw₁ : ∑ x ∈ s.attach, w ↑x • ↑x = 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
exact fun x hx ↦ hp.eq_zero_of_sum_eq_zero hw₀ hw₁ ⟨x, hx⟩ (mem_univ _)

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (s.weightedVSub p) w ∈ vectorSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂} ↔
    ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
rw [mem_vectorSpan_pair]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w) ↔
    ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
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 : (affineCombination k univ s.points) w ∈ s.closedInterior
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
⊢ (affineCombination k univ s.points) w ∉ s.interior →
    (affineCombination k univ s.points) w ∈ ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
intro h

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 : (affineCombination k univ s.points) w ∈ s.closedInterior
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : (affineCombination k univ s.points) w ∉ s.interior
⊢ (affineCombination k univ s.points) w ∈ ⋃ i, (s.faceOpposite i).closedInterior
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab

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

Goal state before:
pp: case inr
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 : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
rw [← linearIndependent_subtype_iff,
      linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi

Goal state after:
case inr
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 : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
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
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ (∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s) →
    Convex R s

Tactic:
intro h

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
⊢ Convex R s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_1.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
h : LocallyPathConnectedSpace ((i : ι) → Z i)
x : (i : ι) → Z i
this : ∀ (i : ι), Nonempty (Z i)
⊢ {i | ¬PathConnectedSpace (Z i)}.Finite

Tactic:
have hVn : pathComponent x ∈ 𝓝 x :=
      (IsOpen.pathComponent x).mem_nhds (mem_pathComponent_self x)

Goal state after:
case refine_1.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
h : LocallyPathConnectedSpace ((i : ι) → Z i)
x : (i : ι) → Z i
this : ∀ (i : ι), Nonempty (Z i)
hVn : pathComponent x ∈ 𝓝 x
⊢ {i | ¬PathConnectedSpace (Z i)}.Finite
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
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
⊢ ![p₁, p₂, p₃] 2 ∉ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})

Tactic:
intro h

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
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ False
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_eq_iInter_thickening hδ]
    exact convex_iInter₂ fun _ _ => hs.thickening _

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 : Set E
hU' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left✝ : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r

Tactic:
exact ⟨U, hU', Eq.subset hU⟩

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

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_4
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ f z ≤ max (f x) (f y)

Tactic:
rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz

Goal state after:
𝕜 : Type u_1
β : Type u_4
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)
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
⊢ (∃ 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:
intro h

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

Tactic:
intro h

Goal state after:
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
p : V
h : p ∈ s.closedInterior
⊢ ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mp
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_11
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded (fun x ↦ p) q f → ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p

Tactic:
intro h

Goal state after:
case mp
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_11
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : IsBounded (fun x ↦ p) q f
⊢ ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_11
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ (∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p) → IsBounded (fun x ↦ p) q f

Tactic:
intro h

Goal state after:
case mpr
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_11
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p
⊢ IsBounded (fun x ↦ p) q f
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_11
E : Type u_12
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ 𝓝 0 = comap (⇑(normSeminorm 𝕜 E)) (𝓝 0)

Tactic:
coe_normSeminorm,

Goal state after:
𝕜 : Type u_11
E : Type u_12
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ 𝓝 0 = comap norm (𝓝 0)
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

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

Tactic:
intro h

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

Goal state before:
pp: R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (f x + f x') y = (f x) y + (f x') y

Tactic:
add_apply

Goal state after:
R : Type u_1
𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : Semiring R
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜₃ G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
σ₁₃ : R →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x x' : E
y : F
⊢ (f x) y + (f x') y = (f x) y + (f x') y
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Countable ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
⊢ FirstCountableTopology E

Tactic:
by
  have := hp.topologicalAddGroup
  let _ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  have : (𝓝 (0 : E)).IsCountablyGenerated := by
    rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
    exact Filter.iInf.isCountablyGenerated _
  have : (uniformity E).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
  exact UniformSpace.firstCountableTopology E

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

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U) →
    ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
intro h

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K) →
    ∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
intro h

Goal state after:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
⊢ ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
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:
by
  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.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᵐ[μ] f

Tactic:
by
  rw [← mk_eq_mk (hf := AEEqFun.aestronglyMeasurable ..) (hg := hf), mk_coeFn]

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
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
x : ℝ≥0
hx : some x > ENNReal.ofReal r
⊢ ↑x > r

Tactic:
simpa [ofReal_lt_coe_iff hr] using hx

Goal state after:
Module: Mathlib.Probability.UniformOn

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

Tactic:
have := isProbabilityMeasure_uniformOn hs hs'
  refine eq_of_le_of_not_lt prob_le_one ?_
  rw [not_lt, ← uniformOn_self hs hs']
  exact measure_mono ht

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)

Tactic:
intro h

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s
⊢ ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s) →
    ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)

pp: case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s

Tactic:
· intro h s hs; refine (h _ hs).trans_eq (piPremeasure_pi hs)

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
⊢ (∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)) →
    ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)
⊢ ∀ (s : Set ((i : ι) → α i)), s.Nonempty → n s ≤ piPremeasure m s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
μ : Measure α
f : α → ε
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ 1 ∂μ) ^ 1 = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
ENNReal.rpow_one

Goal state after: