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

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
hai : LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
⊢ LinearIndependent k fun i_1 ↦ f (p ↑i_1) -ᵥ f (p i)

Tactic:
←
    f.linearMap_vsub

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
hai : LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
⊢ LinearIndependent k fun i_1 ↦ f.linear (p ↑i_1 -ᵥ p 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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
hn : ∃ a b, affineSpan k (p '' a) = affineSpan k (p '' b) ∧ a ≠ b
⊢ False

Tactic:
obtain ⟨s₁, s₂, hs₁₂, hne⟩ := hn

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 ι
hs₁₂ : affineSpan k (p '' s₁) = affineSpan k (p '' s₂)
hne : s₁ ≠ s₂
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case neg.inr
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
i : ι
his₂ : i ∈ s₂
his₁ : i ∉ s₁
⊢ False

Tactic:
· exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm

Goal state after:
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
t : Finset V
h : ¬AffineIndependent k Subtype.val
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
rw [affineIndependent_iff_of_fintype] at h

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
h : ¬∀ (w : ↥t → k), ∑ i, w i = 0 → (univ.weightedVSub Subtype.val) w = 0 → ∀ (i : ↥t), w i = 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: r ε : ℝ
hε : 0 < ε
⊢ Ioo (r - ε) (r + ε) = openSegment ℝ (r - ε) (r + ε)

Tactic:
openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)

Goal state after:
r ε : ℝ
hε : 0 < ε
⊢ Ioo (r - ε) (r + ε) = Ioo (r - ε) (r + ε)
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
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
by_cases h_cases : x = y

Goal state after:
case pos
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • x + b • y ∈ s

case neg
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
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y ∈ s
Module: Mathlib.Topology.Connected.LocallyPathConnected

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

Tactic:
rw [← pathComponentIn_univ]
  exact isOpen_univ.pathComponentIn _

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₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑default -ᵥ ![p₁, p₂] 0 ≠ 0

Tactic:
rw [he' default]

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₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑i₁ -ᵥ ![p₁, p₂] 0 ≠ 0
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case refine_1
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 : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk x.fst '' pathComponentIn (mk x.fst ⁻¹' u) x.snd ⊆ pathComponentIn u x

Tactic:
apply IsPathConnected.subset_pathComponentIn
    · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_sigmaMk
    · exact ⟨x.2, mem_pathComponentIn_self hxu, rfl⟩
    · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

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

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
hU : ∃ «I», «I».Finite ∧ ∃ t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ «I».pi t ⊆ U
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U

Tactic:
obtain ⟨J, hJ, t, ht, htU⟩ := hU

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ U
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₃] ∘ ⇑(Equiv.swap 1 2))

Tactic:
convert! affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₁p₃ hp₁ hp₃ hp₂ using 1

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
⊢ ![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2) = ![p₁, p₃, p₂]
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
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
x : E
⊢ x ∈ (convexHull R) s → ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i, w i • z i = x

Tactic:
simp only [convexHull_eq, mem_ofPred_eq]
    rintro ⟨ι, t, w, z, h⟩
    refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩
    simpa [← sum_attach t, centerMass_eq_of_sum_1 _ _ h.2.1] using h

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

Goal state before:
pp: case insert
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst✝, _] ⇑(p i)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
a✝ : a ∉ s
hs : Continuous[inst✝, _] ⇑(s.sup p)
⊢ Continuous[inst✝, _] ⇑((insert a s).sup p)

Tactic:
simp only [Finset.sup_insert, coe_sup]

Goal state after:
case insert
𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst✝, _] ⇑(p i)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
a✝ : a ∉ s
hs : Continuous[inst✝, _] ⇑(s.sup p)
⊢ Continuous[inst✝, _] (⇑(p a) ⊔ ⇑(s.sup p))
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ (pullback f) (∑ i ∈ s', q i) ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
map_sum,

Goal state after:
case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (pullback f) (q x) ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
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
⊢ ContinuousSMul 𝕜₂ (E →SLᵤ[σ, 𝔖] F)

Tactic:
let : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
  have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  let φ : (E →SLᵤ[σ, 𝔖] F) →ₗ[𝕜₂] E → F :=
    ⟨⟨DFunLike.coe, fun _ _ => rfl⟩, fun _ _ => rfl⟩
  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.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
⊢ sphere x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
  grw [← (closedBall_subset_range_iff_surjective x hr), ← convexHull_sphere_eq_closedBall x hr.le,
    convexHull_mono h, (convexHull_eq_self (𝕜 := ℝ) (s := Set.range ↑f)).mpr]
  exact Submodule.Convex.semilinear_range (E := F') (F' := E) (σ := τ) f

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
j : Fin 1
⊢ j ∈ w ↔ j ∈ Finset.univ

Tactic:
simp only [Subsingleton.elim j i, hi, Finset.mem_univ]

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

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

Tactic:
by
  rcases eq_top_or_lt_top M with rfl | h'M
  · simp
  lift M to NNReal using h'M.ne
  simp only [← ofReal_norm, ENNReal.ofReal_le_coe]
  apply opNorm_le_bound _ (by positivity) (fun x ↦ ?_)
  specialize hM x
  simp only [← ofReal_norm, ← ENNReal.ofReal_coe_nnreal] at hM
  rwa [← ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_le_ofReal_iff (by positivity)] at hM

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖f y‖₊
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
← inv_inv ‖f y‖₊,

Goal state after:
𝕜 : 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 σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖f y‖₊⁻¹⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
this : r < ‖x‖₊⁻¹ * ‖f x‖₊
⊢ ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖₊ = 1 ∧ r < ‖f ((algebraMap ℝ 𝕜) ‖x‖⁻¹ • x)‖₊

Tactic:
simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this

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

Goal state before:
pp: 𝕜 : 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ₗ
⊢ ‖smulRight c f‖ = ‖c‖ * ‖f‖

Tactic:
by
  refine le_antisymm ?_ ?_
  · refine opNorm_le_bound _ (by positivity) fun x => ?_
    calc
      ‖c x • f‖ = ‖c x‖ * ‖f‖ := norm_smul _ _
      _ ≤ ‖c‖ * ‖x‖ * ‖f‖ := by gcongr; apply le_opNorm
      _ = ‖c‖ * ‖f‖ * ‖x‖ := by ring
  · obtain hf | hf := (norm_nonneg f).eq_or_lt'
    · simp [hf]
    · rw [← le_div_iff₀ hf]
      refine opNorm_le_bound _ (by positivity) fun x => ?_
      rw [div_mul_eq_mul_div, le_div_iff₀ hf]
      calc
        ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
        _ = ‖smulRight c f x‖ := rfl
        _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
⊢ l ≤ 𝓟 {g | EqOn (⇑g) f s} → ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x

Tactic:
hlf

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
· have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ := by
      rw [EventuallyEq, not_eventually] at hu
      exact hu.mono fun x hx => by simpa
    have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
      eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
    have hfu : f.limsup u ≠ 0 := mt limsup_eq_bot.1 hu
    simp [ha_top, top_mul', h_top_le, hfu]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ Measure.count[↑t | ↑s] = ↑(#(s ∩ t)) / ↑(#s)

Tactic:
cond_apply hs,

Goal state after:
Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (Measure.count ↑s)⁻¹ * Measure.count (↑s ∩ ↑t) = ↑(#(s ∩ t)) / ↑(#s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
μ : Measure α
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ ↑p ≠ 0

Tactic:
by exact_mod_cast hp

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Tactic:
eLpNorm'_eq_lintegral_enorm,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst✝ : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = ((∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)) ^ q
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
μ : Measure α
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ ↑?m.32 ≠ 0

Tactic:
by exact_mod_cast hp

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure

Tactic:
clear hs s

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
⊢ (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i ↦ (μ i).toOuterMeasure
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
eLpNorm'_eq_lintegral_enorm,

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ (∫⁻ (a : α), ‖c‖ₑ ^ q ∂μ) ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
eLpNorm'_eq_lintegral_enorm,

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ (∫⁻ (a : α), ‖c‖ₑ ^ q ∂μ) ^ (1 / q) = ‖c‖ₑ * μ Set.univ ^ (1 / q)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
hp_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
by rw [hp_cancel, ENNReal.rpow_one]

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

Goal state before:
pp: case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
ENNReal.mul_lt_top_iff

Goal state after:
case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ < ∞ ∧ μ Set.univ ^ (1 / p.toReal) < ∞ ∨ ‖c‖ₑ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Goal state after:
case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + p * -1 < (1 + -1) ^ p

case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
⊢ 1 + p * s < (1 + s) ^ p
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p < 1 + p * s

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Goal state after:
case inl
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ (1 + -1) ^ p < 1 + p * -1

case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
⊢ (1 + s) ^ p < 1 + p * s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ
h : p.HolderTriple q r
⊢ r < p

Tactic:
simpa using inv_strictAnti₀ h.inv_pos h.inv_lt_inv

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
hp : 1 < p
⊢ 1 < ↑p

Tactic:
by exact_mod_cast hp

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 - x ^ p / y ^ p < p * y ^ (p - 1) * (y - x) / y ^ p

Tactic:
← div_rpow hx hy.le,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 - (x / y) ^ p < p * y ^ (p - 1) * (y - x) / y ^ p