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

Goal state before:
pp: 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
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ cfcₙ (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
by
  have key₁ (z : quasispectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₃]
    refine integral_congr_ae ?_
    filter_upwards [hf₁, hf₂] with x cont_x zero_x
    rw [mkD_apply_of_continuousOn cont_x zero_x]
  have key₂ (z : quasispectrum 𝕜 a) :
      ∫ x, f x z ∂μ = mkD ((quasispectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
    rw [mkD_apply_of_continuousOn]
    · rw [continuousOn_iff_continuous_domRestrict]
      refine continuous_congr key₁ |>.mpr ?_
      exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
    · exact integral_eq_zero_of_ae hf₂
  simp_rw [cfcₙ_eq_cfcₙL_mkD _ a, cfcₙL_integral a _ hf₃ ha]
  congr
  ext z
  rw [← key₁, key₂]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, b i⟫ = ⟪y, b i⟫
⊢ x = y

Tactic:
by
  refine ext_inner_left_basis b fun i => ?_
  rw [← inner_conj_symm]
  conv_rhs => rw [← inner_conj_symm]
  exact congr_arg conj (h i)

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : ¬Yᗮ = ⊥
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
change Yᗮ ≠ ⊥ at htriv

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Yᗮ ≠ ⊥
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
refine ⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ = x
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ IsExtreme 𝕜 A {x} ↔ x ∈ extremePoints 𝕜 A

Tactic:
by
  simp [isExtreme_iff, extremePoints]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
⊢ extremePoints 𝕜 (s ×ˢ t) = extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t

Tactic:
ext ⟨x, y⟩
  refine (and_congr_right fun hx ↦ ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩).trans and_and_and_comm
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hx'⟩
    ext
    · exact h.1 hx₁.1 hx₂.1 ⟨a, b, ha, hb, hab, congrArg Prod.fst hx'⟩
    · exact h.2 hx₁.2 hx₂.2 ⟨a, b, ha, hb, hab, congrArg Prod.snd hx'⟩
  · rintro x₁ hx₁ x₂ hx₂ hx_fst
    refine congrArg Prod.fst (h (mk_mem_prod hx₁ hx.2) (mk_mem_prod hx₂ hx.2) ?_)
    rw [← Prod.image_mk_openSegment_left]
    exact mem_image_of_mem _ hx_fst
  · rintro x₁ hx₁ x₂ hx₂ hx_snd
    refine congrArg Prod.snd (h (mk_mem_prod hx.1 hx₁) (mk_mem_prod hx.1 hx₂) ?_)
    rw [← Prod.image_mk_openSegment_right]
    exact mem_image_of_mem _ hx_snd

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
⊢ ‖U i j‖ ≤ 1

Tactic:
have diag_eq_norm_sum : (U * Uᴴ) i i = (∑ x : n, ‖U i x‖ ^ 2 : ℝ) := by
    simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj]
    norm_cast

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
⊢ ‖U i j‖ ≤ 1
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x : ℝ
n : ℕ
⊢ exp (↑n * x) = exp x ^ n

Tactic:
← nsmul_eq_mul,

Goal state after:
x : ℝ
n : ℕ
⊢ exp (n • x) = exp x ^ n
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: e : AddChar ℝ Circle
x : ℝ
⊢ star ↑(e x) = ↑(e (-x))

Tactic:
have h := Circle.coe_inv_eq_conj ⟨e x, ?_⟩

Goal state after:
case refine_2
e : AddChar ℝ Circle
x : ℝ
h : ↑⟨↑(e x), ?refine_1⟩⁻¹ = (starRingEnd ℂ) ↑⟨↑(e x), ?refine_1⟩
⊢ star ↑(e x) = ↑(e (-x))

case refine_1
e : AddChar ℝ Circle
x : ℝ
⊢ ↑(e x) ∈ Submonoid.unitSphere ℂ
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ EqOn (↑(e'.symm.trans (e.restr s))) (↑((e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)))
    (e'.symm.trans (e.restr s)).source

Tactic:
· simp [Set.eqOn_refl]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

Tactic:
change _ = U.openPartialHomeomorphSubtypeCoe hU _

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(U.openPartialHomeomorphSubtypeCoe hU) (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y))
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}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ c ∈ s

Tactic:
rcases hc.1.eq_or_lt with heq | hlt
    · rwa [← heq]
    refine ⟨hc, ?_⟩
    /- In order to show that `c ∈ s`, consider a trivialization `ec` of `proj` over a neighborhood
      of `c`. Its base set includes `(c', c]` for some `c' ∈ [a, c)`. -/
    obtain ⟨ec, hc⟩ : ∃ ec : Trivialization F (π F E), c ∈ ec.baseSet :=
      ⟨trivializationAt F E c, mem_baseSet_trivializationAt F E c⟩
    obtain ⟨c', hc', hc'e⟩ : ∃ c' ∈ Ico a c, Ioc c' c ⊆ ec.baseSet :=
      (mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset hlt).1
        (mem_nhdsWithin_of_mem_nhds <| IsOpen.mem_nhds ec.open_baseSet hc)
    /- Since `c' < c = Sup s`, there exists `d ∈ s ∩ (c', c]`. Let `ead` be a trivialization of
      `proj` over `[a, d]`. Then we can glue `ead` and `ec` into a trivialization over `[a, c]`. -/
    obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2
    refine ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 ?_⟩
    exact ⟨fun x hx => had ⟨hx.1.1, hx.2⟩, fun x hx => hc'e ⟨hd.1.trans (not_le.1 hx.2), hx.1.2⟩⟩

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 ⁻¹' proj ⁻¹' e'.baseSet ∩ e.baseSet ×ˢ univ = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
e.preimage_symm_proj_inter,

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'.baseSet ∩ e.baseSet) ×ˢ univ = (e.baseSet ∩ e'.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
by
  let := a.totalSpaceTopology
  obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he')
    e.source (a.isOpen_source e)
  rw [inter_comm, hu2]
  exact hu1.inter e'.open_target

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
e₁ e₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

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

Goal state before:
pp: case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
hg : Function.Injective g
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← hg.preimage_pullbackDiagonal]

Goal state after:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
hg : Function.Injective g
⊢ IsOpen[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inr
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 ∈ e'.source
⊢ (e.source.piecewise (↑e) (↑e') p).1 = proj p

Tactic:
rw [piecewise_eq_of_notMem, e'.coe_fst hp']

Goal state after:
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 ∈ e'.source
⊢ p ∉ e.source
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
b : A
⊢ ‖a.toProd.1 b‖₊ ^ 2 = ‖star (a.toProd.1 b) * a.toProd.1 b‖₊

Tactic:
by
        simpa only [← sq] using CStarRing.nnnorm_star_mul_self.symm

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

Goal state before:
pp: case refine_2.refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < (fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) x

Tactic:
simpa [a.central, CStarRing.nnnorm_star_mul_self, ← sq]
            using pow_lt_pow_left₀ hxr zero_le two_ne_zero

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (x ^ n)) a = n • cfc Real.log a

Tactic:
simp_rw [Real.log_pow, ← Nat.cast_smul_eq_nsmul ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ x.angleDiff y + y.angleDiff x = 2 * π

Tactic:
grind [arg_eq_arg, neg_pi_lt_arg x.val, arg_le_pi y.val]

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

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ 2 ^ 2 ≤ ‖u - 1‖ ^ 2 → -1 ∈ spectrum ℂ u

Tactic:
rw [norm_sub_one_sq_eq hu hx]

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ 2 ^ 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case succ
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H
T : ℝ
hT : T ≠ 0
b : AddCircle T
z✝ : ℝ
h : toCircle ↑z✝ = b.toCircle
⊢ ↑z✝ = b

Tactic:
induction b using QuotientAddGroup.induction_on

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case succ
z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
ih : z ∈ centeredArc (π / 2 ^ (n + 1))
⊢ z ∈ centeredArc (π / 2 ^ (n + 1 + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖↑(expUnitary (t • argSelfAdjoint u)) - 1‖ ≤ ‖↑u - 1‖

Tactic:
by
  have key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖ := by
    rw [← one_mul ‖argSelfAdjoint u‖]
    simp_rw [AddSubgroupClass.coe_norm, val_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg ht.1]
    gcongr
    exact ht.2
  rw [← sq_le_sq₀ (by positivity) (by positivity)]
  rw [norm_sq_expUnitary_sub_one (key.trans <| norm_argSelfAdjoint_le_pi u)]
  trans 2 * (1 - Real.cos ‖argSelfAdjoint u‖)
  · gcongr
    exact Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) (norm_argSelfAdjoint_le_pi u) key
  · exact (two_mul_one_sub_cos_norm_argSelfAdjoint hu).le

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

Goal state before:
pp: case mp
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ u ∈ thickening 2 (Set.range fun y ↦ (List.map expUnitary y).prod) → u ∈ Set.range fun y ↦ (List.map expUnitary y).prod

Tactic:
hu

Goal state after:
case mp
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : u ∈ thickening 2 (Set.range fun y ↦ (List.map expUnitary y).prod)
⊢ u ∈ Set.range fun y ↦ (List.map expUnitary y).prod
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
h : ∑ i, (s.points i -ᵥ p) = 0
x : Fin (n + 1)
hx : x ∈ univ
⊢ s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)

Tactic:
rw [vsub_sub_vsub_cancel_right _ _ s.centroid]

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
x : E
⊢ adjoint (toSpanSingleton 𝕜 E x) = (innerₛₗ 𝕜) x

Tactic:
by
  simp [← adjoint_innerₛₗ_apply]

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n * (↑n)⁻¹ = 1

Tactic:
mul_inv_cancel₀ (NeZero.ne (n : k))

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
i : Fin (n + 1)
⊢ 1 = 1
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_1
𝕜 : 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
u : H →L[𝕜] K
h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
x : H
⊢ (adjoint u ∘SL u) x = 1 x

pp: case refine_2
𝕜 : 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
u : H →L[𝕜] K
h : adjoint u ∘SL u = 1
⊢ ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜

Tactic:
· refine ext_inner_right 𝕜 fun y ↦ ?_
    simpa [star_eq_adjoint, adjoint_inner_left] using h x y

Goal state after:
case refine_2
𝕜 : 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
u : H →L[𝕜] K
h : adjoint u ∘SL u = 1
⊢ ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜
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
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n

Tactic:
have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]

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
hi' : AffineIndependent k fun x ↦ ↑x
hc' : #(Finset.image p s) = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
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✝ : ∃ α, ∀ (x : H), f x = (α • g) x
y : ↥(unitary 𝕜)
h : ∀ (x : H), f x = (y • g) x
⊢ ↑y • 1 = ↑(↑g).symm ∘SL ↑↑f

Tactic:
ext; simp [h]

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

Goal state before:
pp: case e_a
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
i : Fin (n + 1)
⊢ ↑n * (↑n)⁻¹ = ↑n * (↑n + 1)⁻¹ + (↑n + 1)⁻¹

Tactic:
mul_inv_cancel₀ (NeZero.ne (n : k))

Goal state after:
case e_a
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
i : Fin (n + 1)
⊢ 1 = ↑n * (↑n + 1)⁻¹ + (↑n + 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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.median i

Tactic:
by
  simp [median, left_mem_affineSpan_pair]

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
hcard : #s' = n
hcard' : 1 < #s'
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1

Tactic:
Finset.one_lt_card_iff

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
hcard : #s' = n
hcard' : ∃ a b, a ∈ s' ∧ b ∈ s' ∧ a ≠ b
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

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

Tactic:
simp [Real.zero_rpow hp.ne', summable_zero]

Goal state after: