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

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
⊢ Icc a a ⊆ ea.baseSet

Tactic:
simp [hea]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)
⊢ x ∈ Set.range toProd → x ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProd ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
by
  rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag]
  exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
⊢ x ∈ Set.range toProdMulOpposite → x ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProdMulOpposite ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}
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_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Multiplicative G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1

Tactic:
obtain ⟨U, hU, hU'⟩ := hf.disjoint e

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e : E
U : Set E
hU : U ∈ 𝓝 e
hU' : ∀ (g : G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Multiplicative G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
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_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Additive G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0

Tactic:
obtain ⟨U, hU, hU'⟩ := hf.disjoint e

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
U : Set E
hU : U ∈ 𝓝 e
hU' : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Additive G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0
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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
⊢ Trivialization ι f

Tactic:
Set.subset_def,

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
surj : ∀ (i : ι), Set.SurjOn f (U i) V
disjoint : Pairwise (Disjoint on U)
exhaustive : ∀ x ∈ f ⁻¹' V, x ∈ ⋃ i, U i
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
⊢ Trivialization ι f
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T

Tactic:
AddSubgroup.mem_zmultiples_iff,

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, k • T = -z✝¹ + z✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
y : F
x : E
⊢ 0 ∈ lowerBounds (Set.range fun w ↦ ‖y - ↑w‖)

Tactic:
rintro - ⟨_, rfl⟩; positivity

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
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖

Tactic:
have := star_eq_adjoint T ▸ toLinearMap_sub (star _ * T) _ ▸
    ((IsSelfAdjoint.star_mul_self T).sub (IsSelfAdjoint.mul_star_self T)).isSymmetric

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
⊢ s.centroid -ᵥ p = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ p)

Tactic:
by
  rw [centroid_vsub_const _ _ (by simp), centroid_def, affineCombination_eq_linear_combination
    (hw := sum_centroidWeights_eq_one_of_nonempty _ _ (by simp))]
  simp [smul_sum]

Goal state after:
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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ Finset.centroid k univ (⇑f ∘ s.points) = f ((affineCombination k univ s.points) (centroidWeights k univ))

Tactic:
Finset.map_affineCombination

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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ Finset.centroid k univ (⇑f ∘ s.points) = (affineCombination k univ (⇑f ∘ s.points)) (centroidWeights k univ)

case hw
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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ univ.sum (centroidWeights k univ) = 1
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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ ↑(s.restrict S hS).centroid = s.centroid

Tactic:
eq_comm

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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ s.centroid = ↑(s.restrict S hS).centroid
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
| f.conjStarAlgEquiv = g.conjStarAlgEquiv

Tactic:
eq_comm

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
| g.conjStarAlgEquiv = f.conjStarAlgEquiv
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
inst✝⁴ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
i : Fin (n + 1)
⊢ (affineCombination k univ (⇑f ∘ (s.faceOpposite i).points)) (centroidWeights k univ) =
    f ((affineCombination k univ (s.faceOpposite i).points) (centroidWeights k univ))

Tactic:
Finset.map_affineCombination

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
inst✝⁴ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
i : Fin (n + 1)
⊢ (affineCombination k univ (⇑f ∘ (s.faceOpposite i).points)) (centroidWeights k univ) =
    (affineCombination k univ (⇑f ∘ (s.faceOpposite i).points)) (centroidWeights k univ)

case hw
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
inst✝⁴ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
i : Fin (n + 1)
⊢ univ.sum (centroidWeights k univ) = 1
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : 1 = (starRingEnd 𝕜) y * y ∨ ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
eq_comm

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : (starRingEnd 𝕜) y * y = 1 ∨ ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x
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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ ↑((s.restrict S hS).faceOppositeCentroid i) = s.faceOppositeCentroid i

Tactic:
eq_comm

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i = ↑((s.restrict S hS).faceOppositeCentroid i)
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
⊢ (range fun p ↦ (lineMap q ↑p) ↑(w p)) ⊆ u

Tactic:
rintro y ⟨⟨p, hp⟩, rfl⟩

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ t
⊢ (fun p ↦ (lineMap q ↑p) ↑(w p)) ⟨p, hp⟩ ∈ u
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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ vectorSpan k (Set.range s.medial.points) = vectorSpan k (Set.range s.points)

Tactic:
vectorSpan_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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
⊢ Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points) =
    Submodule.span k (Set.range s.points -ᵥ Set.range s.points)
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
⊢ ↑f x = 0

Tactic:
← notMem_support,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : f.rOut ≤ dist x c
⊢ x ∉ support ↑f
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Integrable (fun t ↦ f (g / t)) μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.comp_div_left g⟩
  convert! h.comp_inv.comp_mul_left g⁻¹
  simp_rw [div_inv_eq_mul, mul_inv_cancel_left]

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
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)

Tactic:
by
    have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    apply this.congr (.of_forall (fun x ↦ by simp; abel))

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)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter, dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε

Tactic:
refine (this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ (x : Finset α),
    dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal → dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1
𝕜 : 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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
x✝ : t ∈ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * C

pp: case refine_2
𝕜 : 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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ 0

Tactic:
· apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]

Goal state after:
case refine_2
𝕜 : 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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ 0
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1.hy
𝕜 : 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✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun t ↦ -t + x₀) ⁻¹' s
hbg : BddAbove ((fun i ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
⊢ t - x₀ + x₀ ∈ s

Tactic:
sub_add_cancel

Goal state after:
case refine_1.hy
𝕜 : 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✝² : AddGroup G
inst✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
s' : Set G := (fun t ↦ -t + x₀) ⁻¹' s
hbg : BddAbove ((fun i ↦ ‖g i‖) '' s')
t : G
ht : t ∈ s
⊢ t ∈ s
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

pp: case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
· exact convolution_mono_right H hfg' hf hg

Goal state after:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x