mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
;

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

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

Tactic:
;

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: case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T

Tactic:
;

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

Goal state before:
pp: case e'_5
x✝ : ℝ
⊢ ↑(exp x✝) = ↑((⇑(homeomorphCircle ⋯) ∘ QuotientAddGroup.mk) x✝)

Tactic:
;

Goal state after:
case e'_5
x✝ : ℝ
⊢ ↑(exp x✝) = ↑((⇑(homeomorphCircle ⋯) ∘ QuotientAddGroup.mk) x✝)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case e'_5
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := ⋯
x✝ : AddCircle 1
⊢ ↑((⇑(zpowGroupHom n) ∘ ⇑e) x✝) = ↑((⇑e ∘ fun x ↦ n • x) x✝)

Tactic:
;

Goal state after:
case e'_5
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := ⋯
x✝ : AddCircle 1
⊢ ↑((⇑(zpowGroupHom n) ∘ ⇑e) x✝) = ↑((⇑e ∘ fun x ↦ n • x) x✝)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case e'_3
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
⊢ ↑(φ e) = f

Tactic:
;

Goal state after:
case e'_3
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝² : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝¹ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this : Nonempty E
e : ↑(f ⁻¹' {x})
⊢ ↑(φ e) = f
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✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    1 x✝

Tactic:
;

Goal state after:
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✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits 1);
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    1 x✝
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)
x✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝² * x✝¹));
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    ((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' := ⋯ })
      x✝

Tactic:
;

Goal state after:
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)
x✝ : A
⊢ (let __spread.0 := (Units.mulLeftLinearEquiv R A) (toUnits (x✝² * x✝¹));
      { toLinearEquiv := __spread.0, norm_map' := ⋯ })
      x✝ =
    ((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' := ⋯ })
      x✝
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
u : ↥(unitary A)
x✝ : A
⊢ ((mulLeft R A) u).symm x✝ = ((mulLeft R A) (star u)) x✝

Tactic:
;

Goal state after:
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
u : ↥(unitary A)
x✝ : A
⊢ ((mulLeft R A) u).symm x✝ = ((mulLeft R A) (star u)) x✝
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✝ : IsScalarTower R A A
u : ↥(unitary A)
x✝ : A
⊢ (mulRight R u).symm x✝ = (mulRight R (star u)) x✝

Tactic:
;

Goal state after:
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✝ : IsScalarTower R A A
u : ↥(unitary A)
x✝ : A
⊢ (mulRight R u).symm x✝ = (mulRight R (star u)) x✝
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✝ : IsScalarTower R A A
u v : ↥(unitary A)
x✝ : A
⊢ ((mulRight R u).trans (mulRight R v)) x✝ = (mulRight R (u * v)) x✝

Tactic:
;

Goal state after:
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✝ : IsScalarTower R A A
u v : ↥(unitary A)
x✝ : A
⊢ ((mulRight R u).trans (mulRight R v)) x✝ = (mulRight R (u * v)) x✝
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✝ : IsScalarTower R A A
x✝ : A
⊢ (mulRight R 1) x✝ = (LinearIsometryEquiv.refl R A) x✝

Tactic:
;

Goal state after:
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✝ : IsScalarTower R A A
x✝ : A
⊢ (mulRight R 1) x✝ = (LinearIsometryEquiv.refl R A) x✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪(adjoint A ∘SL A) x, x⟫_𝕜 = ⟪(adjoint A) (A x), x⟫_𝕜

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪(adjoint A ∘SL A) x, x⟫_𝕜 = ⟪(adjoint A) (A x), x⟫_𝕜
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
⊢ ‖↑v - 1‖ ^ 2 ≤ ε

Tactic:
refine Real.le_sqrt (by positivity) (by positivity) |>.mp ?_

Goal state after:
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
⊢ ‖↑v - 1‖ ≤ √ε
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪x, (adjoint A) (A x)⟫_𝕜

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪x, (adjoint A) (A x)⟫_𝕜
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:
;

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
huv : ‖↑v - ↑u‖ < 2
⊢ ↑(expUnitary (↑0 • argSelfAdjoint (v * star u)) * u) = ↑u
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ IsPathConnected (ball u δ)

Tactic:
by
  suffices IsPathConnected (ball (1 : unitary A) δ) by
    convert! this |>.image (f := (u * ·)) (by fun_prop)
    ext v
    rw [← inv_mul_cancel u]
    simp [-inv_mul_cancel, Subtype.dist_eq, dist_eq_norm, ← mul_sub]
  refine ⟨1, by simpa, fun {u} hu ↦ ?_⟩
  have hu : ‖(u - 1 : A)‖ < δ := by simpa [Subtype.dist_eq, dist_eq_norm] using hu
  refine ⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩
  simpa [Subtype.dist_eq, dist_eq_norm] using
    norm_expUnitary_smul_argSelfAdjoint_sub_one_le u t.2 (hu.trans hδ₂) |>.trans_lt hu

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

Goal state before:
pp: case mp
A : Type u_1
inst✝ : CStarAlgebra A
⊢ pathComponent 1 ⊆ Set.range fun y ↦ (List.map expUnitary y).prod

Tactic:
pathComponent_eq_connectedComponent

Goal state after:
case mp
A : Type u_1
inst✝ : CStarAlgebra A
⊢ connectedComponent 1 ⊆ Set.range fun y ↦ (List.map expUnitary y).prod
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hf : ContDiff ℝ ∞ f
h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x
⊢ AbsolutelyMonotoneOn f s

Tactic:
refine ⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩
  exact iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx

Goal state after:
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ
hT : T = c • ContinuousLinearMap.id ℝ ℝ
x : ℝ
⊢ (⇑T ∘ f) x = (c • f) x

Tactic:
;

Goal state after:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ
hT : T = c • ContinuousLinearMap.id ℝ ℝ
x : ℝ
⊢ (⇑T ∘ f) x = (c • f) x
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

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

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
y : F
x : E
w✝ : ↥(↑A).range
⊢ 0 ≤ (fun w ↦ ‖y - ↑w‖) w✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case hbc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖(adjoint A ∘SL A) x‖ ≤ ‖adjoint A ∘SL A‖ * ‖x‖

Tactic:
;

Goal state after:
case hbc
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖(adjoint A ∘SL A) x‖ ≤ ‖adjoint A ∘SL A‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖adjoint A ∘SL A‖ = 0 ↔ A = 0

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖adjoint A ∘SL A‖ = 0 ↔ A = 0
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : F
f : E →L[𝕜] F
x✝ : E
⊢ ((innerSL 𝕜) x ∘SL f) x✝ = ((innerSL 𝕜) ((adjoint f) x)) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : F
f : E →L[𝕜] F
x✝ : E
⊢ ((innerSL 𝕜) x ∘SL f) x✝ = ((innerSL 𝕜) ((adjoint f) x)) x✝
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : (↑f).IsSymmetric
x✝ : E
⊢ ((innerSL 𝕜) x ∘SL f) x✝ = ((innerSL 𝕜) (f x)) x✝

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : (↑f).IsSymmetric
x✝ : E
⊢ ((innerSL 𝕜) x ∘SL f) x✝ = ((innerSL 𝕜) (f x)) x✝
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✝ : CompleteSpace E
w✝¹ : Submodule 𝕜 E
w✝ : w✝¹.HasOrthogonalProjection
⊢ IsStarProjection w✝¹.starProjection

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
w✝¹ : Submodule 𝕜 E
w✝ : w✝¹.HasOrthogonalProjection
⊢ IsStarProjection w✝¹.starProjection
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪(adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
← coe_toContinuousLinearMap A,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪(adjoint ↑(toContinuousLinearMap A)) y, x⟫_𝕜 = ⟪y, ↑(toContinuousLinearMap A) x⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
← coe_toContinuousLinearMap A,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
y : F
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ ⟪x, (adjoint ↑(toContinuousLinearMap A)) y⟫_𝕜 = ⟪↑(toContinuousLinearMap A) x, y⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥A.range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥A.range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range
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
⊢ Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Tactic:
by
  refine ⟨fun h => ?_, @congrArg _ _ fs₁ fs₂ (fun z => Finset.centroid k z s.points)⟩
  rw [Finset.centroid_eq_affineCombination_fintype,
    Finset.centroid_eq_affineCombination_fintype] at h
  have ha :=
    (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _
      (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁)
      (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h
  simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff,
    Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha
  ext i
  specialize ha i
  have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast at h
  -- we should be able to golf this to
  -- `refine ⟨fun hi ↦ decidable.by_contradiction (fun hni ↦ ?_), ...⟩`,
  -- but for some unknown reason it doesn't work.
  constructor <;> intro hi <;> by_contra hni
  · simp [hni, hi, key] at ha
  · simpa [hni, hi, key] using ha.symm

Goal state after:
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✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
⊢ Finite ι

Tactic:
;

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✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
⊢ Finite ι
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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ #(Finset.image (fun p ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) ≤ n

Tactic:
rw [Finset.card_image_of_injective _ (vsub_left_injective p₁), Finset.card_erase_of_mem hp₁,
    tsub_le_iff_right, ← hc]

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
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ #(Finset.image p s) ≤ #s
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
x✝ : H
⊢ (↑y • 1) x✝ = (↑(↑g).symm ∘SL ↑↑f) x✝

Tactic:
;

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
x✝¹ : ∃ α, ∀ (x : H), f x = (α • g) x
y : ↥(unitary 𝕜)
h : ∀ (x : H), f x = (y • g) x
x✝ : H
⊢ (↑y • 1) x✝ = (↑(↑g).symm ∘SL ↑↑f) 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
⊢ ↑↑f x✝ = (y • ↑↑g) x✝

Tactic:
;

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