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

Goal state before:
pp: case refine_1
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x

pp: case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x, (a • f + b • g) x = 1

Tactic:
· apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]

Goal state after:
case refine_2
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x, (a • f + b • g) x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
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, w j = 0

Tactic:
by
      obtain ⟨i, hi | hi⟩ := h
      · exact ⟨i, le_antisymm hi (hp i).1⟩
      · have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1
        exact ⟨i + 1, hw1 _ (by simp)⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : IsOpen[inst✝¹] F
x y : X
hy : y ∈ pathComponentIn F x
s : Set X
hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F
⊢ pathComponentIn F x ∈ 𝓝 y

Tactic:
exact mem_of_superset hs.1.1 <| pathComponentIn_congr hy ▸
    hs.1.2.subset_pathComponentIn (mem_of_mem_nhds hs.1.1) hs.2

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

Goal state before:
pp: case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ ⇑(Equiv.vaddConst p).symm '' insert p (⇑(Equiv.vaddConst p) '' b) = insert 0 b

Tactic:
rw [Set.image_insert_eq, ← Set.image_comp]

Goal state after:
case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm ∘ ⇑(Equiv.vaddConst p) '' b) = insert 0 b
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: 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 : X
h : (𝓝 x).HasBasis (fun s ↦ IsOpen[inst✝²] s ∧ x ∈ s ∧ IsPathConnected s) id
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hu : IsOpen[inst✝²] u
hxu : x ∈ u
hu' : IsPathConnected u
hus : id u ⊆ s
⊢ ∃ i, (IsOpen[inst✝²] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩

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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ (s ∪ s').sum W = 1

Tactic:
rw [sum_add_distrib, ← sum_subset subset_union_left,
        ← sum_subset subset_union_right, sum_ite_of_true,
        sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
        mul_one] <;> intros

Goal state after:
case h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x✝ : ι
a✝ : x✝ ∈ s'
⊢ x✝ ∈ s'

case h
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x✝ : ι
a✝ : x✝ ∈ s
⊢ x✝ ∈ s

R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x✝ : ι
a✝¹ : x✝ ∈ s ∪ s'
a✝ : x✝ ∉ s'
⊢ (if x✝ ∈ s' then b * w' x✝ else 0) = 0

R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x✝ : ι
a✝¹ : x✝ ∈ s ∪ s'
a✝ : x✝ ∉ s
⊢ (if x✝ ∈ s then a * w x✝ else 0) = 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : (p i) x ≠ 0
⊢ 0 ∉ (p i).ball x ((p i) x)

Tactic:
mem_ball,

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : (p i) x ≠ 0
⊢ ¬(p i) (0 - x) < (p i) x
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
⊢ (WithSeminorms fun x ↦ p) ↔ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
by
  /- The nontrivial direction is from right to left. With `SeminormFamily.withSeminorms_of_nhds`,
  we need to see that the neighborhoods of zero for the initial topology and for `p` coincide. -/
  refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
  · apply (h.mem_nhds_iff _ _).2
    exact ⟨Finset.univ, 1, zero_lt_one, by simp⟩
  · apply h.isVonNBounded_iff_seminorm_bounded.2 (fun i ↦ ?_)
    exact ⟨1, zero_lt_one, by simp⟩
  rintro ⟨h, h'⟩
  apply SeminormFamily.withSeminorms_of_nhds
  ext s
  refine ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩
  · /- Show that a neighborhood `s` of zero for the topology is a neighborhood for `p`, by using the
    boundedness of `p.ball 0 1`: this ensures that, for some nonzero `c`, we have
    `p.ball 0 1 ⊆ c • s`, and therefore `p.ball 0 (‖c‖⁻¹) ⊆ s`. -/
    obtain ⟨c, hc, c_ne⟩ : ∃ (c : 𝕜), p.ball 0 1 ⊆ c • s ∧ c ≠ 0 :=
      ((h' hs).and (eventually_ne_cobounded 0)).exists
    have : p.ball 0 (‖c⁻¹‖) ⊆ s := by
      have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
      rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
    grw [← this]
    apply FilterBasis.mem_filter_of_mem
    change p.ball 0 (‖c⁻¹‖) ∈ SeminormFamily.basisSets (fun (i : Fin 1) ↦ p)
    apply SeminormFamily.basisSets_singleton_mem _ 0
    simpa using c_ne
  · /- Show that a neighborhood `s` for `p` is a neighborhood for the topology, by using the
    fact that `p.ball 0 1` is a neighborhood of `0`. Indeed, `s` contains a ball `p.ball 0 r`,
    which contains `c • p.ball 0 1` for some nonzero `c`. The latter set is a neighborhood of zero
    for the topology thanks to the topological vector space assumption. -/
    rcases (FilterBasis.mem_filter_iff _).1 hs with ⟨t, ht, ts⟩
    grw [← ts]
    rcases (SeminormFamily.basisSets_iff _).1 ht with ⟨w, r, r_pos, hw⟩
    rcases eq_or_ne w ∅ with rfl | w_ne
    · simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, ofPred_true] at hw
      simp [hw]
    have : t = p.ball 0 r := by
      have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
      simpa only [this, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
        Finset.sup_singleton] using hw
    rw [this]
    obtain ⟨c, c_pos, hc⟩ : ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < r := exists_norm_lt 𝕜 r_pos
    have c_ne : c ≠ 0 := (by simpa using c_pos)
    have : c • p.ball 0 1 ⊆ p.ball 0 r := by
      rw [smul_ball_zero c_ne]
      exact ball_mono (by simpa using hc.le)
    grw [← this]
    simpa using smul_mem_nhds_smul₀ c_ne h

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

Goal state before:
pp: case h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst✝¹⁴ : SeminormedAddCommGroup E
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜₂
inst✝⁸ : NontriviallyNormedField 𝕜₃
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : y ∈ ⇑ℓ '' s
σ : E
hσ : σ ∈ s ∧ ℓ σ = y
⊢ ‖y‖ ≤ ‖ℓ‖ * M

Tactic:
calc ‖y‖
      _ ≤ ‖ℓ σ‖ := by rw [hσ.2]
      _ ≤ ‖ℓ‖ * ‖σ‖ := ContinuousLinearMap.le_opNorm ℓ σ
      _ ≤ ‖ℓ‖ * M := mul_le_mul (by rfl) (hM σ hσ.1) (norm_nonneg σ) (opNorm_nonneg ℓ)

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
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(α, β)
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 α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
have hcomp : IsCompact s := hK.inter_right <| (isClosed_ball _ hWc).preimage f.continuous

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 α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝³² : SeminormedAddCommGroup E
inst✝³¹ : SeminormedAddCommGroup Eₗ
inst✝³⁰ : SeminormedAddCommGroup F
inst✝²⁹ : SeminormedAddCommGroup Fₗ
inst✝²⁸ : SeminormedAddCommGroup G
inst✝²⁷ : SeminormedAddCommGroup Gₗ
inst✝²⁶ : NontriviallyNormedField 𝕜
inst✝²⁵ : NontriviallyNormedField 𝕜₂
inst✝²⁴ : NontriviallyNormedField 𝕜₃
inst✝²³ : NormedSpace 𝕜 E
inst✝²² : NormedSpace 𝕜 Eₗ
inst✝²¹ : NormedSpace 𝕜₂ F
inst✝²⁰ : NormedSpace 𝕜 Fₗ
inst✝¹⁹ : NormedSpace 𝕜₃ G
inst✝¹⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : FunLike 𝓕 E F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁴ : RingHomInvPair σ₂₁ σ₁₂
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 σ₂₃'
inst✝² : RingHomIsometric σ₁₃
inst✝¹ : RingHomIsometric σ₁'
inst✝ : RingHomIsometric σ₂'
c₁ c₂ : StrongDual 𝕜 E
⊢ smulRightₗ (c₁ + c₂) = smulRightₗ c₁ + smulRightₗ c₂

Tactic:
by
        ext x
        simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]

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
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
g : C(α, β) := { toFun := s.piecewise f ⇑f', continuous_toFun := ⋯ }
⊢ 𝓝 f' = 𝓝 g

Tactic:
rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
hst : μ (s ∩ t) ≠ 0
hs : μ s ≠ 0
⊢ μ[|s][u | t] = μ[u | s ∩ t]

Tactic:
simp [*, hms.inter hmt, cond_apply, ← Set.inter_assoc, ENNReal.mul_inv, ← mul_assoc,
      mul_comm _ (μ s)⁻¹, ENNReal.inv_mul_cancel]

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u

Tactic:
isBoundedDefault

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ (‖c‖ₑ ^ p.toReal * μ s) ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
ENNReal.mul_rpow_of_nonneg,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ (‖c‖ₑ ^ p.toReal) ^ (1 / p.toReal) * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

case hz
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : 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
⊢ eLpNorm (fun x ↦ c) p μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_ne_zero hp_ne_top

Goal state after:
case pos
α : 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
⊢ ∫⁻ (a : α), ‖c‖ₑ ^ p.toReal ∂μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) =
    (μ i) (s i) * (Measure.pi fun i_1 ↦ μ (i.succAbove i_1)) (univ.pi fun i_1 ↦ s (i.succAbove i_1))

Tactic:
← prod_prod

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) := (MeasurableEquiv.piFinSuccAbove α i).symm
s : (i : Fin (n + 1)) → Set (α i)
x✝ : ∀ (i : Fin (n + 1)), MeasurableSet (s i)
⊢ ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j))) (⇑e ⁻¹' univ.pi s) =
    ((μ i).prod (Measure.pi fun i_1 ↦ μ (i.succAbove i_1))) (s i ×ˢ univ.pi fun i_1 ↦ s (i.succAbove i_1))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
refine lintegral_mono_ae ?_

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∀ᵐ (a : α) ∂μ, s.indicator (fun x ↦ ↑C ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [hx]

Goal state after:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
this : (fun x ↦ ‖f x‖ₑ ^ q) =ᵐ[μ] fun x ↦ ‖g x‖ₑ ^ q
⊢ eLpNorm' f q μ = eLpNorm' g q μ
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: ⊢ 2⁻¹ + 2⁻¹ = 1⁻¹

Tactic:
rw [← two_mul, ENNReal.mul_inv_cancel]

Goal state after:
⊢ 1 = 1⁻¹

case h0
⊢ 2 ≠ 0

case ht
⊢ 2 ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ MemLp f p μ

Tactic:
apply (memLp_const_enorm hC).of_le_enorm (ε' := ℝ≥0∞) hf <| hfC.mono fun _x hx ↦ ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
_x : α
hx : ‖f _x‖ₑ ≤ C
⊢ ‖f _x‖ₑ ≤ ‖C‖ₑ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (p - 1) / (p - 1) + 1 / (p - 1)

Tactic:
ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp),

Goal state after:
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = 1 + 1 / (p - 1)
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 / y - 1

Tactic:
rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]

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
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun x ↦ ‖f x‖₊) → eLpNormEssSup f μ < ∞

Tactic:
rintro ⟨C, hC⟩

Goal state after:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ∞
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 < z - y
⊢ -1 ≤ z / y - 1

Tactic:
rw [le_sub_iff_add_le, neg_add_cancel, div_nonneg_iff]

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 < z - y
⊢ 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0