mathlib-initiative/mathlib-tactics huggingface dataset:
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.reindex e).points) w ∈ Simplex.setInterior I s

Tactic:
simp_rw [reindex]

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 ∘ ⇑e.symm)) w ∈ Simplex.setInterior I s
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
⊢ ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X ⊆ stdSimplex S Y

Tactic:
rintro _ ⟨s, ⟨hs₀, hs₁⟩, rfl⟩
  refine ⟨fun y ↦ ?_, ?_⟩
  · rw [FunOnFinite.linearMap_apply_apply]
    exact Finset.sum_nonneg (by aesop)
  · simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]
    exact Finset.sum_fiberwise Finset.univ f s

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

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x ↦ if hx : x ∈ t then f x hx else 0) e • e = 0

pp: case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x ↦ if hx : x ∈ t then f x hx else 0) e = 0

Tactic:
on_goal 1 =>
      suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by
        convert! this
        rename V => x
        by_cases hx : x ∈ t <;> simp [hx]

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
⊢ (∑ e ∈ t, if hx : e ∈ t then f e hx • e else 0) = 0

case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
t : Finset V
w : ↥t → k
hw : ∑ i, w i = 0
i : ↥t
hi : ¬w i = 0
hwt : ∑ x, w x • ↑x = 0
f : (x : V) → x ∈ t → k := fun x hx ↦ w ⟨x, hx⟩
⊢ ∑ e ∈ t, (fun x ↦ if hx : x ∈ t then f x hx else 0) e = 0
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
W : Type u_4
Q : Type u_5
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : AddTorsor W Q
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : IsTopologicalAddTorsor Q
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : Module R W
inst✝ : ContinuousSMul R W
x : Q
s t : Set Q
ht : t.Finite
h : t ⊆ interior s
this : ∀ y ∈ t, ∀ᶠ (δ : R) in 𝓝 1, (homothety x δ) y ∈ s
⊢ ∀ᶠ (δ : R) in 𝓝 1, ⇑(homothety x δ) '' t ⊆ s

Tactic:
by
    simp_rw [Set.image_subset_iff]
    exact (Filter.eventually_all_finite ht).mpr this

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ IsOpenMap ⇑(homothety x t)

Tactic:
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)

Goal state after:
case l_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)

case r_inv
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : AddTorsor V P
inst✝⁴ : TopologicalSpace P
inst✝³ : IsTopologicalAddTorsor P
inst✝² : Field R
inst✝¹ : Module R V
inst✝ : ContinuousConstSMul R V
x : P
t : R
ht : t ≠ 0
⊢ Function.RightInverse ⇑(homothety x t) ⇑(homothety x t⁻¹)
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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0

Tactic:
intro v

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
h : AffineIndependent k fun p ↦ ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
v : V
⊢ v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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 : Set P
p₁ : P
h : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k ⇑bsv
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
have hsvt := bsv.span_eq

Goal state after:
case inr
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 : Set P
p₁ : P
h : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k ⇑bsv
hsvt : Submodule.span k (Set.range ⇑bsv) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
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 : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
⊢ ∀ v ∈ h.extend ⋯, v ≠ 0

Tactic:
intro v

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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
v : V
⊢ v ∈ h.extend ⋯ → v ≠ 0
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 ↔ y ∈ connectedComponent x

Tactic:
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.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)
⊢ IsEmpty ((i : ι) → Z i) ∨ (∀ (i : ι), LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite

Tactic:
refine .inr ⟨fun i ↦ ((isOpenMap_eval i).isQuotientMap (continuous_apply i)
      (surjective_eval i)).locallyPathConnectedSpace, ?_⟩

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)
⊢ {i | ¬PathConnectedSpace (Z i)}.Finite
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
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ {x | x ≠ 2} ⊆ ![p₁, p₂, p₃] ⁻¹' ↑s

Tactic:
Set.subset_def,

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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ x ∈ {x | x ≠ 2}, x ∈ ![p₁, p₂, p₃] ⁻¹' ↑s
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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)

Tactic:
by
  simpa only [centerMass, h₁, inv_one, one_smul] using!
    hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t₁ t₂ : Finset E
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂ ⊆ (convexHull R) (↑t₁ ⊓ ↑t₂)

Tactic:
Set.subset_def,

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t₁ t₂ : Finset E
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ ∀ x ∈ (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂, x ∈ (convexHull R) (↑t₁ ⊓ ↑t₂)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
exact AddGroupFilterBasis.nhds_zero_hasBasis _

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0

Tactic:
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r) ↔ ∀ (i : ι), ∃ x, ∀ y ∈ ⇑(p i) '' s, y ≤ x

Tactic:
forall_mem_image

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r) ↔ ∀ (i : ι), ∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range ⇑f
⊢ ball 0 r ⊆ ↑(↑f).range

Tactic:
Set.subset_def,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ∀ x_1 ∈ ball x r, x_1 ∈ Set.range ⇑f
⊢ ∀ x ∈ ball 0 r, x ∈ ↑(↑f).range
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case neg
𝕜 : 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 σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
rw [← inv_inv c, norm_inv, inv_lt_one₀ (norm_pos_iff.2 <| inv_ne_zero h0)] at hc
    refine opNorm_le_of_shell ε_pos hC hc ?_
    rwa [norm_inv, div_eq_mul_inv, inv_inv]

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

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
have hnhds : s ∈ 𝓝[K] x := inter_mem_nhdsWithin _ <| f.continuousAt _ (ball_mem_nhds _ hW)

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f

Tactic:
conv_rhs => rw [← Quotient.out_eq' f]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
g : β →ₘ[ν] γ
⊢ g.compQuasiMeasurePreserving id ⋯ = g

Tactic:
by
  ext
  exact coeFn_compQuasiMeasurePreserving _ _

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

Goal state before:
pp: case cons
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod
⊢ (Measure.tprod (a :: l) μ) (Set.tprod (a :: l) s) = (List.map (fun i ↦ (μ i) (s i)) (a :: l)).prod

Tactic:
| cons a l ih =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by
  by_cases hp_zero : p = 0
  · simp only [hp_zero, eLpNorm_exponent_zero]
  by_cases hp_top : p = ∞
  · simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm,
       enorm_indicator_eq_indicator_enorm, ENNReal.essSup_indicator_eq_essSup_restrict hs]
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top]
  rw [← lintegral_indicator hs]
  congr
  simp_rw [enorm_indicator_eq_indicator_enorm]
  rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
    Function.comp_def]
  simp [ENNReal.toReal_pos hp_zero hp_top]

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)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NullSingletonClass (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i ↦ Iio (f i)) =ᵐ[Measure.pi μ] Iic f

Tactic:
rw [← pi_univ_Iic]; exact pi_Iio_ae_eq_pi_Iic

Goal state after:
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
⊢ (Measure.pi μ).IsInvInvariant

Tactic:
refine ⟨(Measure.pi_eq fun s hs => ?_).symm⟩

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)
⊢ (Measure.pi μ).inv (univ.pi s) = ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
hq0 : 0 ≤ q
⊢ eLpNorm' 0 q μ = 0

Tactic:
exact eLpNorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
      ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i))) =
    Measure.pi μ

Tactic:
refine (pi_eq fun s _ => ?_).symm
    simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
      Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
      Fintype.prod_sum_type]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : p = 0
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
· simp [h₀]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ ⇑(MeasurableEquiv.arrowCongr' eα eβ) = ⇑(MeasurableEquiv.piCongrLeft (fun i ↦ β₂) eα) ∘ fun a i ↦ eβ (a i)

Tactic:
simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
    comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
    Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]

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

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 - p * y ^ (p - 1) * (y - x) / y ^ p < (x / y + 1 - 1) ^ p

Tactic:
add_comm,

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 1 - p * y ^ (p - 1) * (y - x) / y ^ p < (1 + x / y - 1) ^ p
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr.inl
p : ℝ≥0∞
hp : p ≠ ∞
h : p.HolderConjugate ∞
⊢ p * ∞ = p + ∞

Tactic:
simp [ne_zero p ∞]

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

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ∞

Tactic:
exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

Goal state after: