mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = (g ∘ ↑f) (↑f.symm y)

Tactic:
Function.comp_apply,

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = g (↑f (↑f.symm y))
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
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 : ↑(f ⁻¹' {x})
⊢ ↑(H (Set.inclusion ⋯ ((fun i ↦ ⟨↑(H.symm (⟨x, hxU⟩, i)), ⋯⟩) ((fun e ↦ (H ⟨↑e, ⋯⟩).2) e)))).1 =
    ↑(H (Set.inclusion ⋯ e)).1

Tactic:
simpa [hH] using e.2.symm

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

Goal state before:
pp: 𝕜 : 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
x : A
⊢ ∀ (y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊

Tactic:
y

Goal state after:
𝕜 : 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
x y : A
⊢ ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ IsEvenlyCovered f x I

Tactic:
by convert! h.homeomorph_comp g.symm <;> ((try ext); simp)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : IsTopologicalRing 𝕜
p : 𝕜
inst✝² : T0Space (AddCircle p)
inst✝¹ : Algebra ℚ 𝕜
n : ℕ
inst✝ : NeZero n
⊢ IsUnit ↑n

Tactic:
convert! (Nat.cast_ne_zero.mpr <| NeZero.ne n).isUnit.map (algebraMap ℚ 𝕜)

Goal state after:
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : IsTopologicalRing 𝕜
p : 𝕜
inst✝² : T0Space (AddCircle p)
inst✝¹ : Algebra ℚ 𝕜
n : ℕ
inst✝ : NeZero n
⊢ ↑n = (algebraMap ℚ 𝕜) ↑n
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:
log,

Goal state after:
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
⊢ cfc Real.log (r • a) = (algebraMap ℝ A) (Real.log r) + log a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

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

Tactic:
log,

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc Real.log (a ^ n) = n • log a
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
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ log (exp a) = a

Tactic:
log,

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc Real.log (exp a) = a
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
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc Real.exp (log a) = a

Tactic:
log,

Goal state after:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ cfc Real.exp (cfc Real.log a) = a
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ IsLeast ((fun a ↦ Real.cos a) '' spectrum ℝ ↑x) (Real.cos ‖x‖)

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ Real.cos ‖x‖ ∈ (fun a ↦ Real.cos a) '' spectrum ℝ ↑x

case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ Real.cos ‖x‖ ∈ lowerBounds ((fun a ↦ Real.cos a) '' spectrum ℝ ↑x)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = ‖↑u - 1‖ ^ 2

Tactic:
by
  conv_rhs => rw [← expUnitary_argSelfAdjoint hu]
  exact Eq.symm <| norm_sq_expUnitary_sub_one <| norm_argSelfAdjoint_le_pi u

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

Tactic:
by
  obtain (_ | _) := subsingleton_or_nontrivial A
  · simp [Subsingleton.elim (a + I • CFC.sqrt (1 - a ^ 2)) 1, one_mem (unitary A)]
  have key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x : ℂ ↦ x.re + I * √(1 - x.re ^ 2)) a := by
    rw [CFC.sqrt_eq_real_sqrt (1 - a ^ 2) ?nonneg]
    case nonneg =>
      rwa [sub_nonneg, ← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2), sq, ha.norm_mul_self,
        sq_le_one_iff₀ (by positivity)]
    rw [cfc_add .., cfc_const_mul .., ← cfc_real_eq_complex (fun x ↦ x) ha, cfc_id' ℝ a,
      ← cfc_real_eq_complex (fun x ↦ √(1 - x ^ 2)) ha, cfcₙ_eq_cfc, cfc_comp' (√·) (1 - · ^ 2) a,
      cfc_sub .., cfc_pow .., cfc_const_one .., cfc_id' ..]
  rw [key, cfc_unitary_iff ..]
  intro x hx
  rw [← starRingEnd_apply, ← Complex.normSq_eq_conj_mul_self,
    Complex.normSq_ofReal_add_I_mul_sqrt_one_sub, Complex.ofReal_one]
  exact spectrum.norm_le_norm_of_mem (ha.spectrumRestricts.apply_mem hx) |>.trans ha_norm

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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪(adjoint B) x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
adjoint_inner_left

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
B : F →L[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪x, B y⟫_𝕜 = ⟪x, B y⟫_𝕜
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

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

Tactic:
exact iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx

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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ Function.Injective (⇑T ∘ ⇑(adjoint T)) ↔ Function.Injective ⇑(adjoint T)

Tactic:
simpa using T†.adjoint_comp_self_injective_iff

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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ∀ (y : F), ((innerₛₗ 𝕜).flip (A x)) y = ((innerₛₗ 𝕜).flip x) ((adjoint A) y)

Tactic:
y

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
y : F
⊢ ((innerₛₗ 𝕜).flip (A x)) y = ((innerₛₗ 𝕜).flip x) ((adjoint A) y)
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
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x : E
⊢ ∀ (y : E), ⟪↑A x, y⟫_𝕜 = ⟪x, ↑A y⟫_𝕜

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x y : E
⊢ ⟪↑A x, y⟫_𝕜 = ⟪x, ↑A 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
v : E
w : F
⊢ ⟪(adjoint A) w, v⟫_𝕜 = ⟪w, A v⟫_𝕜

Tactic:
adjoint_inner_left

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
v : E
w : F
⊢ ⟪w, A v⟫_𝕜 = ⟪w, A v⟫_𝕜
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
B : F →ₗ[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪(adjoint B) x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
adjoint_inner_left

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
B : F →ₗ[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪x, B y⟫_𝕜 = ⟪x, B y⟫_𝕜
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
h : s.centroid ∈ affineSpan k (s.points '' t)
hssubset : t ⊂ Set.univ
⊢ False

Tactic:
obtain ⟨i, hi⟩ := Set.exists_of_ssubset hssubset

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
h : s.centroid ∈ affineSpan k (s.points '' t)
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : i ∈ Set.univ ∧ i ∉ t
⊢ False
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
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι₁
y : ι₂
⊢ ⟪(adjoint B) (b₁ x), b₂ y⟫_𝕜 = ⟪b₁ x, B (b₂ y)⟫_𝕜

Tactic:
adjoint_inner_left

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
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι₁
y : ι₂
⊢ ⟪b₁ x, B (b₂ y)⟫_𝕜 = ⟪b₁ x, B (b₂ 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
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : F
⊢ ⟪(adjoint B) (b x), y⟫_𝕜 = ⟪b x, B y⟫_𝕜

Tactic:
adjoint_inner_left

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
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : F
⊢ ⟪b x, B y⟫_𝕜 = ⟪b x, B 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
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : E
⊢ ⟪(adjoint B) y, b x⟫_𝕜 = ⟪y, B (b x)⟫_𝕜

Tactic:
adjoint_inner_left

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
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : E
⊢ ⟪y, B (b x)⟫_𝕜 = ⟪y, B (b 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
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
  ext x
  exact ext_inner_right_basis b fun i => by simp only [h i, adjoint_inner_left]

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
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
x : E
⊢ ∀ (y : F), ((innerₛₗ 𝕜).flip (A x)) y = ((innerₛₗ 𝕜).flip x) ((adjoint A) y)

Tactic:
y

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
⊢ ((innerₛₗ 𝕜).flip (A x)) y = ((innerₛₗ 𝕜).flip x) ((adjoint A) y)
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
⊢ ∀ (y : E), ⟪(adjoint T * T) x, y⟫_𝕜 = ⟪x, (adjoint T * T) y⟫_𝕜

Tactic:
y

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 y : E
⊢ ⟪(adjoint T * T) x, y⟫_𝕜 = ⟪x, (adjoint T * T) y⟫_𝕜
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)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) = ((↑n + 1) * ((↑n)⁻¹ - (↑n + 1)⁻¹)) • ∑ x, (s.points x -ᵥ s.points i)

Tactic:
congr

Goal state after:
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ = (↑n + 1) * ((↑n)⁻¹ - (↑n + 1)⁻¹)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n * ((↑n + 1)⁻¹ - (↑n)⁻¹)) • ∑ x, (s.points x -ᵥ s.points i) = -(↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)

Tactic:
congr

Goal state after:
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ↑n * ((↑n + 1)⁻¹ - (↑n)⁻¹) = -(↑n + 1)⁻¹
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i = (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid

Tactic:
by
  rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
i : ↥s'
hi : p ∈ s.median ↑i
⊢ p -ᵥ s.centroid ∈ k ∙ u i

Tactic:
grind only [median_eq_line_point_centroid, vadd_right_mem_affineSpan_pair,
      Submodule.smul_mem, Submodule.mem_span_singleton_self]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent k fun i ↦ (if ↑i = i₀ then s.centroid else s.points ↑i) -ᵥ if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x // x ≠ i₀ } :=
  have h := ⋯;
  fun x ↦ ⟨↑x, ⋯⟩
x : ↥{i₀}ᶜ
⊢ ∀ ⦃a₂ : ↥{i₀}ᶜ⦄, f x = f a₂ → x = a₂

Tactic:
y

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent k fun i ↦ (if ↑i = i₀ then s.centroid else s.points ↑i) -ᵥ if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x // x ≠ i₀ } :=
  have h := ⋯;
  fun x ↦ ⟨↑x, ⋯⟩
x y : ↥{i₀}ᶜ
⊢ f x = f y → x = y
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inr
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 : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]
    refine (Submodule.finrank_add_le_finrank_add_finrank _ _).trans ?_
    gcongr
    refine finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_
    have h := v.property
    rw [Submodule.mem_span_singleton] at h
    rcases h with ⟨c, hc⟩
    refine ⟨c, ?_⟩
    ext
    exact hc

Goal state after:
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
hp : 0 < p.toReal
hf : Memℓp f p
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ∑' (i : α), ‖f i‖ ^ p.toReal

Tactic:
simp only [Memℓp, hp₁.ne', ↓reduceIte, hp₂.ne] at hf

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
⊢ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ∑' (i : α), ‖f i‖ ^ p.toReal