mathlib-initiative/mathlib-tactics huggingface dataset:
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
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y < r - p x
⊢ y ∈ p.ball x r

Tactic:
exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x <;> rfl

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₁, p₃, p₂] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x <;> rfl

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₃, p₂, p₁] ∘ ⇑(Equiv.swap 0 2)) x = ![p₁, p₂, p₃] x

Tactic:
fin_cases x <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
⊢ (affineCombination k univ (s.points ∘ ⇑e.symm)) w ∈ Simplex.setInterior I s

Tactic:
rw [← Function.comp_id w, ← e.self_comp_symm, ← Function.comp_assoc,
      ← Equiv.coe_toEmbedding, ← Finset.univ.affineCombination_map e.symm.toEmbedding,
      map_univ_equiv]

Goal state after:
case refine_1
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
⊢ (affineCombination k univ s.points) (w ∘ ⇑e) ∈ Simplex.setInterior 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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∈ affineSpan k (p '' s) ↔ i ∈ s

Tactic:
by
  constructor
  · intro hs
    have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
    rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
  · exact fun h => mem_affineSpan k (Set.mem_image_of_mem p h)

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

Goal state before:
pp: S : Type u_1
inst✝³ : Semiring S
inst✝² : PartialOrder S
X : Type u_2
inst✝¹ : Fintype X
inst✝ : IsOrderedRing S
s : ↑(stdSimplex S X)
x : X
⊢ s x ≤ 1

Tactic:
rw [← sum_eq_one s]
  exact Finset.single_le_sum (by simp) (by simp)

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

Goal state before:
pp: E : Type u_3
𝕜 : Type u_4
inst✝¹¹ : Field 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : TopologicalSpace 𝕜
inst✝⁷ : OrderClosedTopology 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : ContinuousAdd 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsCompact ((convexHull 𝕜) s)

Tactic:
by
  rw [hs.convexHull_eq_image]
  let := hs.fintype
  exact (isCompact_stdSimplex 𝕜 s).image (LinearMap.continuous_on_pi _)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent x = connectedComponent y ↔ Joined x y

Tactic:
rw [← mem_pathComponent_iff, pathComponent_eq_connectedComponent, eq_comm]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
⊢ connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
x : Fin 2
⊢ ((fun x ↦ ![p₁, p₂, p₃] ↑x) ∘ ⇑(finSuccAboveEquiv 2)) x = ![p₁, p₂] x

Tactic:
fin_cases x <;> rfl

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₃, p₂] x

Tactic:
fin_cases x <;> rfl

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : p₁ ∉ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2)) x = ![p₃, p₂, p₁] x

Tactic:
fin_cases x <;> rfl

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 : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ SignType.sign (w i₂) = SignType.sign (w i₃)

Tactic:
refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_

Goal state after:
case refine_1
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 : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ ∑ i ∈ s, Pi.single i₁ 1 i = 1

case refine_2
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 : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ SignType.sign (affineCombinationLineMapWeights i₂ i₃ c i₂) =
    SignType.sign (affineCombinationLineMapWeights i₂ i₃ c i₃)
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 : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Tactic:
by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
  refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
  refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_
  rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

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

Goal state before:
pp: case refine_1
𝕜 : 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 : WithSeminorms fun x ↦ p
⊢ p.ball 0 1 ∈ 𝓝 0

pp: case refine_2
𝕜 : 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 : WithSeminorms fun x ↦ p
⊢ IsVonNBounded 𝕜 (p.ball 0 1)

pp: case refine_3
𝕜 : 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
⊢ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) → WithSeminorms fun x ↦ p

Tactic:
· apply (h.mem_nhds_iff _ _).2
    exact ⟨Finset.univ, 1, zero_lt_one, by simp⟩

Goal state after:
case refine_2
𝕜 : 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 : WithSeminorms fun x ↦ p
⊢ IsVonNBounded 𝕜 (p.ball 0 1)

case refine_3
𝕜 : 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
⊢ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) → WithSeminorms fun x ↦ p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
        Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE

Tactic:
tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
⊢ [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ p, Continuous[inst✝².toTopologicalSpace, _] ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p,
      BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧
        Continuous[inst✝².toTopologicalSpace, _] (⨆ k, ⇑((q i).comp (f k)))].TFAE
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 σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ 𝓤 (E →SL[σ₁₂] F) = ⨅ r, ⨅ (_ : r > 0), 𝓟 {f | ‖f.1 - f.2‖ < r}

Tactic:
refine ContinuousLinearMap.seminorm (σ₁₂ := σ₁₂) (E := E) (F := F) |>.uniformity_eq_of_hasBasis
    (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_

Goal state after:
case refine_1
𝕜 : 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 σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ ∃ r, ContinuousLinearMap.seminorm.closedBall 0 r ∈ 𝓝 0

case refine_2
𝕜 : 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 σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set E × ℝ
s : Set E
r : ℝ
x✝ : IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
⊢ ∃ r_1 > 0, ContinuousLinearMap.seminorm.ball 0 r_1 ⊆ {f | ∀ x ∈ (s, r).1, f x ∈ closedBall 0 (s, r).2}
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l✝ : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (a b : α → β), a ≈ b → (∃ b, a =ᶠ[l] fun x ↦ b) = ∃ b_1, b =ᶠ[l] fun x ↦ b_1

Tactic:
suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l✝ : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun x ↦ b) → g =ᶠ[l] fun x ↦ b
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst✝¹] f → IsOpen (f ⁻¹' s)
⊢ ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)

Tactic:
intro K hK

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous[_, inst✝¹] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsOpen[inst✝] A
⊢ ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)

Tactic:
intro K hK

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsOpen[inst✝] A
K : Set X
hK : IsCompact K
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
Module: Mathlib.Topology.UniformSpace.CompactConvergence

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

Tactic:
intro K hK

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ u * v ≤ᶠ[f] fun x ↦ limsup u f * v x

Tactic:
filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : (univ.pi fun i ↦ s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i ↦ s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C

Tactic:
univ_pi_nonempty_iff

Goal state after:
ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
s₁ : (i : ι) → Set (α i)
hs₁ : s₁ ∈ univ.pi C
s₂ : (i : ι) → Set (α i)
hs₂ : s₂ ∈ univ.pi C
hst : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty
⊢ (univ.pi fun i ↦ s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝

Tactic:
exact le_inf haf hag

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)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
f : (i : ι) → Set (α i)
s : Finset ι
⊢ (Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)

Tactic:
by
  classical simp [← Set.univ_pi_ite, pi_pi, apply_ite]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
⊢ Measure.pi μ = dirac x

Tactic:
refine pi_eq fun s _ => ?_

Goal state after:
α : Type u_4
inst✝¹ : Fintype α
inst✝ : IsEmpty α
β : α → Type u_5
m : (a : α) → MeasurableSpace (β a)
μ : (a : α) → Measure (β a)
x : (a : α) → β a
this : ∀ (a : α), SigmaFinite (μ a)
s : (i : α) → Set (β i)
x✝ : ∀ (i : α), MeasurableSet (s i)
⊢ (dirac x) (univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal

Tactic:
rw [← ENNReal.rpow_one (ε * μ { x | ε ≤ ‖f x‖ₑ ^ p.toReal }), ← this, ENNReal.rpow_mul]

Goal state after:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ ((ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal)) ^ p.toReal ≤ eLpNorm f p μ ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun x ↦ ‖s.indicator f x‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ) (μ.restrict s)

Tactic:
enorm_indicator_eq_indicator_enorm,

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ essSup (fun x ↦ s.indicator (fun a ↦ ‖f a‖ₑ) x) μ = essSup (fun a ↦ ‖f a‖ₑ) (μ.restrict s)
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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
⊢ ∀ ⦃K : Set ((i : ι) → α i)⦄, IsCompact K → (Measure.pi μ) K < ∞

Tactic:
intro K hK

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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
⊢ (Measure.pi μ) K < ∞
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 : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)
K : Set ((i : ι) → α i)
hK : IsCompact K
this : (Measure.pi μ) (univ.pi fun j ↦ eval j '' K) < ∞
⊢ (Measure.pi μ) K < ∞

Tactic:
by
    exact lt_of_le_of_lt (measure_mono (univ.subset_pi_eval_image K)) this

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

Goal state before:
pp: case mpr
α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c

Tactic:
· rintro ⟨rfl, rfl⟩
    rw [mul_zero]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
⊢ y⁻¹ < (log y - log x) / (y - x)

Tactic:
have h : 0 < y - x := by linarith

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < y - x
⊢ y⁻¹ < (log y - log x) / (y - x)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case 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
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
have hs4 : 1 + p * s ≠ 1 := by
    contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'

Goal state after:
case 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
⊢ 1 + p * s < (1 + s) ^ p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : 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 = ∞
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q

Tactic:
eLpNorm_eq_eLpNorm' _ (by finiteness)

Goal state after:
case neg
α : 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 = ∞
⊢ eLpNorm' (fun x ↦ ‖f x‖ₑ ^ q) p.toReal μ = eLpNorm' f (p * ENNReal.ofReal q).toReal μ ^ q

α : 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 = ∞
⊢ p * ENNReal.ofReal q ≠ 0