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

Goal state before:
pp: case a
𝕜 : 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
⊢ ∀ x ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

pp: case a
𝕜 : 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
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val

Tactic:
· intro x h_x
      rw [Multiset.mem_map] at h_x
      obtain ⟨a, h_a⟩ := h_x
      rw [← h_a.2]
      apply sq_nonneg

Goal state after:
case a
𝕜 : 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
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val
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
⊢ ∑ j, ↑‖U i j‖ ^ 2 = ↑(∑ x, ‖U i x‖ ^ 2)

Tactic:
norm_cast

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
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) = ∑ x, ‖U i x‖ ^ 2

Tactic:
norm_cast

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

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ F (f x₀) = (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f x₀)

Tactic:
F_eq,

Goal state after:
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) (f x₀) =
    (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f x₀)
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✝¹ : FiberBundle F E
inst✝ : T1Space B
x : B
⊢ IsClosed[inst✝³] (range (TotalSpace.mk x))

Tactic:
rw [TotalSpace.range_mk]
    exact isClosed_singleton.preimage <| continuous_proj F E

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
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
z : TotalSpace F E
hz : z.proj ∈ e.baseSet
⊢ e.symm z.proj (↑e z).2 = z.snd

Tactic:
by
  rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)]

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
e✝ : Pretrivialization F proj
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : x ∈ Prod.map Subtype.val id ⁻¹' e.target
⊢ (if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2) ∈
    Subtype.val ⁻¹' e.source

Tactic:
by
    simp only [mem_preimage, (Prod.map_apply), id_eq] at hx
    rw [dif_pos hx]; exact e.map_target' hx

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
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (proj ⁻¹' e.baseSet) e'.source

Tactic:
e'.source_eq

Goal state after:
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
⊢ Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hg : IsLocalHomeomorphOn g (f '' s)
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
by
  obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩
  obtain ⟨gf, hgf, he⟩ := hgf x hx
  refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩
  change f y = g.symm (gf y)
  have : f y ∈ g.source := by apply interior_subset hy.1.2
  rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]

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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
inst✝ : Nonempty I
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
e : E
he : f e ∈ U
⊢ (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)) ∈ U ×ˢ Set.univ

Tactic:
simp [he]

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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
inst✝ : Nonempty I
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
e : E
he : f e ∈ U
⊢ ↑(H.symm
        (if hx : (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).1 ∈ U then
            ⟨(if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).1, hx⟩
          else ⟨x, hxU⟩,
          (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).2)) =
    e

Tactic:
simp [he]

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

Goal state before:
pp: case 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‖₊
⊢ ∃
    a_1 ∈
      (fun a_2 ↦ sSup ((fun x ↦ ‖a.toProd.2 (star (a.toProd.1 (star a_2))) * x‖₊) '' Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1,
    r < a_1

Tactic:
simp only [Set.mem_image, exists_exists_and_eq_and]

Goal state after:
case 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‖₊
⊢ ∃ a_1 ∈ Metric.closedBall 0 1,
    r < sSup ((fun x ↦ ‖a.toProd.2 (star (a.toProd.1 (star a_1))) * x‖₊) '' Metric.closedBall 0 1)
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
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ log (r • a) = (algebraMap ℝ A) (Real.log r) + log a

Tactic:
by
  rw [log, ← cfc_smul_id (R := ℝ) r a, ← cfc_comp Real.log (r • ·) a, log]
  calc
    _ = cfc (fun z => Real.log r + Real.log z) a :=
      cfc_congr (Real.log_mul hr <| ha₂ · ·)
    _ = _ := by rw [cfc_const_add _ _ _]

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

Goal state before:
pp: x y : ℝ
n : ℤ
⊢ ↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)

Tactic:
norm_cast

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

Goal state before:
pp: x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
⊢ Disjoint (⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (⇑(y.path x) '' Ioc 0 1)

Tactic:
path_image_Ioc_of_ne h.symm

Goal state after:
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
⊢ Disjoint (⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (⇑exp '' Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
hP₂ : x ∈ range ⇑(y.path (-x))
h : x ∈ range ⇑((-x).path y) ∩ range ⇑(y.path (-x))
⊢ False

Tactic:
rw [range_path_inter_range_path hne] at h

Goal state after:
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
hP₂ : x ∈ range ⇑(y.path (-x))
h : x ∈ {-x, y}
⊢ False
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)
⊢ IsCoveringMapOn f s

Tactic:
intro x hx
  refine hf.isEvenlyCovered_of_openPartialHomeomorph (hs x hx) fun e he ↦ ?_
  obtain ⟨φ, hφ, rfl⟩ := h e (by aesop)
  aesop

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

Goal state before:
pp: case h.right
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := ⋯
u₂ : ↥(unitary A) := ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
⊢ ∀ (i : Fin 4), ‖![↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹ * I, ↑‖x‖ * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2

Tactic:
intro i

Goal state after:
case h.right
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
i : Fin 4
⊢ ‖![↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹ * I, ↑‖x‖ * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ‖A x‖ ≤ √‖adjoint A ∘SL A‖ * ‖x‖

Tactic:
have :=
      calc
        re ⟪(A† ∘L A) x, x⟫ ≤ ‖(A† ∘L A) x‖ * ‖x‖ := re_inner_le_norm _ _
        _ ≤ ‖A† ∘L A‖ * ‖x‖ * ‖x‖ := by gcongr; exact le_opNorm _ _

Goal state after:
case refine_2
𝕜 : 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
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ ‖A x‖ ≤ √‖adjoint A ∘SL A‖ * ‖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
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 = ↑‖(adjoint T) x‖ ^ 2) ↔ ∀ (v : E), ‖T v‖ ^ 2 = ‖(adjoint T) v‖ ^ 2

Tactic:
norm_cast

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
i : Fin (n + 1)
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

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
h : (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.centroid) = 0
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

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
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
⊢ (↑n + 1) • (p -ᵥ s.centroid) = 0

Tactic:
norm_cast

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
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : (↑n + 1) • (p -ᵥ s.centroid) = 0
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

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
p : P
⊢ p = s.centroid ↔ ∑ i, (s.points i -ᵥ p) = 0

Tactic:
constructor
  · intro h
    rw [h, centroid_weighted_vsub_eq_zero]
  · intro h
    rw [← vsub_eq_zero_iff_eq]
    have : ∑ i, (s.points i -ᵥ p) = ∑ i, ((s.points i -ᵥ s.centroid) - (p -ᵥ s.centroid)) := by
      apply sum_congr rfl
      intro x hx
      rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
    rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h
    simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h
    have h' : ((n : k) + 1) • (p -ᵥ s.centroid) = 0 := by norm_cast
    rw [smul_eq_zero_iff_right (by norm_cast)] at h'
    exact h'

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
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re (↑‖T x‖ ^ 2)

Tactic:
norm_cast

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ‖T x‖ ^ 2
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
T : E →ₗ[𝕜] E
x : E
⊢ im (↑‖T x‖ ^ 2) = 0

Tactic:
norm_cast

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 j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points j) + (s.points i -ᵥ s.points j) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i)

Tactic:
h1 i,

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 j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)) - (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points j) +
      (s.points i -ᵥ s.points j) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i)
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 + 1 ≠ 0

Tactic:
norm_cast

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)
this : (↑n + 1)⁻¹ = 1 * (↑n + 1)⁻¹
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

Goal state after:
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
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
⊢ ⟪((toLin v₂.toBasis v₁.toBasis) Aᴴ) (v₂.toBasis i), v₁.toBasis j⟫_𝕜 =
    ⟪v₂.toBasis i, ((toLin v₁.toBasis v₂.toBasis) A) (v₁.toBasis j)⟫_𝕜

Tactic:
toLin_self

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
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
⊢ ⟪∑ j, Aᴴ j i • v₁.toBasis j, v₁.toBasis j⟫_𝕜 = ⟪v₂.toBasis i, ∑ j_1, A j_1 j • v₂.toBasis j_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
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
⊢ ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i

Tactic:
intro i

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
i : ↥s'
⊢ p -ᵥ s.centroid ∈ k ∙ u i
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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
p : P
⊢ FiniteDimensional k ↥(vectorSpan k (insert p s))

Tactic:
have : FiniteDimensional k (affineSpan k s).direction :=
    (direction_affineSpan k s).symm ▸ inferInstance
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
  exact finiteDimensional_vectorSpan_insert (affineSpan k s) p

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ vectorSpan k s ≤ k ∙ v

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]

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
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ ∀ x ∈ (fun x ↦ x -ᵥ p₀) '' s, x ∈ ↑(k ∙ v)
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 : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Tactic:
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by decide +revert
  rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]

Goal state after: