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

Goal state before:
pp: case inr
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k (⇑f '' s)

Tactic:
apply ext_of_direction_eq

Goal state after:
case inr.hd
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ (map f (affineSpan k s)).direction = (affineSpan k (⇑f '' s)).direction

case inr.hn
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ (↑(map f (affineSpan k s)) ∩ ↑(affineSpan k (⇑f '' s))).Nonempty
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
h₂₃₅₆ : ∃ z, z • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
h₃₁₆₄ : ∃ z, z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
obtain ⟨r₂, hr₂⟩ := h₂₃₅₆

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
h₃₁₆₄ : ∃ z, z • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
r₁ : kˣ
hr₁ : r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ ↑r₁ • (p₃ -ᵥ p₂) + ↑r₁ • (p₂ -ᵥ p₁) ∈ vectorSpan k {p₁, p₃}

Tactic:
← smul_add,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ ↑r₁ • (p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)) ∈ vectorSpan k {p₁, p₃}
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : s.sum (Function.const ι 1) = 1
⊢ (b.coord i) q = 1 q

Tactic:
have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by
    simp [eq_iff_true_of_subsingleton]

Goal state after:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
hp : (range ⇑b).Subsingleton
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : s.sum (Function.const ι 1) = 1
hq : q = (Finset.affineCombination k s ⇑b) (Function.const ι 1)
⊢ (b.coord i) q = 1 q
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
⊢ Injective p

Tactic:
intro i j hij
  rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha
  by_contra hij'
  refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)
  simp_all only [ne_eq]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (range fun x_1 ↦ (p x_1) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
⊢ BddAbove (range fun i ↦ (p i) x)

Tactic:
rcases h _ hc with ⟨M, hM⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (range fun x_1 ↦ (p x_1) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : M ∈ upperBounds (range fun x_1 ↦ (p x_1) (c • x))
⊢ BddAbove (range fun i ↦ (p i) x)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: 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 : ℕ
s1 s2 : Simplex k P n
h : ∀ (i : Fin (n + 1)), s1.points i = s2.points i
⊢ s1 = s2

Tactic:
cases s1

Goal state after:
case mk
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 : ℕ
s2 : Simplex k P n
points✝ : Fin (n + 1) → P
independent✝ : AffineIndependent k points✝
h : ∀ (i : Fin (n + 1)), { points := points✝, independent := independent✝ }.points i = s2.points i
⊢ { points := points✝, independent := independent✝ } = s2
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hw : p = (affineCombination k univ (s.map f hf).points) w
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, f x = p

Tactic:
hw,

Goal state after:
case pos
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hw : p = (affineCombination k univ (s.map f hf).points) w
⊢ (affineCombination k univ (s.map f hf).points) w ∈ Simplex.setInterior I (s.map f hf) ↔
    ∃ x ∈ Simplex.setInterior I s, f x = (affineCombination k univ (s.map f hf).points) w
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ t.centerMass (fun j ↦ if i = j then 1 else 0) z = z i

Tactic:
by
  rw [Finset.centerMass_eq_of_sum_1]
  · trans ∑ j ∈ t, if i = j then z i else 0
    · congr with i
      split_ifs with h
      exacts [h ▸ one_smul _ _, zero_smul _ _]
    · rw [sum_ite_eq, if_pos hi]
  · rw [sum_ite_eq, if_pos hi]

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
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ (∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i = t'.centerMass w z

Tactic:
sum_subset ht h,

Goal state after:
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
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ (∑ x ∈ t', w x)⁻¹ • ∑ i ∈ t, w i • z i = t'.centerMass w z
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 ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ r • ∑ x ∈ s, w₁ x - r • ∑ x ∈ s, w₂ x - ∑ x ∈ s, w x = 0

Tactic:
hw,

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
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
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
⊢ r • ∑ x ∈ s, w₁ x - r • ∑ x ∈ s, w₂ x - 0 = 0
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
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
have hfin_w : HasFiniteSupport (w ∘ PLift.down) := by
    by_contra H
    rw [finsum, dif_neg H] at h₁
    exact zero_ne_one h₁
  have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
    (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge
  rw [finsum_eq_sum_plift_of_support_subset hsub]
  refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_
  · rwa [finsum, dif_pos hfin_w] at h₁
  · rwa [hfin_w.mem_toFinset] at hi

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

Goal state before:
pp: case inl.refine_1
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✝ : R
a✝ : ⊥ < i✝
⊢ Iio i✝ ∈ 𝓝 ⊥ ∧ Convex R (Iio i✝)

Tactic:
simp_all [Iio_mem_nhds, convex_Iio]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x : E
hx : x ∈ (convexHull ℝ) s
y : E
hy : y ∈ (convexHull ℝ) s
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x' y' ≤ ediam s

Tactic:
exact edist_le_ediam_of_mem hx' hy'

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 ι
U V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩

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 ι
U V : Set E
hU✝ : U ∈ p.basisSets
hV : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1.refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ (p i).ball 0 ε ∈ p.moduleFilterBasis.toFilterBasis

Tactic:
rw [← (Finset.sup_singleton : _ = p i)]

Goal state after:
case refine_1.refine_1
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ({i}.sup p).ball 0 ε ∈ p.moduleFilterBasis.toFilterBasis
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
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s

Tactic:
have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc

Goal state after:
𝕜 : 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
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : c • p.ball 0 ‖c⁻¹‖ ⊆ c • s
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s
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
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ CompleteSpace (E →SLᵤ[σ, 𝔖] F)

Tactic:
completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ IsComplete (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
hf : MapsTo (⇑f) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
rcases lebesgue_number_of_compact_open (hK.image (map_continuous f)) hU hf.image_subset
        with ⟨V, hV, -, hVf⟩

Goal state after:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
hf : MapsTo (⇑f) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ x ∈ ⇑f '' K, ball x V ⊆ U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : CompactSpace ↑s
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ Tendsto (fun i ↦ { toFun := s.domRestrict (F i), continuous_toFun := ⋯ }) p
      (𝓝 { toFun := s.domRestrict f, continuous_toFun := ⋯ }) ↔
    TendstoUniformlyOn F f p s

Tactic:
by
  rw [ContinuousMap.tendsto_iff_tendstoUniformly, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]
  congr!

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

Goal state before:
pp: case mp
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≥ b
⊢ ∃ x, ∃ (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ ↑(u a)

Tactic:
exact ⟨b.toNNReal, by simp, by simpa⟩

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

Goal state before:
pp: case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ∞ ≤ if u x = 0 then 0 else ∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
      eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)

Goal state after:
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ∞ ≤ if u x = 0 then 0 else ∞
h_top_le : limsup (fun x ↦ if u x = 0 then 0 else ∞) f = ∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ ↑(g.compQuasiMeasurePreserving f hf) =ᵐ[μ] ↑(g.compQuasiMeasurePreserving f' ⋯)

Tactic:
grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]

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
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
| Measure.count s * ((Measure.count s)⁻¹ * Measure.count (s ∩ u)) * (Measure.count (s ∪ t))⁻¹ +
    (Measure.count t)⁻¹ * Measure.count (t ∩ u) * Measure.count t * (Measure.count (s ∪ t))⁻¹

Tactic:
mul_comm _ (Measure.count t),

Goal state after:
Ω : 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)⁻¹ * Measure.count (s ∩ u)) * (Measure.count (s ∪ t))⁻¹ +
    Measure.count t * ((Measure.count t)⁻¹ * Measure.count (t ∩ u)) * (Measure.count (s ∪ t))⁻¹
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case h
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ t \ (fun b ↦ b i) ⁻¹' s ⊆ t

Tactic:
apply sdiff_subset

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

Goal state before:
pp: α : Type u_1
q : ℝ
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : MeasurableSpace α
f : α → ε
hq_pos : 0 < q
⊢ eLpNorm' f q 0 = 0

Tactic:
simp [eLpNorm', hq_pos]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
exact eLpNorm_indicator_sub_le_of_dist_bdd μ hp hs hc (fun x _ ↦ h x)

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

Goal state before:
pp: α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
x : α
hx : ‖f x‖₊ = ‖g x‖₊
⊢ (fun x ↦ ‖f x‖ₑ ^ q) x = (fun x ↦ ‖g x‖ₑ ^ q) x

Tactic:
simp [enorm, hx]

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

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hr₀ : r ≠ 0
hr : r ≠ ∞
⊢ (p / r)⁻¹ + (q / r)⁻¹ = 1⁻¹

Tactic:
by
    rw [ENNReal.inv_div (.inl hr) (.inl hr₀), ENNReal.inv_div (.inl hr) (.inl hr₀), div_eq_mul_inv,
      div_eq_mul_inv, ← mul_add, inv_add_inv_eq_inv p q r, ENNReal.mul_inv_cancel hr₀ hr, inv_one]

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
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z

Tactic:
by
  have hxy' : 0 < y - x := by linarith
  have hyz' : 0 < z - y := by linarith
  have hxz' : 0 < z - x := by linarith
  have ha : 0 < (z - y) / (z - x) := by positivity
  have hb : 0 < (y - x) / (z - x) := by positivity
  have key := hf.2 hx hz (by linarith) ha hb ?_
  · simp only [smul_eq_mul] at key
    ring_nf at key
    field_simp at key
    linear_combination key
  · field

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

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y : 𝕜
hx : x ∈ s
hxy : x < y
hxy' : f x < f y
u : 𝕜
hu : u ∈ s ∩ Set.Ici y
v : 𝕜
hv : v ∈ s ∩ Set.Ici y
huv : u < v
step1 : ∀ {z : 𝕜}, z ∈ s ∩ Set.Ioi y → f y < f z
hu2 : y < u
⊢ u ∈ Set.Ioo y v

Tactic:
exact ⟨hu2, huv⟩

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (-(a • x + b • y)) = log (a • x + b • y)

Tactic:
rw [log_neg_eq_log]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
by
  rw [one_div,
    ← @NNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1]), inv_inv]
  exact add_rpow_le_rpow_add _ _ hp1

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case refine_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ (∑ i ∈ s, w i * z i) ^ p = ∞ → ∑ i ∈ s, w i * z i ^ p = ∞

Tactic:
rw [rpow_eq_top_iff, sum_eq_top, sum_eq_top]

Goal state after:
case refine_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ ∑ i ∈ s, w i * z i = 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ∞) ∧ 0 < p → ∃ a ∈ s, w a * z a ^ p = ∞
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
rwa [ENNReal.inv_lt_one, one_lt_ofReal]

Goal state after:
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 = ∞
hq_top : q = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [hp_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 : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f ∞ μ < ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, w i / ∑ i ∈ s, w i = 1

Tactic:
simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]

Goal state after:
case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ (∑ i ∈ s, w i) * (∑ i ∈ s, w i)⁻¹ = 1