mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∀ ⦃x : Z.TotalSpace⦄,
    x ∈ Z.proj ⁻¹' Z.baseSet i →
      { proj := (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1,
          snd :=
            Z.coordChange i (Z.indexAt (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1)
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).2 } =
        x

Tactic:
rintro ⟨x, v⟩ hx

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : { proj := x, snd := v } ∈ Z.proj ⁻¹' Z.baseSet i
⊢ {
      proj :=
        ({ proj := x, snd := v }.proj,
            Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
              { proj := x, snd := v }.snd).1,
      snd :=
        Z.coordChange i
          (Z.indexAt
            ({ proj := x, snd := v }.proj,
                Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                  { proj := x, snd := v }.snd).1)
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).1
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).2 } =
    { proj := x, snd := v }
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ Z.baseSet i ×ˢ univ →
      ({ proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj,
          Z.coordChange (Z.indexAt { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj) i
            { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.proj
            { proj := x.1, snd := Z.coordChange i (Z.indexAt x.1) x.1 x.2 }.snd) =
        x

Tactic:
rintro ⟨x, v⟩ hx

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : (x, v) ∈ Z.baseSet i ×ˢ univ
⊢ ({ proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj,
      Z.coordChange (Z.indexAt { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj)
        i { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj
        { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.snd) =
    (x, v)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j))) (↑(Z.trivChange i j).toPartialEquiv)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source

Tactic:
rintro ⟨x, v⟩ hx

Goal state after:
case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
⊢ ↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) (x, v) =
    ↑(Z.trivChange i j).toPartialEquiv (x, v)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ ↑f ⁻¹' s)
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      (↑(Z.localTrivAsPartialEquiv i).symm ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        ↑(Z.localTrivAsPartialEquiv i).symm ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s) =
    e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e' ∘ ↑e.symm ⁻¹' s

Tactic:
← preimage_comp,

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ ↑f ⁻¹' s)
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      (↑(Z.localTrivAsPartialEquiv i).symm ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        ↑(Z.localTrivAsPartialEquiv j) ∘ ↑(Z.localTrivAsPartialEquiv i).symm ⁻¹' s) =
    e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e' ∘ ↑e.symm ⁻¹' s
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ Z.baseSet (Z.indexAt b)

Tactic:
exact Z.mem_baseSet_at b

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
constructor <;> intro h x

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ Set.InjOn f U
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝¹ : TopologicalSpace G := ⊥
this✝ : DiscreteTopology G
this : ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t, x ∈ t.baseSet
⊢ IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})

Tactic:
by
    choose t ht using this; exact IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
t : Set E
x : X
e : E
he : e ∈ t
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
htx : t ⊆ ↑φ ⁻¹' {x}
hf : ∀ e ∈ t, ∃ φ_1, e ∈ φ_1.source ∧ ↑φ_1 = ↑φ
⊢ ∃ u, IsOpen[inst✝¹] u ∧ u ∩ t = {e}

Tactic:
exact ⟨_, φ.open_source, subset_antisymm (fun e' he' ↦ φ.injOn he'.1 hφ <|
      (htx he'.2).trans (htx he).symm) <| Set.singleton_subset_iff.mpr ⟨hφ, he⟩⟩

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝¹ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
e : ↑(f ⁻¹' {x})
⊢ IsOpen[inst✝¹] (f '' V' e)

Tactic:
convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝¹ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
e : ↑(f ⁻¹' {x})
a✝¹ : E
a✝ : a✝¹ ∈ V' e
⊢ ↑(φ e) = f
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_2
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ (⇑e ⁻¹' ↑(zpowGroupHom n).ker).Finite

Tactic:
convert! finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]
    ext
    simp [e, homeomorphCircle_apply, ← toCircle_zsmul, ← (injective_toCircle one_ne_zero).eq_iff]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T U : E →L[𝕜] E
hT : (↑T).IsSymmetric
hU : (↑U).IsSymmetric
h : (↑U).ker ≤ (↑T).ker
this : CompleteSpace E
⊢ (↑T).range ≤ (↑U).range

Tactic:
simpa [orthogonal_ker, hT, hU] using Submodule.orthogonal_le h

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k fun x ↦ ↑x
hc' : #(Finset.image p s) = n + 1
⊢ (Finset.image p s).Nonempty

Tactic:
simp [hc', ← Finset.card_pos]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑↑(Finset.image (fun p ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ #(Finset.image (fun x ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n

Tactic:
rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑↑(Finset.image (fun p ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ #(Finset.image p s) - 1 = n
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
m : ℕ
inst✝¹ : NeZero m
s : Simplex k P m
inst✝ : NeZero m
e : Fin (m + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
⊢ ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ ⇑e.symm) i

Tactic:
exact centroid_eq_of_range_eq <| Affine.Simplex.range_faceOpposite_reindex s e i

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

Goal state before:
pp: case h
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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ r, p_1 = r • v +ᵥ p
p₂ : P
⊢ p₂ ∈ s → ∃ r, p₂ = r • v +ᵥ p₁

Tactic:
hp₂

Goal state after:
case h
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
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ p_1 ∈ s, ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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
h : p₁ ∈ line[k, p₂, p₃]
⊢ Collinear k {p₁, p₂, p₃}

Tactic:
rw [collinear_insert_iff_of_mem_affineSpan h]
  exact collinear_pair _ _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i ↦ ‖f i‖ ^ p.toReal

Tactic:
ENNReal.toReal_pos_iff

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i ↦ ‖f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp g ∞
⊢ Memℓp f ∞

Tactic:
memℓp_infty_iff

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : BddAbove (Set.range fun i ↦ ‖g i‖)
⊢ BddAbove (Set.range fun i ↦ ‖f i‖)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 ↦ ↥(lp E x) → ℝ) (fun f ↦ ↑⋯.toFinset.card) ⋯ f
    else if p = ∞ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
ENNReal.toReal_pos_iff

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 ↦ ↥(lp E x) → ℝ) (fun f ↦ ↑⋯.toFinset.card) ⋯ f
    else if p = ∞ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ Memℓp (f * g) ∞

Tactic:
memℓp_infty_iff

Goal state after:
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ BddAbove (Set.range fun i ↦ ‖(f * g) i‖)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
⊢ LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a ↦ ↑(f a) i

Tactic:
simp_rw [← lipschitzOnWith_univ]
  apply LipschitzOnWith.coordinate

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
⊢ x ∈ t

Tactic:
exact A y (ε / 2) yt (B.trans hε) (Metric.mem_ball.2 hxy)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ ↑n ↑(univBall c r)

Tactic:
unfold univBall; split_ifs with h
  · exact (contDiff_unitBallBall h).comp contDiff_univUnitBall
  · exact contDiff_id.add contDiff_const

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
⊢ support (f ⋆[L, μ] g) ⊆ support g + support f

Tactic:
intro x h2x
  by_contra hx
  apply h2x
  simp_rw [Set.mem_add, ← exists_and_left, not_exists, not_and_or, notMem_support] at hx
  rw [convolution_def]
  convert! integral_zero G F using 2
  ext t
  rcases hx (x - t) t with (h | h | h)
  · rw [h, (L _).map_zero]
  · rw [h, L.map_zero₂]
  · exact (h <| sub_add_cancel x t).elim

Goal state after:
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a‖ + ‖x - x₀‖⁻¹ * ‖(F' a) (x - x₀)‖ ≤
    ‖x - x₀‖⁻¹ * (b a * ‖x - x₀‖) + ‖x - x₀‖⁻¹ * (‖F' a‖ * ‖x - x₀‖)

Tactic:
by
        gcongr; exact (F' a).le_opNorm _

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ pa,
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
⊢ ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε

Tactic:
obtain ⟨p, hp, δ, hδ, hgδ⟩ := hcg _ h2ε

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ pa,
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (uncurry g (i, x)) z₀ < ε / 3
⊢ ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (f.normed μ)) = closedBall c f.rOut

Tactic:
f.support_normed_eq,

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut