mathlib-initiative/mathlib-tactics huggingface dataset:
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
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
i✝ j✝ : n
⊢ star M (e.symm i✝) (e.symm j✝) = star (Matrix.submatrix M ⇑e.symm ⇑e.symm) i✝ j✝

Tactic:
rw [star_apply, star_apply]

Goal state after:
m : Type u_1
n : Type u_2
R✝ : Type u_3
S : Type u_4
A✝ : Type u_5
B : Type u_6
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
i✝ j✝ : n
⊢ star (M (e.symm j✝) (e.symm i✝)) = star (Matrix.submatrix M (⇑e.symm) (⇑e.symm) j✝ i✝)
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✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ x✝ : A
⊢ (fun x y ↦ x✝¹ + x✝) = (fun x y ↦ x✝¹) + fun x y ↦ x✝

Tactic:
by ext; simp

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✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝¹ : R
x✝ : A
⊢ (fun x y ↦ x✝¹ • x✝) = x✝¹ • fun x y ↦ x✝

Tactic:
by ext; simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
⊢ (toCLM M) v = (WithCStarModule.equiv A (n → A)).symm fun j ↦ ∑ i, v i * M i j

Tactic:
ext i
  simp [toCLM_apply, Matrix.vecMul, dotProduct]

Goal state after:
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
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ Integrable (fun x ↦ cfcₙ (f x) a) μ

Tactic:
conv in cfcₙ _ _ => rw [cfcₙ_eq_cfcₙL_mkD _ a]

Goal state after:
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
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ Integrable (fun x ↦ (cfcₙL ha) (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0)) μ
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
hmain : ‖M‖ ≤ √‖M * star M‖
⊢ ‖M‖ * ‖M‖ ≤ ‖M * star M‖

Tactic:
rw [← Real.sqrt_le_sqrt_iff (by positivity)]

Goal state after:
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
hmain : ‖M‖ ≤ √‖M * star M‖
⊢ √(‖M‖ * ‖M‖) ≤ √‖M * star M‖
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y✝ : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
x y : M
⊢ { toLinearMap := p (x + y), cont := ⋯ } = { toLinearMap := p x, cont := ⋯ } + { toLinearMap := p y, cont := ⋯ }

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.PerfectPairing

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
x✝ : M
y : N
inst✝¹ : p.IsContPerfPair
inst✝ : IsTopologicalRing R
r : R
x : M
⊢ { toLinearMap := p (r • x), cont := ⋯ } = (RingHom.id R) r • { toLinearMap := p x, cont := ⋯ }

Tactic:
by ext; simp

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 : ∃ x ∈ Yᗮ, x ≠ 0
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := 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
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
m : ℂ
x : A
⊢ (f.leftMulMapPreGNS (m • x)).completion = m • (f.leftMulMapPreGNS x).completion

Tactic:
ext a
  induction a using induction_on with
  | hp =>
    exact isClosed_eq (f.leftMulMapPreGNS (m • x)).completion.continuous
      (m • (f.leftMulMapPreGNS x).completion).continuous
  | ih a => simp [smul_mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ ball 0 1
hy : b✝ ∈ ball 0 1
⊢ a✝ * b✝ ∈ ball 0 1

Tactic:
mem_ball_zero_iff

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ < 1
hy : ‖b✝‖ < 1
⊢ ‖a✝ * b✝‖ < 1
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:
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.restr s).symm) (↑((e.symm.trans e').restr (↑e '' s))) ((e.restr s).symm.trans e').source
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 : Pretrivialization F TotalSpace.proj
⊢ IsOpen[a.totalSpaceTopology] e.source

Tactic:
by
  refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_
  refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)
  ext ⟨x, hx⟩
  simp only [mem_preimage, Pretrivialization.setSymm, domRestrict, e.mem_target, e.mem_source,
    e'.proj_symm_apply hx]

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
X : Type u_5
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
⊢ ContinuousAt f z

Tactic:
by
  have hez : z ∈ e.toPartialEquiv.symm.target := by
    rw [PartialEquiv.symm_target, e.mem_source]
    exact he
  rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
    OpenPartialHomeomorph.symm_symm]

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:
intro x
    rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Goal state after:
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
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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₂.coordChange e₁ b (e₁.coordChange e₂ b x) = x

Tactic:
by simp only [*, coordChange_coordChange, coordChange_same_apply]

Goal state after:
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
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
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ e₁.coordChange e₂ b (e₂.coordChange e₁ b x) = x

Tactic:
by simp only [*, coordChange_coordChange, coordChange_same_apply]

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

Goal state before:
pp: case e'_5
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
s : Set B
hps : IsOpen[inst✝²] (proj ⁻¹' s)
e : Trivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ ↑e.toPretrivialization.domExtend.toPartialEquiv ∘ Subtype.val = ↑e.toPartialEquiv

Tactic:
ext1 ⟨x, (hx : proj x ∈ s)⟩

Goal state after:
case e'_5
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
s : Set B
hps : IsOpen[inst✝²] (proj ⁻¹' s)
e : Trivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x : Z
hx : proj x ∈ s
⊢ (↑e.toPretrivialization.domExtend.toPartialEquiv ∘ Subtype.val) ⟨x, hx⟩ = ↑e.toPartialEquiv ⟨x, hx⟩
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.toProd.1‖

Tactic:
norm_fst_eq_snd

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)
⊢ ‖a.toProd.2‖ = ‖a.toProd.2‖
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
g : Multiplicative G
⊢ ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1

Tactic:
simpa using hU' (Multiplicative.ofAdd.symm g)

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
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Subtype.val ∘ f ⁻¹' Subtype.val '' U = f ⁻¹' U

Tactic:
by ext; simp

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : Group E
inst✝¹ : IsTopologicalGroup E
inst✝ : Group X
f : E →* X
hf : IsQuotientMap ⇑f
disc : IsDiscrete ↑f.ker
x✝¹ x✝ : E
⊢ f x✝ = f x✝¹ ↔ x✝ * x✝¹⁻¹ ∈ f.ker

Tactic:
← mul_inv_eq_one,

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : Group E
inst✝¹ : IsTopologicalGroup E
inst✝ : Group X
f : E →* X
hf : IsQuotientMap ⇑f
disc : IsDiscrete ↑f.ker
x✝¹ x✝ : E
⊢ f x✝ * (f x✝¹)⁻¹ = 1 ↔ x✝ * x✝¹⁻¹ ∈ f.ker
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ 0 ≤ x.angleDiff y

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

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ range ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) ⊆ Icc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
rw [Path.range_segment, segment_eq_Icc (by simp)]

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (insert (exp (↑x).arg) (⇑(x.path y) '' Ioc 0 1))ᶜ = ⇑(y.path x) '' Ioo 0 1

Tactic:
← union_singleton,

Goal state after:
x y : Circle
h : x ≠ y
⊢ (⇑(x.path y) '' Ioc 0 1 ∪ {exp (↑x).arg})ᶜ = ⇑(y.path x) '' Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ IsAddQuotientCoveringMap ⇑exp ↥(AddSubgroup.zmultiples (2 * π))

Tactic:
by
  convert! (isAddQuotientCoveringMap_coe _).homeomorph_comp (homeomorphCircle _)
  on_goal 2 => simp
  ext; simp [homeomorphCircle_apply, toCircle]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    1

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
x✝¹ x✝ : ↥(unitary A)
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝¹ * x✝));
    { toLinearEquiv := __spread.0, norm_map' := ⋯ }) =
    (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝¹);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ }) *
      let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits x✝);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ }

Tactic:
by ext; simp

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
s : Set X
inst✝ : T2Space E
hf : IsClosedMap f
hs : ∀ x ∈ s, (f ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ ∃ φ, e ∈ φ.source ∧ ↑φ = f

Tactic:
obtain ⟨φ, hφ, rfl⟩ := h e (by aesop)

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T2Space E
x : X
hx : x ∈ s
e : E
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
hf : IsClosedMap ↑φ
hs : ∀ x ∈ s, (↑φ ⁻¹' {x}).Finite
h : IsLocalHomeomorphOn (↑φ) (↑φ ⁻¹' s)
he : e ∈ ↑φ ⁻¹' {x}
⊢ ∃ φ_1, e ∈ φ_1.source ∧ ↑φ_1 = ↑φ
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✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
hf : Continuous[inst✝⁴, inst✝³] f
h : IsLocalHomeomorphOn f (f ⁻¹' s)
x : X
hx : x ∈ s
e : E
he : e ∈ f ⁻¹' {x}
⊢ ∃ φ, e ∈ φ.source ∧ ↑φ = f

Tactic:
obtain ⟨φ, hφ, rfl⟩ := h e (by aesop)

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
s : Set X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
x : X
hx : x ∈ s
e : E
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
hf : Continuous[inst✝⁴, inst✝³] ↑φ
h : IsLocalHomeomorphOn (↑φ) (↑φ ⁻¹' s)
he : e ∈ ↑φ ⁻¹' {x}
⊢ ∃ φ_1, e ∈ φ_1.source ∧ ↑φ_1 = ↑φ
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
⊢ ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖

Tactic:
← one_mul ‖argSelfAdjoint u‖

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • (2⁻¹ • (↑u₁ + star ↑u₁) + I • 2⁻¹ • (↑u₂ + star ↑u₂))

Tactic:
← realPart_apply_coe (u₁ : A),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
⊢ x = ‖x‖ • (↑(ℜ ↑u₁) + I • 2⁻¹ • (↑u₂ + star ↑u₂))
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖↑v - ↑u‖ < 2
⊢ expUnitary (↑0 • argSelfAdjoint (v * star u)) * u = u

Tactic:
by ext; simp

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✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : i ∈ Set.univ ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h : (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' t)
wdef : w = centroidWeights k univ
⊢ ∑ i, w i = 1

Tactic:
sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)

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✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : i ∈ Set.univ ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h : (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' t)
wdef : w = centroidWeights k univ
⊢ 1 = 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
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₂

Tactic:
constructor <;> intro hi <;> by_contra hni

Goal state after:
case mp
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
hi : i ∈ fs₁
hni : i ∉ fs₂
⊢ False

case mpr
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
hi : i ∈ fs₂
hni : i ∉ fs₁
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
⊢ ↑↑e * ↑↑e.symm = 1

Tactic:
by ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
e : H ≃ₗᵢ[𝕜] H
⊢ ↑↑e.symm * ↑↑e = 1

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p : P
hcol : Collinear k {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
⊢ AffineIndependent k ![p₁, p₂, p] ↔ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
refine ⟨fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h hcol hne2,
    fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h ?_ hne1⟩

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
p₁ p₂ p₃ p : P
hcol : Collinear k {p₂, p, p₃}
hne1 : p₂ ≠ p
hne2 : p₂ ≠ p₃
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ Collinear k {p₂, p₃, p}
Module: Mathlib.Analysis.Normed.Lp.lpSpace

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

Tactic:
obtain (rfl | rfl | hp) := p.trichotomy

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) 0 ↔ Memℓp f 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) ∞ ↔ Memℓp f ∞

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p