mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (s ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

Tactic:
· exact hasFiniteIntegral_mkD_restrict_of_bound f _ this f_zero bound bound_int bound_ge

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ e * t • a * e = t • e

Tactic:
apply inr_injective (R := ℂ) <| Eq.symm ?_

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
this : t • (↑e * (1 - ↑a) * ↑e) = 0
⊢ ↑(t • e) = ↑(e * t • a * e)
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖

Tactic:
adjoint_toContinuousLinearMap

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖ContinuousLinearMap.adjoint
        (toContinuousLinearMap
          ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case refine_1
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
⊢ ‖toEuclideanCLM (diagonal v)‖ ≤ ‖v‖

Tactic:
refine T.opNorm_le_bound (norm_nonneg _) fun x ↦ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
⊢ ‖T x‖ ≤ ‖v‖ * ‖x‖
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case h₁.hs
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
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ proj ⁻¹' e.baseSet = e'.source

Tactic:
e'.source_eq,

Goal state after:
case h₁.hs
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
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ proj ⁻¹' e.baseSet = proj ⁻¹' e'.baseSet
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 : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e.toPartialEquiv (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1

Tactic:
e.right_inv hx

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = x.1
⊢ proj (↑e.symm x) = x.1
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.source ∩ ↑e.symm ⁻¹' e'.source = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
e'.source_eq,

Goal state after:
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.source ∩ ↑e.symm ⁻¹' proj ⁻¹' e'.baseSet = (e.baseSet ∩ e'.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inr.hi
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp' : p ∈ proj ⁻¹' e'.baseSet
⊢ p ∉ proj ⁻¹' e.baseSet

Tactic:
exact fun h => H.le_bot ⟨h, hp'⟩

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
inst✝² : TopologicalSpace Z
T : Trivialization F proj
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : LocallyCompactPair ι ↑T.baseSet
γ : C(ι, ↑T.baseSet)
i : ι
e : ↑T.source
h : proj ↑e = ↑(γ i)
⊢ (T.clift (e, γ)) i = e

Tactic:
by
  have : proj e ∈ T.baseSet := by simp [h]
  simp [clift, liftCM, ← h, lift_self, this]

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
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖

Tactic:
have h1 : ∀ b, ‖a.fst b‖₊ ^ 2 ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ := by
    intro b
    calc
      ‖a.fst b‖₊ ^ 2 = ‖star (a.fst b) * a.fst b‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_star_mul_self.symm
      _ ≤ ‖a.snd (star (a.fst b))‖₊ * ‖b‖₊ := (a.central (star (a.fst b)) b ▸ nnnorm_mul_le _ _)
      _ ≤ ‖a.snd‖₊ * ‖a.fst b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.fst b) ▸ mul_le_mul_left (a.snd.le_opNNNorm _) _

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
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
⊢ ‖a.toProd.1‖ = ‖a.toProd.2‖
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
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.2‖ = ‖a‖

Tactic:
rw [← norm_fst, norm_fst_eq_snd]

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
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : f e₁ ∈ hf.toTrivialization.baseSet
he₂ : f e₂ ∈ hf.toTrivialization.baseSet
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
rw [← t.mem_source] at he₁ he₂

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n ↦ (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f
⊢ ∑' (i : ℕ), ((↑i.factorial)⁻¹ • f ^ i) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
simp [NormedSpace.exp_eq_tsum 𝕜]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) ≤ ‖cfc (fun x ↦ x - 1 x) u‖

Tactic:
convert! norm_apply_le_norm_cfc (fun z ↦ z - 1) u hz

Goal state after:
case e'_3
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
z : ℂ
hz : z ∈ spectrum ℂ u
this : ‖z‖ = 1
⊢ √(2 * (1 - z.re)) = ‖z - 1‖
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Goal state after:
case inl
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Subsingleton A
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)

case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
⊢ ‖u - 1‖ ^ 2 = 2 * (1 - x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * (x + T)) = Circle.exp (2 * π / T * x)

Tactic:
mul_add

Goal state after:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * x + 2 * π / T * T) = Circle.exp (2 * π / T * x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦
    ⇑exp '' {x | -(π / 2 ^ (n + 1)) < x ∧ x < π / 2 ^ (n + 1)}

Tactic:
Set.Ioo_def,

Goal state after:
⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ ⇑exp '' Ioo (-(π / 2 ^ (n + 1))) (π / 2 ^ (n + 1))
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Goal state after:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Subsingleton A
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

case inr
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : ↥(selfAdjoint A)
ha_norm : ‖a‖ ≤ 1
⊢ star ↑(unitarySelfAddISMul a ha_norm) = ↑a - I • CFC.sqrt (1 - ↑a ^ 2)

Tactic:
simp [IsSelfAdjoint.star_eq, ← sub_eq_add_neg, (CFC.sqrt_nonneg (1 - a ^ 2 : A)).isSelfAdjoint]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : v ∈ closedBall 1 √ε
z : ℂ
hz : z ∈ spectrum ℂ ↑v
⊢ 2 * (1 - z.re) ≤ ‖↑v - 1‖ ^ 2

Tactic:
exact two_mul_one_sub_le_norm_sub_one_sq v.2 hz

Goal state after:
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
⊢ g.conjStarAlgEquiv = f.conjStarAlgEquiv ↔ ∃ α, f = α • g

Tactic:
StarAlgEquiv.ext_iff,

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
⊢ (∀ (a : H →L[𝕜] H), g.conjStarAlgEquiv a = f.conjStarAlgEquiv a) ↔ ∃ α, f = α • g
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
⊢ ↑(↑g).symm ∘SL ↑↑f ∈ Set.range ⇑(algebraMap 𝕜 (H →L[𝕜] H)) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
Set.mem_range,

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
⊢ (∃ y, (algebraMap 𝕜 (H →L[𝕜] H)) y = ↑(↑g).symm ∘SL ↑↑f) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
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
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y = 0
x : H
⊢ ?m.170

Tactic:
simpa [hy] using congr($h x).symm

Goal state after:
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
x✝¹ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
x✝ : H
⊢ ↑↑f x✝ = (y • ↑↑g) x✝

Tactic:
simpa using congr(g ($h _)).symm

Goal state after:
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
u : H ≃ₗᵢ[𝕜] H
⊢ (conjStarAlgAut 𝕜 (H →L[𝕜] H)) (linearIsometryEquiv.symm u) = u.conjStarAlgEquiv

Tactic:
simp [← conjStarAlgEquiv_unitaryLinearIsometryEquiv]

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

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)
⊢ #s < #t

Tactic:
have finrank_lt := add_lt_add_left (Submodule.finrank_lt_finrank_of_lt dir_lt) 1

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)
finrank_lt :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s < #t
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' * x⁻¹) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
integral_inv_eq_self (fun x => f (x' * x)) μ,

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' * x) ∂μ = ∫ (x : G), f x ∂μ
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 ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) x.1 x.2 =
    -f x.1.1 x.2 + f x.1.2 x.2

Tactic:
by simp; abel

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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝² : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝¹ : l.NeBot
hr : 0 < r
this✝ :
  TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
this :
  TendstoUniformlyOn ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
n : ι × ι
z : E
a✝ : z ∈ Metric.ball x r
⊢ ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) n z =
    (fun z ↦ -f n.1 z + f n.2 z) z

Tactic:
by simp; abel

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

Goal state before:
pp: case h₂
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i ↦ ‖g a₀ i‖)
i : ι
⊢ |g a₀ i| ≤ M

Tactic:
exact hM ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inl
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x] fun x ↦ 0

Tactic:
filter_upwards [gt_mem_nhds hx] with y hy

Goal state after:
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
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
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ⋆[L, μ] g)

Tactic:
rw [← continuousOn_univ]
  let g' : G → G → E' := fun _ q => g q
  have : ContinuousOn ↿g' (univ ×ˢ univ) := (hg.comp continuous_snd).continuousOn
  exact continuousOn_convolution_right_with_param_comp L
    (continuousOn_univ.2 continuous_id) hcg
    (fun p x _ hx => image_eq_zero_of_notMem_tsupport hx) hf this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ Integrable (fun x ↦ g (S • x)) μ

Tactic:
refine (integrable_map_equiv t g).mp (?_ : Integrable g (map (S • ·) μ))

Goal state after:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ Integrable g (Measure.map (fun x ↦ S • x) μ)
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
⊢ ∃ f, IsInducing f

Tactic:
let s : Set (Set X × Set X) := { UV ∈ B ×ˢ B | closure UV.1 ⊆ UV.2 }

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
⊢ ∃ f, IsInducing f