mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)

Tactic:
exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
exact isVonNBounded_iff _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y ∈ interior s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> simp

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y

Tactic:
rw [openSegment_eq_image']

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ (fun θ ↦ x + θ • (y - x)) '' Ioo 0 1
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_1
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun x ≤ q x

Tactic:
exact fun j => hq (mem_image_of_mem _ j.2) _

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_2
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun y ≤ q y

Tactic:
exact fun j => hq (mem_image_of_mem _ j.2) _

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

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
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
p : ι → P
⊢ centroid k (map e s₂) p = centroid k s₂ (p ∘ ⇑e)

Tactic:
simp [centroid_def, affineCombination_map, centroidWeights]

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

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
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂

Tactic:
classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
⊢ x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r

Tactic:
let := AddGroupSeminorm.toSeminormedAddCommGroup p.toAddGroupSeminorm
  simp [closedBall_eq_metric]

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

Goal state before:
pp: ι : 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✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1, ∑ i, w_1 i = 1 ∧ (Finset.affineCombination k s p) w = (Finset.affineCombination k Finset.univ p) w_1

Tactic:
refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩

Goal state after:
ι : 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✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i, (↑s).indicator w i = 1
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (p.closedBall x r)

Tactic:
rw [closedBall_eq_biInter_ball]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mpr
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✝ : Fintype ι
p : ι → P
⊢ (∀ (w1 w2 : ι → k),
      ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2) →
    ∀ (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

Tactic:
intro h s1 s2 w1 w2 hw1 hw2 hweq

Goal state after:
case mpr
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✝ : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    ∑ i, w1 i = 1 → ∑ i, w2 i = 1 → (affineCombination k univ p) w1 = (affineCombination k univ p) w2 → w1 = w2
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1, w1 i = 1
hw2 : ∑ i ∈ s2, w2 i = 1
hweq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
⊢ (↑s1).indicator w1 = (↑s2).indicator w2
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective ⇑f
⊢ AffineIndependent k (⇑f ∘ p)

Tactic:
rcases isEmpty_or_nonempty ι with h | h
  · apply affineIndependent_of_subsingleton
  obtain ⟨i⟩ := h
  rw [affineIndependent_iff_linearIndependent_vsub k p i] at hai
  simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub]
  have hf' : LinearMap.ker f.linear = ⊥ := by rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
  exact LinearIndependent.map' hai f.linear hf'

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

Goal state before:
pp: case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹

Tactic:
div_mul_eq_mul_div,

Goal state after:
case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹ / (w i + ∑ i ∈ t, w i)
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:
rw [hw, Affine.Simplex.affineCombination_mem_setInterior_iff hw1, Simplex.map_points,
      ← Finset.map_affineCombination _ _ _ hw1]

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
⊢ (∀ (i : Fin (n + 1)), w i ∈ I) ↔
    ∃ x ∈ Simplex.setInterior I s, f x = f ((affineCombination k univ s.points) fun i ↦ w i)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: r ε : ℝ
hε : 0 < ε
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)

Tactic:
ball_eq_Ioo,

Goal state after:
r ε : ℝ
hε : 0 < ε
⊢ Ioo (r - ε) (r + ε) = openSegment ℝ (r - ε) (r + ε)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: r ε : ℝ
hε : 0 < ε
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)

Tactic:
rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ (⋃ x ∈ s, nhdsKer {x}) ×ˢ ⋃ y ∈ t, nhdsKer {y} = nhdsKer s ×ˢ nhdsKer t

Tactic:
simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ (univ.pi fun i ↦ ⋃ x ∈ s i, nhdsKer {x}) = univ.pi fun i ↦ nhdsKer (s i)

Tactic:
simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst✝¹] s
⊢ IsOpen[coinduced f inst✝¹] (⋂₀ S)

Tactic:
rw [isOpen_coinduced, preimage_sInter]

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen[coinduced f inst✝¹] s
⊢ IsOpen[inst✝¹] (⋂ t ∈ S, f ⁻¹' t)
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
this : ∀ (i : ι), Nonempty (Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ pathComponent x
i : ι
hi : i ∈ {i | ¬PathConnectedSpace (Z i)}
hiJ : i ∉ J
z : Z i
x✝ : z ∈ univ
j : ι
hj : j ∈ J
⊢ update x i z j ∈ t j

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hj hiJ)]

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)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htV : J.pi t ⊆ pathComponent x
i : ι
hi : i ∈ {i | ¬PathConnectedSpace (Z i)}
hiJ : i ∉ J
z : Z i
x✝ : z ∈ univ
j : ι
hj : j ∈ J
⊢ x j ∈ t j
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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∀ y ∈ t₁, y ∈ t₂ → 0 ≤ w₁ y

Tactic:
exact fun y hy₁ _ ↦ h₁w₁ y hy₁

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

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ ≤ ‖smulRight c f‖ / ‖f‖ * ‖x‖

Tactic:
div_mul_eq_mul_div,

Goal state after:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ ≤ ‖smulRight c f‖ * ‖x‖ / ‖f‖
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
⊢ { toFun := fun x ↦ (algebraMap R A) 1, continuous_toFun := ⋯ } = 1

Tactic:
ext _

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 1, continuous_toFun := ⋯ } a✝ = 1 a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ * c₂), continuous_toFun := ⋯ } =
    { toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } *
      { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ }

Tactic:
ext _

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ * c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } *
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
⊢ { toFun := fun x ↦ (algebraMap R A) 0, continuous_toFun := ⋯ } = 0

Tactic:
ext _

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) 0, continuous_toFun := ⋯ } a✝ = 0 a✝
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } =
    { toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
      { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ }

Tactic:
ext _

Goal state after:
α : Type u_1
inst✝⁹ : TopologicalSpace α
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : IsTopologicalSemiring A
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
c₁ c₂ : R
a✝ : α
⊢ { toFun := fun x ↦ (algebraMap R A) (c₁ + c₂), continuous_toFun := ⋯ } a✝ =
    ({ toFun := fun x ↦ (algebraMap R A) c₁, continuous_toFun := ⋯ } +
        { toFun := fun x ↦ (algebraMap R A) c₂, continuous_toFun := ⋯ })
      a✝
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
by simpa [this] using hx

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

Goal state before:
pp: α : 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
this✝ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
x : ℝ
hx : x > r
this : 0 < x
⊢ ENNReal.ofReal x > ENNReal.ofReal r

Tactic:
by simpa [this] using hx

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

Goal state before:
pp: α : 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
⊢ (essSup f μ).toReal = essSup (fun a ↦ (f a).toReal) μ

Tactic:
obtain rfl | hμ := eq_zero_or_neZero μ

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

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) μ
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 : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ (Measure.pi μ) (univ.pi fun b ↦ Metric.ball (x b) r) = ∏ i, (μ i) (Metric.ball (x i) r)

Tactic:
pi_pi

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 < r
⊢ ∏ i, (μ i) (Metric.ball (x i) r) = ∏ i, (μ i) (Metric.ball (x i) r)
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 : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (univ.pi fun b ↦ Metric.closedBall (x b) r) = ∏ i, (μ i) (Metric.closedBall (x i) r)

Tactic:
pi_pi

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ ∏ i, (μ i) (Metric.closedBall (x i) r) = ∏ i, (μ i) (Metric.closedBall (x i) r)
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
⊢ Measure.pi μ = dirac x

Tactic:
have : ∀ a, SigmaFinite (μ a) := isEmptyElim
  refine pi_eq fun s _ => ?_
  rw [Fintype.prod_empty, dirac_apply_of_mem]
  exact isEmptyElim (α := α)

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 : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : (μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : (μ i) t = 0
⊢ (Measure.pi μ) (univ.pi (update (fun j ↦ univ) i t)) = 0

Tactic:
pi_pi

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
i : ι
s : Set (α i)
hs : (μ i) s = 0
t : Set (α i)
hst : s ⊆ t
left✝ : MeasurableSet t
hμt : (μ i) t = 0
⊢ ∏ i_1, (μ i_1) (update (fun j ↦ univ) i t i_1) = 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i
⊢ (Measure.pi μ) (univ.pi fun i ↦ f i ⁻¹' s i) = ∏ i, (map (f i) (μ i)) (s i)

Tactic:
pi_pi

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i
⊢ ∏ i, (μ i) (f i ⁻¹' s i) = ∏ i, (map (f i) (μ i)) (s i)