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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfc x a) ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
range_cfc_nnreal_eq_image_cfc_real a ha,

Goal state after:
A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x} ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} ⊆ Set.range fun x ↦ cfc x a

Tactic:
range_cfc_nnreal_eq_image_cfc_real a ha,

Goal state after:
A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} ⊆ (fun x ↦ cfc x a) '' {f | ∀ x ∈ spectrum ℝ a, 0 ≤ f x}
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
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖v‖ * ‖(toCLM Mᴴ) ((toCLM M) v)‖ ≤ ‖v‖ * (‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖)

Tactic:
gcongr

Goal state after:
case hbc
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
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖(toCLM Mᴴ) ((toCLM M) v)‖ ≤ ‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖
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
v : C⋆ᵐᵒᵈ(A, n → A)
h₁ : ‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ ‖M * star M‖ * ‖v‖ ^ 2
h₂ : ‖v‖ = √(‖v‖ ^ 2)
⊢ √‖⟪v, (toCLM Mᴴ) ((toCLM M) v)⟫_A‖ ≤ √(‖M * star M‖ * ‖v‖ ^ 2)

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_1.a
𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x ∈ update x i '' openSegment 𝕜 x₁ x₂

Tactic:
exact ⟨_, hi, update_eq_self _ _⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A

Tactic:
rintro ⟨hxA, hAx⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
⊢ x ∈ extremePoints 𝕜 A
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x

Tactic:
convex_iff_segment_subset

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : NormMulClass 𝕜
inst✝ : NormOneClass 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ sphere 0 1
hy : b✝ ∈ sphere 0 1
⊢ a✝ * b✝ ∈ sphere 0 1

Tactic:
mem_sphere_zero_iff_norm

Goal state after:
𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : NormMulClass 𝕜
inst✝ : NormOneClass 𝕜
a✝ b✝ : 𝕜
hx : ‖a✝‖ = 1
hy : ‖b✝‖ = 1
⊢ ‖a✝ * b✝‖ = 1
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
b : B
hb : b ∉ e.baseSet
y : F
⊢ e.symm b y = Classical.arbitrary (E b)

Tactic:
by
  simp [Pretrivialization.symm, hb]

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
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))

Tactic:
by
  refine Prod.ext ?_ rfl
  rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁]
  · rwa [e₁.proj_symm_apply' h₁]
  · rwa [e₁.proj_symm_apply' h₁]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ f.toPartialEquiv.2 '' (f.target ∩ ↑f.symm ⁻¹' U) = f.source ∩ U

Tactic:
apply (f.symm_image_target_inter_eq _).trans
      rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]

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)
n : ℤ
hn : IsUnit ↑n
x✝ : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, (fun x ↦ n • x) x✝ = (fun x ↦ n • x) a₂ → x✝ = a₂

Tactic:
simp_rw [zsmul_eq_mul]

Goal state after:
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℤ
hn : IsUnit ↑n
x✝ : 𝕜
⊢ ∀ ⦃a₂ : 𝕜⦄, ↑n * x✝ = ↑n * a₂ → x✝ = 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
⊢ exp (log a) = a

Tactic:
rw [← real_exp_eq_normedSpace_exp .log, log, ← cfc_comp' Real.exp Real.log a (by fun_prop)]

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 (fun x ↦ Real.exp (Real.log x)) a = a
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ 2 * (1 - b✝) ≤ 2 * (1 - a✝¹)

Tactic:
gcongr

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

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
x : ℝ
hx : IsLeast (re '' spectrum ℂ u) x
⊢ 2 ^ 2 ≤ 2 * (1 - x) → -1 ∈ spectrum ℂ u

Tactic:
obtain ⟨z, hz, rfl⟩ := hx.1

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
⊢ 2 ^ 2 ≤ 2 * (1 - z.re) → -1 ∈ spectrum ℂ u
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
⊢ 2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π)

Tactic:
gcongr

Goal state after:
case h
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ Real.cos π < Real.cos ‖x‖
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)‖ ≤ 1 * ‖↑(argSelfAdjoint u)‖

Tactic:
gcongr

Goal state after:
case hbc
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ t ≤ 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
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖t • argSelfAdjoint u‖) ≤ 2 * (1 - Real.cos ‖argSelfAdjoint u‖)

Tactic:
gcongr

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

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

Tactic:
gcongr

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
⊢ ‖(adjoint A ∘SL A) x‖ * ‖x‖ ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖

Tactic:
gcongr

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.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)
⊢ s.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i

Tactic:
vsub_vadd

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
i : Fin (n + 1)
⊢ s.centroid = s.centroid
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 = (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i

Tactic:
vsub_vadd

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 : Fin (n + 1)
⊢ s.faceOppositeCentroid i = s.faceOppositeCentroid 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)
⊢ s.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i

Tactic:
vsub_vadd

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 : Fin (n + 1)
⊢ s.centroid = s.centroid
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
⊢ p = (p -ᵥ s.centroid) +ᵥ s.centroid

Tactic:
vsub_vadd

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
⊢ p = p
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) t)).Nonempty
⊢ interior ((convexHull ℝ) t) ⊆ interior ((convexHull ℝ) s)

Tactic:
gcongr

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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₁, p₂, p₃, p₄} ⊆ {p₁, p₂, p₃, p₄, p₅}

Tactic:
gcongr

Goal state after:
case h
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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₄} ⊆ {p₄, p₅}
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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₁, p₂, p₃} ⊆ {p₁, p₂, p₃, p₄}

Tactic:
gcongr

Goal state after:
case h
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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ {p₃} ⊆ {p₃, p₄}
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 ↥(k ∙ (p -ᵥ p₀)) + finrank k ↥s.direction ≤ 1 + finrank k ↥s.direction

Tactic:
gcongr

Goal state after:
case h₁
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 ↥(k ∙ (p -ᵥ p₀)) ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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

Tactic:
vsub_vadd

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : CharZero k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i = s.points i
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
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖f i‖ ^ p.toReal ≤ ‖g i‖ ^ p.toReal

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖f i‖ ≤ ‖g i‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
C : ℝ
hC : C ∈ upperBounds ((fun i ↦ ‖f i‖) '' {i | f i ≠ 0})
⊢ BddAbove (Set.range fun i ↦ ‖f i‖)

Tactic:
use max 0 C

Goal state after:
case h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ∞
C : ℝ
hC : C ∈ upperBounds ((fun i ↦ ‖f i‖) '' {i | f i ≠ 0})
⊢ max 0 C ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
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 g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + g) p

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_
    simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_ofPred_eq]
    contrapose!
    rintro ⟨hf', hg'⟩
    simp [hf', hg']
  · apply memℓp_infty
    obtain ⟨A, hA⟩ := hf.bddAbove
    obtain ⟨B, hB⟩ := hg.bddAbove
    refine ⟨A + B, ?_⟩
    rintro a ⟨i, rfl⟩
    exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))
  apply memℓp_gen
  let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)
  refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)
  · intro; positivity
  · refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_
    dsimp only [C]
    split_ifs with h
    · simpa using! NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)
    · let F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
      simp only [not_lt] at h
      simpa [Fin.sum_univ_succ] using!
        Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

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

Tactic:
gcongr

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

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
i : α
⊢ ‖c • f i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f i‖₊) ^ p.toReal

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun a ↦ (‖c‖₊ * ‖f a‖₊) ^ p.toReal
i : α
⊢ ‖c • f i‖₊ ≤ ‖c‖₊ * ‖f i‖₊
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
i : α
⊢ ‖↑(f + g) i‖ ^ p.toReal ≤ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
i : α
⊢ ‖↑(f + g) i‖ ≤ ‖↑f i‖ + ‖↑g i‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
i : α
hp : ∞ ≠ 0
f : ↥(lp E ∞)
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
have : Nonempty α := ⟨i⟩
    exact (isLUB_norm f).1 ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hRHS : HasSum (fun a ↦ ‖c‖₊ ^ p.toReal * ‖↑f a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun a ↦ ‖↑(c • f) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖c • ↑f i‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖↑f i‖₊) ^ p.toReal

Tactic:
gcongr

Goal state after:
case h₁
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hRHS : HasSum (fun a ↦ ‖c‖₊ ^ p.toReal * ‖↑f a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun a ↦ ‖↑(c • f) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
i : α
⊢ ‖c • ↑f i‖₊ ≤ ‖c‖₊ * ‖↑f i‖₊