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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
⊢ ∀ ⦃x : A⦄, x ∈ s → ∀ ⦃y : A⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
intro x hx y hy a b ha hb hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
x : A
hx : x ∈ s
y : A
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul A E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
h : ‖x‖ = 0
⊢ x = 0

Tactic:
by simpa [norm_eq_sqrt_norm_inner_self (A := A), inner_self] using h

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ a * e = a

Tactic:
suffices sqrt a * (1 - e : A⁺¹) = 0 by
    simpa [← mul_assoc, sqrt_mul_sqrt_self a, mul_sub, sub_eq_zero, eq_comm (a := a)]
      using congr(sqrt a * $this)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a✝ e✝ : A
he✝ : IsStarProjection e✝
ha✝ : 0 ≤ a✝
hae✝ : a✝ ≤ e✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ sqrt a * (1 - e) = 0
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
c : Unitization ℂ A
hc : 0 ≤ c
⊢ ContinuousOn (fun x ↦ (1 + x)⁻¹) (σ ℝ≥0 c)

Tactic:
by fun_prop (disch := intro _ _; positivity)

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

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (Filter.comap (fun a ↦ (a.1 i_1, a.2 i_1)) (𝓤 𝕜)) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
Filter.comap_comap

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap ((fun a ↦ (a.1 i_1, a.2 i_1)) ∘ fun a ↦ (a.1 i, a.2 i)) (𝓤 𝕜) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
h₂ : LipschitzWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s}))
h₃ : LipschitzOnWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s})) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}

Tactic:
simpa using! lipschitzOnWith_cfcₙ_fun R a |>.comp h₃ (fun f ↦ .imp_left fun hf ↦ hf.mono hs)

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖toLp 2 fun i ↦ toLp 2 fun j ↦ A i j‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
PiLp.nnnorm_eq_of_L2,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ NNReal.sqrt (∑ x, NNReal.sqrt (∑ x_1, ‖A x x_1‖₊ ^ 2) ^ 2) = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : One α
⊢ ‖toLp 2 (Function.const n 1)‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊

Tactic:
rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]
      simp [NNReal.sqrt_eq_rpow]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
⊢ (mapₗ ↑f) (star M) = star ((mapₗ ↑f) M)

Tactic:
ext; simp [map, star_apply, map_star]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)

Tactic:
simp [mul_comm I, re_add_im, cfcₙ_id' .., realPart_add_I_smul_imaginaryPart]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: case mpr
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} → x✝ ∈ Set.range fun x ↦ cfcₙ x a

Tactic:
rintro ⟨f, hf, rfl⟩
    simp only [cfcₙ_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(((rankOne 𝕜) x) y)).rank = 1

Tactic:
rw [LinearMap.rank, rankOne_def, range_smulRight_apply, Module.rank_eq_one_iff_finrank_eq_one]

Goal state after:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ finrank 𝕜 ↥(𝕜 ∙ x) = 1

case hf
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ (innerSL 𝕜) y ≠ 0
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: case refine_2.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : 0 ≤ ↑(2 • e - e * e)
⊢ ‖2 • e - e * e‖ ≤ 1

Tactic:
· rw [← norm_inr (𝕜 := ℂ), norm_le_one_iff_of_nonneg _ this, ← sub_nonneg]
      calc 0 ≤ star (1 - e : A⁺¹) * (1 - e) := star_mul_self_nonneg _
        _ = _ := by simp [LE.le.star_eq, h1, mul_sub, sub_mul, two_smul, sub_sub, add_sub]

Goal state after:
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
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ EqOn (↑((e.restr s).symm.trans e')) (↑((e.symm.trans e').restr (↑e '' s))) ((e.restr s).symm.trans e').source

Tactic:
simp_rw [coe_trans, restr_symm_apply, restr_apply, coe_trans]

Goal state after:
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
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ EqOn (↑e' ∘ ↑e.symm) (↑e' ∘ ↑e.symm) ((e.restr s).symm.trans e').source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: 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
⊢ ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target

Tactic:
rw [Opens.openPartialHomeomorphSubtypeCoe_target] at hy ⊢

Goal state after:
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
⊢ ↑e.symm y ∈ ↑V
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: 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
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ e.target = e.baseSet ×ˢ univ

Tactic:
ext; simp [e.target_eq]

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

Goal state before:
pp: case neg
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 : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ e.source
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
e.source_eq

Goal state after:
case neg
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 : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ proj ⁻¹' e.baseSet
hl : ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)
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₃ (↑e₂.symm (↑e₂.toOpenPartialHomeomorph (↑e₁.symm (b, x))))).2 = e₁.coordChange e₃ b x

Tactic:
e₂.left_inv,

Goal state after:
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₃ (↑e₁.symm (b, x))).2 = e₁.coordChange e₃ b x

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
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 : 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

Tactic:
exact ⟨U, hU, fun g ↦ by simpa using hU' (Multiplicative.ofAdd.symm g)⟩

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

Goal state before:
pp: case refine_1
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₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
e' : E
he' : e' ∈ U
hfe : f e' = f e
⊢ e ∈ ⋃ i, (fun x ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)

Tactic:
obtain ⟨g', rfl⟩ := hfG.mp hfe

Goal state after:
case refine_1
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₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun m ↦ m • e) g' ∈ U
hfe : f ((fun m ↦ m • e) g') = f e
⊢ e ∈ ⋃ i, (fun x ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
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
a : A
ha : IsSelfAdjoint a
⊢ log (exp a) = a

Tactic:
have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)
  rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]
  simp [cfc_id' (R := ℝ) a]

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

Goal state before:
pp: x y : Circle
⊢ ⇑(x.path y) = ⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))

Tactic:
by
  ext t
  rw [path_apply, comp_apply]

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

Goal state before:
pp: T : ℝ
x : AddCircle T
n : ℕ
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [succ_nsmul, toCircle_add, ih, pow_succ]

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

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

Tactic:
simp_rw [toCircle_apply_mk] at h

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
⊢ ↑z✝¹ = ↑z✝
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ ‖argSelfAdjoint u‖ < π

Tactic:
rw [norm_argSelfAdjoint hu]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2) < π
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr.nil
A : Type u_1
inst✝ : CStarAlgebra A
⊢ (List.map expUnitary []).prod ∈ pathComponent 1

Tactic:
| nil =>

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
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ⟪T x, T x⟫_𝕜 - ⟪T ((adjoint T) x), x⟫_𝕜 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
inner_self_eq_norm_sq_to_K,

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
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ⟪T ((adjoint T) x), x⟫_𝕜 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
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
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ⟪(adjoint T) x, (adjoint T) x⟫_𝕜 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
inner_self_eq_norm_sq_to_K,

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
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ↑‖(adjoint T) x‖ ^ 2 = 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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
⊢ i ∈ fs₁ ↔ i ∈ fs₂

Tactic:
have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast at h

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
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
i : Fin (n + 1)
ha :
  (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1))⁻¹) i =
    (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1))⁻¹) i
key : ∀ (n : ℕ), ↑n + 1 ≠ 0
⊢ i ∈ fs₁ ↔ i ∈ fs₂
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ Nonempty ι

Tactic:
simp [← Fintype.card_pos_iff, hc]

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

Goal state before:
pp: case mp
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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ → Fintype.card ι = finrank k V + 1

pp: case mpr
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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι = finrank k V + 1 → affineSpan k (Set.range p) = ⊤

Tactic:
· intro h_tot
    let n := Fintype.card ι - 1
    have hn : Fintype.card ι = n + 1 :=
      (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
    rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]

Goal state after:
case mpr
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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι = finrank k V + 1 → affineSpan k (Set.range p) = ⊤
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: 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)
y : P
⊢ (lineMap q y) (ε / dist y q) ∈ Metric.closedBall q ε

Tactic:
rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs,
      dist_eq_norm_vsub V y q, abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]

Goal state after:
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)
y : P
⊢ ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε
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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Tactic:
have h := collinear_iff_rank_le_one k s

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1
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
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ finrank k ↥(vectorSpan k s) + 1 ≤ 2

Tactic:
h.finrank_le_one

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ 1 + 1 ≤ 2
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
i : α
⊢ ‖c • f i‖ ≤ ‖c‖ * A

Tactic:
refine (norm_smul_le _ _).trans ?_

Goal state after:
case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
i : α
⊢ ‖c‖ * ‖f i‖ ≤ ‖c‖ * A