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

Tactic:
rw [← affineIndependent_equiv (Equiv.swap 0 1)]
  convert! h using 1
  ext x
  fin_cases x <;> rfl

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 ((normSeminorm 𝕜 E).ball 0 r)

Tactic:
exact (normSeminorm 𝕜 _).absorbent_ball_zero hr

Goal state after:
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
a : E
⊢ Path.segment a a = refl a

Tactic:
ext; simp

Goal state after:
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
a b : E
⊢ (Path.segment a b).symm = Path.segment b a

Tactic:
ext; simp

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ⇑(lineMap x y) '' Subtype.val '' Ioc 0 1 = Ioc x y

Tactic:
simp only [lineMap_apply, vsub_eq_sub, smul_eq_mul, vadd_eq_add, image_subtype_val_Ioc,
    Icc.coe_zero, Icc.coe_one]

Goal state after:
x y : ℝ
h : x < y
⊢ (fun a ↦ a * (y - x) + x) '' Ioc 0 1 = Ioc x y
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝² : Ring 𝕜
inst✝¹ : PartialOrder 𝕜
inst✝ : IsOrderedRing 𝕜
f : ↑(stdSimplex 𝕜 (Fin 2))
⊢ ↑((fun x ↦ ⟨![1 - ↑x, ↑x], ⋯⟩) ((fun f ↦ ⟨↑f 1, ⋯⟩) f)) 0 = ↑f 0 ∧
    ↑((fun x ↦ ⟨![1 - ↑x, ↑x], ⋯⟩) ((fun f ↦ ⟨↑f 1, ⋯⟩) f)) 1 = ↑f 1

Tactic:
simp [← (show f.1 0 + f.1 1 = 1 by simpa using f.2.2)]

Goal state after:
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
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : ∃ i_1, i_1 ∈ s ∩ {i}
⊢ i ∈ s

Tactic:
rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i j : ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
hne : i ≠ j
⊢ (w i + w j)⁻¹ • (w i • z i + w j • z j) = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
module

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

Goal state before:
pp: case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

Tactic:
intro e

Goal state after:
case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t) ((homothety x t⁻¹) e) = e
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.RightInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

Tactic:
intro e

Goal state after:
case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
e : P
⊢ (homothety x t⁻¹) ((homothety x t) e) = e
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hus : u ⊆ s
hu : IsOpen[inst✝¹] u
hxu : x ∈ u
⊢ ∃ i, (IsOpen[inst✝¹] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨pathComponentIn u x, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
    isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ ∑ x ∈ s with x ≠ i, w x = 0

Tactic:
Finset.sum_filter_of_ne,

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
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ ∑ x ∈ s, w x = 0

k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x ↦ w ↑x
⊢ ∀ x ∈ s, w x ≠ 0 → x ≠ i
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x) = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x))

Tactic:
by abel_nf

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝ : j ∈ Finset.univ
⊢ ∀ x ∈ {i}ᶜ, ∑ j ∈ if hk : x = i then ⋯ ▸ {j} else Finset.univ, w x j = 1

Tactic:
simp +contextual [hw₁]

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

Goal state before:
pp: case h₀
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝ : j ∈ Finset.univ
⊢ ∀ b ∈ if hk : i = i then ⋯ ▸ {j} else Finset.univ, b ≠ j → w i b = 0

Tactic:
simp +contextual [hw₁]

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

Goal state before:
pp: case h₁
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝ : j ∈ Finset.univ
⊢ (j ∉ if hk : i = i then ⋯ ▸ {j} else Finset.univ) → w i j = 0

Tactic:
simp +contextual [hw₁]

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : 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
H : ∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
⊢ IsBounded p q f

Tactic:
rw [IsBounded]
  peel H with i s H
  obtain ⟨C, hC⟩ := H
  refine ⟨C.toNNReal, fun x ↦ show q i (f x) ≤ C.toNNReal • ((s.sup p) x) from ?_⟩
  exact (hC x).trans <| mul_le_mul_of_nonneg_right C.le_coe_toNNReal (apply_nonneg _ _)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜₂ : Type u_3
𝕜₃ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : NormedField 𝕜₃
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module 𝕜₃ 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
σ₂₃ : 𝕜₂ →+* 𝕜₃
f : E →L[𝕜₃] F →SL[σ₂₃] G
c : 𝕜₃
x : E
y : F
⊢ (f (c • x)) y = c • (f x) y

Tactic:
rw [f.map_smul, smul_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
← isUniformEmbedding_toUniformOnFun.of_comp_iff

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding ((fun f ↦ (UniformOnFun.ofFun {s | IsVonNBounded 𝕜' s}) ⇑f) ∘ restrictScalars 𝕜')
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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗ[σ₁₂] F
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x : E
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
by
    gcongr; apply le_max_left

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝¹ x✝ : G →L[𝕜] G
⊢ (↑↑(e.arrowCongr e)).toFun (x✝¹ * x✝) = (↑↑(e.arrowCongr e)).toFun x✝¹ * (↑↑(e.arrowCongr e)).toFun x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝ : 𝕜
⊢ (↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝) = (algebraMap 𝕜 (H →L[𝕜] H)) x✝

Tactic:
ext; simp

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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
⊢ f.bilinearComp 0 gF = 0

Tactic:
ext; simp

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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
⊢ f.bilinearComp gE 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ sSup {a | ∀ᶠ (n : ℝ) in f, a ≤ n} = 0

Tactic:
sSup_of_not_bddAbove

Goal state after:
f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ 0 = 0

f : Filter ℝ
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ ¬BddAbove {a | ∀ᶠ (n : ℝ) in f, a ≤ n}
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: f : Filter ℝ≥0
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ sSup {a | ∀ᶠ (n : ℝ≥0) in f, a ≤ n} = 0

Tactic:
sSup_of_not_bddAbove

Goal state after:
f : Filter ℝ≥0
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ 0 = 0

f : Filter ℝ≥0
hf : ¬IsCobounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ ¬BddAbove {a | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : ℝ
⊢ c ≤ liminf (fun i ↦ ↑(u i)) f ↔ c ≤ ↑(liminf u f)

Tactic:
rw [← Real.toNNReal_le_iff_le_coe, le_liminf_iff (by simpa) ⟨0, by simp⟩, le_liminf_iff]

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' ↦ u a' b) f

Tactic:
rw [eventually_countable_forall]
    exact fun b => ENNReal.eventually_le_limsup fun a => u a b

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) = fun x ↦ Classical.choose h

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞ → eLpNorm f p μ < ∞

Tactic:
by
    intro h
    have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top
    have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'
    simpa [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top] using
      ENNReal.rpow_lt_top_of_nonneg (le_of_lt this) (ne_of_lt h)

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
· rw [h_top]
    exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConcaveOn 𝕜 s f

Tactic:
← neg_strictConvexOn_iff

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
⊢ StrictConvexOn 𝕜 s (-f)
Module: Mathlib.Data.Real.ConjExponents

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

Tactic:
by
  simpa [← NNReal.holderTriple_coe_iff, h.nonneg, h.symm.nonneg, h.nonneg']

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.LpAddConst = 1

Tactic:
LpAddConst,

Goal state after:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1) = 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ⊢ LpAddConst 0 = 1

Tactic:
LpAddConst,

Goal state after:
⊢ (if 0 ∈ Set.Ioo 0 1 then 2 ^ (1 / ENNReal.toReal 0 - 1) else 1) = 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1
⊢ (ENNReal.ofReal p)⁻¹.LpAddConst = 2 ^ (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)

Tactic:
LpAddConst,

Goal state after:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1
⊢ (if (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo 0 1 then 2 ^ (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) else 1) =
    2 ^ (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
by
  have :
    Tendsto (fun η : ℝ≥0∞ => LpAddConst p * (η + η)) (𝓝[>] 0)
        (𝓝 (LpAddConst p * (0 + 0))) :=
    (ENNReal.Tendsto.const_mul (tendsto_id.add tendsto_id)
          (Or.inr (LpAddConst_lt_top p).ne)).mono_left
      nhdsWithin_le_nhds
  simp only [add_zero, mul_zero] at this
  rcases (((tendsto_order.1 this).2 δ hδ.bot_lt).and self_mem_nhdsWithin).exists with ⟨η, hη, ηpos⟩
  refine ⟨η, ηpos, fun f g hf hg Hf Hg => ?_⟩
  calc
    eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) :=
      eLpNorm_add_le' hf hg p
    _ ≤ LpAddConst p * (η + η) := by gcongr
    _ < δ := hη

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ n * (∑ i ∈ s, w i / z i)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
(show n = (n⁻¹)⁻¹ by simp),

Goal state after:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ n⁻¹⁻¹ * (∑ i ∈ s, w i / z i)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹