mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
inst✝⁴ : CommRing R
inst✝³ : Module R V₁
inst✝² : Module R V₂
inst✝¹ : Module R V₃
inst✝ : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x✝¹ : P₁ →ᵃ[R] P₃
x✝ : P₁ →ᵃ[R] V₃
p✝ : P₂
⊢ ((e₁.arrowCongrEquiv e₂) (x✝ +ᵥ x✝¹)) p✝ = ((e₁.arrowCongrₗ e₂.linear) x✝ +ᵥ (e₁.arrowCongrEquiv e₂) x✝¹) p✝

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k W)).toFun (x✝¹ + x✝)) p✝ =
    ((e.arrowCongrEquiv (refl k W)).toFun x✝¹ + (e.arrowCongrEquiv (refl k W)).toFun x✝) p✝

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁷ : Ring k
inst✝¹⁶ : AddCommGroup V₁
inst✝¹⁵ : AddCommGroup V₂
inst✝¹⁴ : AddCommGroup V₃
inst✝¹³ : AddCommGroup V₄
inst✝¹² : Module k V₁
inst✝¹¹ : Module k V₂
inst✝¹⁰ : Module k V₃
inst✝⁹ : Module k V₄
inst✝⁸ : AffineSpace V₁ P₁
inst✝⁷ : AffineSpace V₂ P₂
inst✝⁶ : AffineSpace V₃ P₃
inst✝⁵ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁴ : Ring R
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module R W
inst✝ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x✝¹ : R
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k W)).toFun (x✝¹ • x✝)) p✝ =
    ((RingHom.id R) x✝¹ • (e.arrowCongrEquiv (refl k W)).toFun x✝) p✝

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹)) p✝ = ((congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹) p✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
Hx : x = x - c + c
Hy : y = y - c + c
p0 : 0 ≤ 0
p1 : 0 ≤ 1
q0 : 0 ≤ 0
q1 : 0 ≤ 1
H : (1 - 0) • c + (0 • (y - c) + 0 • c) = (1 - 0) • c + (0 • (x - c) + 0 • c)
this : c + 0 • (y - c) = c + 0 • (x - c)
⊢ (1 - 0) • c + 0 • x ∈ {c}

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : ∅.Subsingleton
⊢ vectorSpan k ∅ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
h : {p}.Subsingleton
⊢ vectorSpan k {p} = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
s : AffineSubspace k P
⊢ p ∈ ↑s ↔ p ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
h : x ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) x 0 = x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p = -v +ᵥ v +ᵥ p

Tactic:
simp

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

Goal state before:
pp: case inr
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Tactic:
calc
    a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le
        (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
    _ = r := Convex.combo_self hab _

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ ↑s.direction

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
⊢ p ∈ mk' p direction

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Semiring 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : PartialOrder 𝕜
𝕜' : Type u_5
inst✝⁵ : Semiring 𝕜'
inst✝⁴ : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomSurjective σ
F' : Type u_6
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜' F'
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : 0 ≤ σ r
t : 𝕜
hb : 0 ≤ σ t
hab : σ r + σ t = 1
⊢ f (r • x + t • y) = σ r • f x + σ t • f y

Tactic:
simp

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

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ (0 + 0) • x = 0 • x + 0 • y

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : (↑⊤).Nonempty
⊢ ⊤.direction = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ ‖-1‖ ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ ‖-1‖ ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}

Tactic:
obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
⊢ ∃ p, ↑s₁ ∩ ↑s₂ = {p}
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
by
  by_cases h : (0 : E) ∈ U
  · rw [balancedCore_eq_iInter h]
    refine isClosed_iInter fun a => ?_
    refine isClosed_iInter fun ha => ?_
    have ha' := lt_of_lt_of_le zero_lt_one ha
    rw [norm_pos_iff] at ha'
    exact isClosedMap_smul_of_ne_zero ha' U hU
  · have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
    rw [this]
    exact isClosed_empty

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
hr : ‖0‖ ≤ 1
⊢ ‖1‖ ≤ 1 ∧ 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ affineSpan k s ≤ ↑(Submodule.span k s)

Tactic:
by
  intro x hx
  simp only [Submodule.mem_toAffineSubspace]
  induction hx using affineSpan_induction' with
  | mem x hx => exact Submodule.subset_span hx
  | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
    simp only [vsub_eq_sub, vadd_eq_add]
    apply Submodule.add_mem _ _ hw
    exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedDivisionRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
S V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V

Tactic:
simp only [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV), mapsTo_iff_image_subset,
    image_smul]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), toFun x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G {x | x.2 / x.1 ∈ b x✝¹}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ UniformEquicontinuous (DFunLike.coe ∘ F)

Tactic:
uniformEquicontinuous_iff_uniformContinuous

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Field 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (0 • s)

pp: case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Field 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)

Tactic:
· exact (subsingleton_zero_smul_set _).strictConvex

Goal state after:
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Field 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ 1 = (1 - t) * 1 + t * 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t * 1 = t * 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p -ᵥ p₂ = p -ᵥ p₂_1) ↔ p₂ ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ univ = {p}

Tactic:
← subsingleton_iff_singleton (mem_univ p),

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ univ.Subsingleton
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' +ᵥ p ∈ {p} ∪ (fun v ↦ v +ᵥ p) '' s ∧ (fun x ↦ x -ᵥ p) (↑v' +ᵥ p) = ↑v'

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝⁸ : SeminormedRing 𝕜
inst✝⁷ : AddGroup E
inst✝⁶ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
inst✝⁵ : SMul R ℝ
inst✝⁴ : SMul R ℝ≥0
inst✝³ : IsScalarTower R ℝ≥0 ℝ
inst✝² : Preorder R
inst✝¹ : Zero R
inst✝ : IsOrderedModule R ℝ
p q : Seminorm 𝕜 E
hpq : p ≤ q
c : R
x : E
⊢ (c • p) x ≤ (c • 1) • p x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p -ᵥ p) = s₁.direction ⊔ s₂.direction

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝⁸ : SeminormedRing 𝕜
inst✝⁷ : AddGroup E
inst✝⁶ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
inst✝⁵ : SMul R ℝ
inst✝⁴ : SMul R ℝ≥0
inst✝³ : IsScalarTower R ℝ≥0 ℝ
inst✝² : Preorder R
inst✝¹ : Zero R
inst✝ : IsOrderedModule R ℝ
p q : Seminorm 𝕜 E
hpq : p ≤ q
c : R
x : E
⊢ (c • 1) • q x ≤ (c • q) x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ s.direction ⊔ vectorSpan k {p₂} ⊔ k ∙ (p₂ -ᵥ p₁) = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
simp

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

Goal state before:
pp: case e_a.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ i2 ∈ {i}, i2 ≠ i → (-w) i2 = 0

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w = p i

Tactic:
by
  classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case inl
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ map f (affineSpan k ∅) = affineSpan k (⇑f '' ∅)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ x' ∈ univ

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ y' ∈ univ

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i ∈ map (Function.Embedding.subtype fun x ↦ x ∈ s) fs, (fun i ↦ if h : i ∈ s then w ⟨i, h⟩ else 0) i = ∑ i ∈ fs, w i

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i ∈ fs, w i • (p ↑i -ᵥ b) =
    ∑ i ∈ map (Function.Embedding.subtype fun x ↦ x ∈ s) fs, (fun i ↦ if h : i ∈ s then w ⟨i, h⟩ else 0) i • (p i -ᵥ b)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
r : P₁
hr : r -ᵥ p ∈ direction
⊢ f.linear (r -ᵥ p) = f r -ᵥ f p

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ x' ∈ univ

Tactic:
simp

Goal state after: