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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
⊢ (fs'.weightedVSub p) w' = 0

Tactic:
← hs,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
hw's : ∑ i ∈ fs', w' i = 0
⊢ (fs'.weightedVSub p) w' = (fs.weightedVSub (p ∘ ⇑f)) w
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ (↑q)ᶜ = ⇑(p.prodEquivOfIsCompl q hpq) '' {0}ᶜ ×ˢ univ

Tactic:
prod_univ,

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
p q : Submodule ℝ E
hpq : IsCompl p q
hpc : IsPathConnected {0}ᶜ
⊢ (↑q)ᶜ = ⇑(p.prodEquivOfIsCompl q hpq) '' Prod.fst ⁻¹' {0}ᶜ
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range (s.faceOpposite i).points)
⊢ w i = 0

Tactic:
rw [range_faceOpposite_points] at h

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)
⊢ w i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ∑ j ∈ t, w j = 0
ws : ∀ j ∈ t, w j = 0
wz : ∑ j ∈ t, w j • z j = 0
⊢ (insert i t).centerMass w z ∈ s

Tactic:
simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]

Goal state after:
case pos
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ∑ j ∈ t, w j = 0
ws : ∀ j ∈ t, w j = 0
wz : ∑ j ∈ t, w j • z j = 0
⊢ (w i)⁻¹ • w i • z i ∈ s
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 ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (∃ r, ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Tactic:
simp only [Pi.sub_apply, sub_eq_iff_eq_add]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
⊢ StrictConvex 𝕜 s

Tactic:
by
  refine strictConvex_iff_openSegment_subset.2 ?_
  intro x hx y hy hne
  by_cases hx' : x ∈ interior s
  · exact hs.openSegment_interior_self_subset_interior hx' hy
  by_cases hy' : y ∈ interior s
  · exact hs.openSegment_self_interior_subset_interior hx hy'
  rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩
  refine (openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)
  exacts [hs.openSegment_self_interior_subset_interior hx hc,
    hs.openSegment_interior_self_subset_interior hc hy]

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

Goal state before:
pp: case neg
ι : 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
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
this : PathConnectedSpace (Z i)
⊢ IsPathConnected univ

Tactic:
exact isPathConnected_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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * (w₂ i - 0) + 0) = SignType.sign (r * (w₂ j - w₁ j) + w₁ j)

Tactic:
hj0,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * (w₂ i - 0) + 0) = SignType.sign (r * (w₂ j - 0) + 0)
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 → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ j ∉ u

Tactic:
simp [u]

Goal state after:
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 → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj✝ : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ k ∉ u

Tactic:
simp [u]

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

Goal state before:
pp: case neg
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ (s.sup p).ball 0 r ⊆ (fun y ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
    preimage_const_of_mem, zero_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
⊢ (convexHull 𝕜) (range s.points) = s.closedInterior

Tactic:
by
  ext p
  rw [convexHull_range_eq_exists_affineCombination, Set.mem_ofPred]
  constructor <;> intro h
  · obtain ⟨u, w, hw, hw1, rfl⟩ := h
    have hw' : ∀ i ∈ u, w i ≤ 1 := by
      intro i hi
      rw [← hw1]
      apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi
    have hw1' : ∑ i, (u : Set (Fin (n + 1))).indicator w i = 1 := by
      simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1
    rw [Finset.affineCombination_indicator_subset _ _ u.subset_univ,
      affineCombination_mem_closedInterior_iff hw1']
    intro i
    by_cases hi : i ∈ (u : Set (Fin (n + 1))) <;> aesop
  · obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan
    rw [affineCombination_mem_closedInterior_iff hw1] at h
    exact ⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : FunLike 𝓕 E F
inst✝ : SemilinearMapClass 𝓕 σ₁₂ E F
f : 𝓕
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑f
x : E
hx : 0 ⤳ x
⊢ f 0 ⤳ f x

Tactic:
exact hx.map hf

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖ = 1
H₂ : ‖f x‖ / ‖x‖ ≤ C
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
div_le_iff₀

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖ = 1
H₂ : ‖f x‖ ≤ C * ‖x‖
⊢ ‖f x‖ ≤ C * ‖x‖

𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖ = 1
H₂ : ‖f x‖ / ‖x‖ ≤ C
⊢ 0 < ‖x‖
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

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

Tactic:
by
  rw [← sInf_pair]
  exact .sInf (by simp [ht₁, ht₂])

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Continuous[instTopologicalSpace, inst✝] ⇑(CompactCoherentification.mk X).symm

Tactic:
rw [continuous_dom_iff]
  exact fun _ _ ↦ continuousOn_id

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Tendsto F p (𝓝 f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
rw [tendsto_nhds_compactOpen]

Goal state after:
α : 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
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
this : 0 < x
⊢ ∀ᶠ (a : α) in f, u a < x

Tactic:
filter_upwards [h (.ofReal x) (by simpa [this] using hx)] with a ha

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
this : 0 < x
a : α
ha : ENNReal.ofReal (u a) < ENNReal.ofReal x
⊢ u a < x
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case zero
α : Type u_1
γ : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
⊢ (fun x ↦ x.compQuasiMeasurePreserving f hf)^[0] g = g.compQuasiMeasurePreserving f^[0] ⋯

Tactic:
| zero =>

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i s i'

Tactic:
subst h; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ f ≤ f ⊔ g

Tactic:
rw [← coeFn_le]
  filter_upwards [coeFn_sup f g] with _ ha
  rw [ha]
  exact le_sup_left

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

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩

Goal state after:
case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
i : ι
hi : s i = ∅
this : ∃ i, (m i) (s i) = 0
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

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

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h
  · simp [h]
  exact (boundedBy_le _).trans_eq (piPremeasure_pi h)

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

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)

Tactic:
inv_mul_cancel₀ hp.ne',

Goal state after:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ 1 ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : 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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)

Tactic:
inv_mul_cancel₀ hp.ne',

Goal state after:
α : 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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ 1 ≤ ↑c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p) ≤ c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (p⁻¹ * p)

Tactic:
inv_mul_cancel₀ hp.ne',

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ 1 ≤ c ^ p * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ 1
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i ↦ (μ i).prod (ν i)) =
    (Measure.pi fun i ↦ μ i).prod (Measure.pi fun i ↦ ν i)

Tactic:
refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm
    · refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning
    · rintro _ ⟨s, ⟨s, _, rfl⟩, ⟨_, ⟨t, _, rfl⟩, rfl⟩⟩
      rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow,
        MeasurableEquiv.coe_mk]
      rw [show Equiv.arrowProdEquivProdArrow γ _ _ ⁻¹' (univ.pi s ×ˢ univ.pi t) =
          (univ.pi fun i ↦ s i ×ˢ t i) by
          ext; simp [Set.mem_pi, forall_and]]
      simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]

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

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

Tactic:
simp [h₀]

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ (p - 1) * p⁻¹ = q⁻¹

Tactic:
rw [ENNReal.sub_mul (by simp_all), ENNReal.mul_inv_cancel this (by lia)]

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
hp : p ≠ ∞
this : p ≠ 0
⊢ 1 - 1 * p⁻¹ = q⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p q : ℝ
hq_pos : 0 < q
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p μ = eLpNorm' f (p * q) μ ^ q

Tactic:
simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div,
    mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm, mul_one, enorm_eq_self, ← ENNReal.rpow_mul, mul_comm]

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

Goal state before:
pp: case inr.inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) < log (1 + s) * p

Tactic:
· rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · gcongr
      exact lt_mul_of_one_lt_left hs' hp

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
rcases lt_or_gt_of_ne hxa with hxa | hxa

Goal state after:
case inr.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : x < a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

case inr.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
hxa : a < x
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c

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

Goal state before:
pp: case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p).HolderTriple ↑q ↑r

Tactic:
· rw [holderTriple_iff]
    have hp := h.ne_zero
    have hq := h.symm.ne_zero
    exact_mod_cast h.inv_add_inv_eq_inv

Goal state after: