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
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ AffineIndependent k fun x ↦ ↑x

Tactic:
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }
⊢ AffineIndependent k fun x ↦ ↑x
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 1 2)]
  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
x : E
r : ℝ
y : E
⊢ y ∈ (normSeminorm 𝕜 E).ball x r ↔ y ∈ Metric.ball x r

Tactic:
simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]

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

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

Tactic:
exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)

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

Goal state before:
pp: case inl
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
h : AffineIndependent k fun p ↦ ↑p
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
have p₁ : P := AddTorsor.nonempty.some
    let hsv := Basis.ofVectorSpace k V
    have hsvi := hsv.linearIndependent
    have hsvt := hsv.span_eq
    rw [Basis.coe_ofVectorSpace] at hsvi hsvt
    have h0 : ∀ v : V, v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0 := by
      intro v hv
      simpa [hsv] using hsv.ne_zero ⟨v, hv⟩
    rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
    exact
      ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' _, Set.empty_subset _, hsvi,
        affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt⟩

Goal state after:
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
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False

Tactic:
finsum,

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : (if h : HasFiniteSupport ((fun i ↦ w i) ∘ PLift.down) then ∑ i ∈ Finite.toFinset h, w i.down else 0) = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1

Tactic:
finsum,

Goal state after:
case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : (if h : HasFiniteSupport ((fun i ↦ w i) ∘ PLift.down) then ∑ i ∈ Finite.toFinset h, w i.down else 0) = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub : support ((fun i ↦ w i • z i) ∘ PLift.down) ⊆ ↑(Finite.toFinset hfin_w)
⊢ ∑ i ∈ Finite.toFinset hfin_w, w i.down = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case neg
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
⊢ ∀ i ∈ s, w i = 0

Tactic:
let w' : { y // y ≠ i } → k := fun x => w x

Goal state after:
case neg
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
⊢ ∀ i ∈ s, w i = 0
Module: Mathlib.Topology.Connected.LocallyPathConnected

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

Tactic:
have : ∀ i, Nonempty (Z i) := Classical.nonempty_pi.mp ⟨x⟩

Goal state after:
case refine_1.inr
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
h : LocallyPathConnectedSpace ((i : ι) → Z i)
x : (i : ι) → Z i
this : ∀ (i : ι), Nonempty (Z i)
⊢ IsEmpty ((i : ι) → Z i) ∨ (∀ (i : ι), LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : ∃ b, x < b
x✝¹ x✝ : R
h₁ : x✝¹ < x
h₂ : x < x✝
⊢ Ioo x✝¹ x✝ ∈ 𝓝 x ∧ Convex R (Ioo x✝¹ x✝)

Tactic:
simp [h₁, h₂, Ioo_mem_nhds, convex_Ioo]

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

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := ⋯
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ z ∈ sphere 0 r

Tactic:
simp_all [norm_smul]

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

Goal state before:
pp: R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U

Tactic:
rw [hU, Filter.eventually_iff]

Goal state after:
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ {x | x • v ∈ (s.sup p).ball 0 r} ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
have h' : 0 < I.sup' hI r := by
      rcases hI with ⟨i, hi⟩
      exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)

Goal state after:
case pos
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
this : CompactSpace ↑A := isCompact_iff_compactSpace.mp hA
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace] (A.domRestrict (⇑(CompactCoherentification.mk Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst✝] (A.domRestrict f)

Tactic:
exact continuous_mk_comp_iff_of_compactSpace

Goal state after:
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
G✝ : Type u_5
inst✝³⁴ : AddCommGroup E✝
inst✝³³ : Module 𝕜₁ E✝
inst✝³² : TopologicalSpace E✝
inst✝³¹ : AddCommGroup F✝
inst✝³⁰ : Module 𝕜₂✝ F✝
𝕜 : Type u_6
𝕜₂ : Type u_7
𝕜₃ : Type u_8
𝕜₄ : Type u_9
E : Type u_10
F : Type u_11
G : Type u_12
H : Type u_13
inst✝²⁹ : AddCommGroup E
inst✝²⁸ : AddCommGroup F
inst✝²⁷ : AddCommGroup G
inst✝²⁶ : AddCommGroup H
inst✝²⁵ : NormedField 𝕜
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁷ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁶ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁵ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁴ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
𝔖 : Set (Set E)
𝔗 : Set (Set F)
h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁₂ ⁻¹' t ∈ 𝔖
mapsto₁ : MapsTo (fun x ↦ ⇑e₁₂ '' x) 𝔖 𝔗
t : Set F
⊢ t ∈ 𝔗 → (fun x ↦ ⇑e₁₂.symm '' x) t ∈ 𝔖

Tactic:
by simp [h, e₁₂.image_symm_eq_preimage]

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

Goal state before:
pp: case inl
ι : Type u_1
u : ι → ℝ≥0
⊢ limsup (fun i ↦ ↑(u i)) ⊥ = ↑(limsup u ⊥)

pp: case inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)

Tactic:
· simp [limsup, limsSup]

Goal state after:
case inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
⊢ limsup (fun i ↦ ↑(u i)) f = ↑(limsup u f)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inl
α : Type u_1
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ fun a ↦ (u a).toReal
⊢ (limsup u ⊥).toReal = limsup (fun a ↦ (u a).toReal) ⊥

pp: case inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
⊢ (limsup u f).toReal = limsup (fun a ↦ (u a).toReal) f

Tactic:
· simp [limsup, limsSup]

Goal state after:
case inr
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
⊢ (limsup u f).toReal = limsup (fun a ↦ (u a).toReal) f
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
⊢ s ⊆ t

Tactic:
by
  have hsf := finite_of_uniformOn_ne_zero (by rw [h]; exact one_ne_zero)
  rw [uniformOn, cond_apply hsf.measurableSet, mul_comm] at h
  replace h := ENNReal.eq_inv_of_mul_eq_one_left h
  rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _),
    Nat.cast_inj] at h
  suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
  rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
  exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ (uniformOn s) (t ∪ u) = (uniformOn s) t + (uniformOn s) u

Tactic:
rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
    cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]

Goal state after:
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * Measure.count[s | s ∪ t] +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count[t | s ∪ t] =
    Measure.count[u | s ∪ t]

Tactic:
cond_apply (hs.union ht).measurableSet,

Goal state after:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count[t | s ∪ t] =
    Measure.count[u | s ∪ t]
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count[t | s ∪ t] =
    Measure.count[u | s ∪ t]

Tactic:
cond_apply (hs.union ht).measurableSet,

Goal state after:
case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) +
      (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) =
    Measure.count[u | s ∪ t]
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) fun i ↦ (f i).toReal
hμ : NeZero μ
⊢ (essSup f μ).toReal = essSup (fun a ↦ (f a).toReal) μ

Tactic:
exact ENNReal.toReal_limsup h₁

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
B : 0 < (μ.restrict s) t
⊢ c < essSup f (μ.restrict s)

Tactic:
apply cd.trans_le

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := ⋯
A : 0 < (μ.restrict t) t
B : 0 < (μ.restrict s) t
⊢ d ≤ essSup f (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf

Tactic:
simp_rw [smul_mk, op_smul_eq_smul]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), generateFrom (C i) = inst✝ i
h2C : ∀ (i : ι), IsPiSystem (C i)
h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
μν : Measure ((i : ι) → α i)
h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (univ.pi s) = ∏ i, (μ i) (s i)
h4C : ∀ (i : ι), ∀ s ∈ C i, MeasurableSet s
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), s i ∈ C i
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ (Measure.pi μ) (univ.pi s) = μν (univ.pi s)

Tactic:
simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ε ≤ ‖f x‖₊} < ∞

Tactic:
simp_rw [← ENNReal.coe_le_coe]

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ μ {x | ↑ε ≤ ↑‖f x‖₊} < ∞
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (map (fun x ↦ v * x) (Measure.pi μ)) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
rw [map_apply (measurable_const_mul _) (MeasurableSet.univ_pi hs),
    show (v * ·) ⁻¹' univ.pi s = univ.pi fun i => (v i * ·) ⁻¹' s i by rfl, pi_pi]

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulLeftInvariant
v : (i : ι) → α i
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ i) ((fun x ↦ v i * x) ⁻¹' s i) = ∏ i, (μ i) (s i)
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 ∂μ) ^ (1 / p) ≤ c * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.mul_rpow_of_nonneg _ _ hp.le]

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 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
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
⊢ 0 ≤ 1 / q

Tactic:
by simp [hq_pos.le]

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 : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · rw [h_top]
    exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h
  simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
  exact eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h (ENNReal.toReal_pos h0 h_top)

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

Goal state before:
pp: case neg
α : 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‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∉ s
⊢ s.indicator (fun x ↦ ↑C ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
· simp [Set.indicator_of_notMem hxs]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
by
  have hxz := hxy.trans hyz
  have hxz' := hxz.ne
  rw [← sub_pos] at hxy hxz hyz
  have ha : 0 < (z - y) / (z - x) := by positivity
  have hb : 0 < (y - x) / (z - x) := by positivity
  have key := hf.2 hx hz hxz' ha hb (by field)
  simp only [smul_eq_mul] at key
  ring_nf at key
  field_simp at key ⊢
  linarith

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q

Tactic:
have h_rpow : essSup (‖‖f ·‖ₑ ^ q‖ₑ) μ = essSup (‖f ·‖ₑ ^ q) μ := by congr

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ ^ q) μ
⊢ essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr.inl
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' : s < 0
⊢ 1 + p * s < 1 + s

Tactic:
· gcongr
      exact mul_lt_of_one_lt_left hs' hp

Goal state after: