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

Goal state before:
pp: case neg
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
hj : j ∉ s
⊢ Function.update w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1

Tactic:
Function.update_self,

Goal state after:
case neg
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
hj : j ∉ s
⊢ 1 - (s \ {j}).sum w + ∑ x ∈ s, w x = 1
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) < r ↔ p (x✝ - a⁻¹ • y) < r / ‖a‖

Tactic:
lt_div_iff₀ (norm_pos_iff.mpr ha),

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) < r ↔ p (x✝ - a⁻¹ • y) * ‖a‖ < r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) < r ↔ ‖a‖ * p (x✝ - a⁻¹ • y) < r

Tactic:
←
      map_smul_eq_mul p,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) < r ↔ p (a • (x✝ - a⁻¹ • y)) < r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) ≤ r ↔ ‖a‖ * p (x✝ - a⁻¹ • y) ≤ r

Tactic:
←
      map_smul_eq_mul p,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ p (a • x✝ - y) ≤ r ↔ p (a • (x✝ - a⁻¹ • y)) ≤ r
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 :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ ∑ i ∈ s, w2 i = 1

Tactic:
simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]

Goal state after:
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
I : Set k
n : ℕ
s : Simplex k P n
⊢ Simplex.setInterior I s ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
rintro p ⟨w, hw, hi, rfl⟩
  exact affineCombination_mem_affineSpan_of_nonempty hw _

Goal state after:
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✝ : PartialOrder k
n : ℕ
s : Simplex k P n
⊢ s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
rintro p ⟨w, hw, hi, rfl⟩
  exact affineCombination_mem_affineSpan_of_nonempty hw _

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
t : Finset ι
w : ι → R
z : ι → E
w' : ι → R
h : ∀ i ∈ t, w i = w' i
⊢ t.centerMass w z = t.centerMass w' z

Tactic:
by
  classical
  exact centerMass_congr (by grind)

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
t : Finset ι
w : ι → R
z z' : ι → E
h : ∀ i ∈ t, w i ≠ 0 → z i = z' i
⊢ t.centerMass w z = t.centerMass w z'

Tactic:
by
  classical
  exact centerMass_congr (by grind)

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

Goal state before:
pp: case refine_1
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 ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w
⊢ ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

Tactic:
rcases h with ⟨r, hr⟩
    refine ⟨r, fun i hi => ?_⟩
    rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr
    have hw' : (∑ j ∈ s, (r • (w₁ - w₂) - w) j) = 0 := by
      simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
    have hr' := h s _ hw' hr i hi
    rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]
    exact hr'

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✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
ha : 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
c : k
⊢ ∑ i ∈ s, (AffineMap.lineMap w₁ w₂) c i = 1

Tactic:
simp [AffineMap.lineMap_apply, sum_add_distrib, ← mul_sum, hw₁, hw₂]

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

Goal state before:
pp: case insert
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
⊢ (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    0 < ∑ i ∈ insert i t, w i → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s

Tactic:
| insert i t hi ht =>

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

Goal state before:
pp: case inl.refine_2
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
inst✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inl '' pathComponentIn (inl ⁻¹' u) x)

Tactic:
exact isOpenMap_inl _ <| (hu.preimage continuous_inl).pathComponentIn _

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

Goal state before:
pp: case inl.refine_2
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : IsBot x
inst✝ : OrderBot R
⊢ ∀ (i' : Set R), i' ∈ 𝓝 ⊥ ∧ Convex R i' → id i' ∈ 𝓝 ⊥

Tactic:
· simp +contextual

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

Goal state before:
pp: case inr.inl.refine_2
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 : IsTop x
inst✝ : OrderTop R
⊢ ∀ (i' : Set R), i' ∈ 𝓝 ⊤ ∧ Convex R i' → id i' ∈ 𝓝 ⊤

Tactic:
· simp +contextual

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

Goal state before:
pp: case inr.inr.refine_2
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
⊢ ∀ (i' : Set R), i' ∈ 𝓝 x ∧ Convex R i' → id i' ∈ 𝓝 x

Tactic:
· simp +contextual

Goal state after:
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
s : Set E
⊢ (convexHull R) s ⊆ ⋃ t, ⋃ (_ : ↑t ⊆ s), (convexHull R) ↑t

Tactic:
rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)

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
this :
  f (∑ i ∈ t with w i ≠ 0, w i • p i) = ∑ i ∈ t with w i ≠ 0, w i • f (p i) ↔
    ∀ ⦃j : ι⦄, j ∈ {x ∈ t | w x ≠ 0} → ∀ ⦃k : ι⦄, k ∈ {x ∈ t | w x ≠ 0} → p j = p k
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ ⦃j : ι⦄, j ∈ t → w j ≠ 0 → ∀ ⦃k : ι⦄, k ∈ t → w k ≠ 0 → p j = p k

Tactic:
grind [sum_filter_of_ne, left_ne_zero_of_smul]

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
this :
  f (∑ i ∈ t with w i ≠ 0, w i • p i) < ∑ i ∈ t with w i ≠ 0, w i • f (p i) ↔
    ∃ j ∈ {x ∈ t | w x ≠ 0}, p j ≠ ∑ i ∈ t with w i ≠ 0, w i • p i
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, w j ≠ 0 ∧ p j ≠ ∑ i ∈ t, w i • p i

Tactic:
grind [sum_filter_of_ne, left_ne_zero_of_smul]

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

Goal state before:
pp: case h
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 ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (s.sup p).ball (0 + 0) (r / 2 + r / 2) ⊆ U

Tactic:
rw [hU, add_zero, add_halves]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ ∃ s C, (p i).comp LinearMap.id ≤ C • s.sup fun i ↦ (Finset.Iic i).sup p

Tactic:
refine ⟨{i}, 1, ?_⟩

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup fun i ↦ (Finset.Iic i).sup p
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h✝ : Nontrivial E
this : NormedSpace ℝ E
ub : ℝ≥0
hub : ub < ‖f‖₊
x : E
hx : ‖x‖₊ = 1
hxf : ub < ‖f x‖₊
⊢ x ∈ sphere 0 1

Tactic:
simpa using! congrArg NNReal.toReal hx

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

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance

Tactic:
UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
by
  obtain rfl | hf := f.eq_or_neBot
  · simp [limsup, limsSup]
  by_cases hf : f.IsBoundedUnder (· ≤ ·) u; swap
  · simp [*]
  have : f.IsCoboundedUnder (· ≤ ·) u := by isBoundedDefault
  refine eq_of_forall_le_iff fun c ↦ ?_
  rw [← Real.toNNReal_le_iff_le_coe, le_limsup_iff (by simpa) (by simpa), le_limsup_iff ‹_›]
  simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]
  refine forall₂_congr fun r hr ↦ ?_
  simpa using (le_or_gt 0 r).imp_right fun hr ↦ .of_forall fun i ↦ hr.trans_le (by simp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
⊢ f.toGerm = ↑↑g

Tactic:
← toGerm_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f g : α →ₘ[μ] β
H : f.toGerm = g.toGerm
⊢ f.toGerm = g.toGerm
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ n s ≤ piPremeasure m s

Tactic:
refine le_trans (n.mono <| subset_pi_eval_image univ s) (h _ ?_)

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
n : OuterMeasure ((i : ι) → α i)
h : ∀ (s : (i : ι) → Set (α i)), (univ.pi s).Nonempty → n (univ.pi s) ≤ ∏ i, (m i) (s i)
s : Set ((i : ι) → α i)
hs : s.Nonempty
⊢ (univ.pi fun i ↦ eval i '' s).Nonempty
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 : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
A : Inv.inv ⁻¹' univ.pi s = univ.pi fun i ↦ Inv.inv ⁻¹' s i
⊢ (Measure.pi μ).inv (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
Measure.inv,

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 : ι), MeasurableInv (α i)
inst✝ : ∀ (i : ι), (μ i).IsInvInvariant
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
A : Inv.inv ⁻¹' univ.pi s = univ.pi fun i ↦ Inv.inv ⁻¹' s i
⊢ (map Inv.inv (Measure.pi μ)) (univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi fun i' ↦ μ (f i')) (univ.pi fun i ↦ s (f i)) = ∏ i, (μ i) (s i)

Tactic:
pi_pi _ _,

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
s : (i : ι) → Set (α i)
x✝ : ∀ (i : ι), MeasurableSet (s i)
⊢ ∏ i, (μ (f i)) (s (f i)) = ∏ i, (μ i) (s i)
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inr.inl.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
hya : y < a
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
convert! hf.secant_mono_aux3 hx ha hxy hya using 1 <;> rw [← neg_div_neg_eq] <;> simp

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

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

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top]
  rw [eLpNorm'_smul_measure ENNReal.toReal_nonneg]
  congr
  simp_rw [one_div]
  rw [ENNReal.toReal_inv]

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

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p / q = p - 1

Tactic:
by
  field_simp [h.symm.ne_zero]
  linear_combination -h.sub_one_mul_conj

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

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

Tactic:
simpa using add_halves (1 : ℝ≥0)

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

Goal state before:
pp: p q : ℝ≥0
h : p.HolderConjugate q
⊢ p / q = p - 1

Tactic:
by
  field_simp [h.symm.ne_zero]
  linear_combination -h.sub_one_mul_conj

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

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

Tactic:
gcongr
      exact mul_lt_of_lt_one_left hs' hp2

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

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

Tactic:
convert! hf.secant_strict_mono_aux3 hx ha hxy hya using 1

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f x - f a) / (x - a) = (f a - f x) / (a - x)

case e'_4
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa✝ : x ≠ a
hya✝ : y ≠ a
hxy : x < y
hxa : x < a
hya : y < a
⊢ (f y - f a) / (y - a) = (f a - f y) / (a - y)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ConvexOn ℝ univ fun x ↦ b ^ x

Tactic:
convert! convexOn_exp.comp_linearMap (LinearMap.mul ℝ ℝ (Real.log b)) using 1

Goal state after:
case e'_12
b : ℝ
hb : 0 < b
⊢ (fun x ↦ b ^ x) = rexp ∘ ⇑((LinearMap.mul ℝ ℝ) (log b))
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 ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞

Tactic:
hf.eLpNorm_map_measure

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Tactic:
monovaryOn_inv_left₀ hf,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Semifield β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
s : Set ι
f : ι → α
g : ι → β
hf : ∀ (i : ι), i ∈ s → 0 < f i
hg : ∀ (i : ι), i ∈ s → 0 < g i
⊢ AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Tactic:
by
  simp only [smul_eq_mul, antivaryOn_iff_smul_rearrangement]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case hnc
p : ℝ≥0∞
hp : 1 ≤ p
h : p ∈ Set.Ioo 0 1
⊢ False

Tactic:
exact lt_irrefl _ (h.2.trans_le hp)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
apply le_trans this

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 < z i
p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i
s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹
this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
⊢ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm' f p.toReal μ < ∞