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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
← sameRay_or_sameRay_neg_iff_not_linearIndependent

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
⊢ StarConvex 𝕜 x s

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
⊢ y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
⊢ StarConvex 𝕜 x s

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
⊢ y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s

Tactic:
rw [smul_zero, zero_add]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b • x ∈ s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
⊢ y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mk.mk
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
carrier✝¹ : Set P
smul_vsub_vadd_mem'✝¹ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝¹ → p₂ ∈ carrier✝¹ → p₃ ∈ carrier✝¹ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝¹
carrier✝ : Set P
smul_vsub_vadd_mem'✝ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝ → p₂ ∈ carrier✝ → p₃ ∈ carrier✝ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝
x✝ :
  { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ }.carrier =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ } =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }

Tactic:
congr

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
⊢ [x -[𝕜] y] = Icc (min x y) (max x y)

Tactic:
rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
⊢ StarConvex 𝕜 x ((fun x ↦ z + x) ⁻¹' s)

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
⊢ y ∈ (fun x ↦ z + x) ⁻¹' s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
⊢ StarConvex 𝕜 x (Iio r)

Tactic:
y

Goal state after:
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
⊢ y ∈ Iio r → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ Iio r
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
p : P
hp : p ∈ s
v : V
| ∃ x ∈ ↑s, x -ᵥ p = -v

Tactic:
congr

Goal state after:
case p
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
v : V
| fun x ↦ x ∈ ↑s ∧ x -ᵥ p = -v
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex R x s

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
⊢ y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
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
p : P
hp : p ∈ s
v : V
⊢ (∃ x ∈ ↑s, x -ᵥ p = -v) ↔ ∃ x ∈ ↑s, p -ᵥ x = v

Tactic:
conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
⊢ Absorbs M s ∅

Tactic:
simp [Absorbs]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Bornology M
inst✝¹ : SMul M α
s t : Set α
inst✝ : BoundedSpace M
⊢ Absorbs M s t

Tactic:
simp [Absorbs]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t₁ t₂ : Set α
⊢ Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂

Tactic:
simp [Absorbs]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝³ : Monoid M
inst✝² : AddGroup E
inst✝¹ : DistribMulAction M E
inst✝ : Bornology M
s t : Set E
⊢ Absorbs M (-s) (-t) ↔ Absorbs M s t

Tactic:
simp [Absorbs]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0 ⊔ pure 0, MapsTo (fun x ↦ c • x) t s

Tactic:
Filter.eventually_sup,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔
    (∀ᶠ (x : 𝕜) in 𝓝[≠] 0, MapsTo (fun x_1 ↦ x • x_1) t s) ∧ ∀ᶠ (x : 𝕜) in pure 0, MapsTo (fun x_1 ↦ x • x_1) t s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ StarConvex 𝕜 x {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
y : E
⊢ y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s} →
    ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)

Tactic:
isVonNBounded_iff_tendsto_smallSets_nhds,

Goal state after:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ Tendsto (fun x ↦ x • S) (𝓝 0) (𝓝 0).smallSets ↔ ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝ : x ∈ univ
⊢ ∀ ⦃y : E⦄, y ∈ univ → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝ : x ∈ univ
y : E
⊢ y ∈ univ → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
⊢ ∀ ⦃y : E⦄,
    y ∈ s ∩ t → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (s ∩ t)) x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
⊢ y ∈ s ∩ t → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (s ∩ t)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
⊢ y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ (fun x ↦ z + x) ⁻¹' s →
      x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior ((fun x ↦ z + x) ⁻¹' s)) x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
⊢ y ∈ (fun x ↦ z + x) ⁻¹' s →
    x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior ((fun x ↦ z + x) ⁻¹' s)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
⊢ y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y
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
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x ↦ p i0 -ᵥ x) ∘ p)) = Submodule.span k (range fun i ↦ p i0 -ᵥ p i)

Tactic:
congr

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
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x ↦ x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i ↦ p i -ᵥ p i0)

Tactic:
congr

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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ ∑ i ∈ s, w₁ i • (p i -ᵥ p j) = ∑ i ∈ s, w₂ i • (p i -ᵥ p j)

Tactic:
congr

Goal state after:
case e_f
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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (fun i ↦ w₁ i • (p i -ᵥ p j)) = fun i ↦ w₂ i • (p i -ᵥ p j)
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
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr

Goal state after:
case s
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
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
| s

case f
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
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
| fun x ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y ≤ f z
⊢ f z ≤ f x

Tactic:
by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz

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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr

Goal state after:
case a
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂

case a
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case a
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr

Goal state after:
case a.s
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| s

case a.f
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| fun x ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄,
    y ∈ s →
      ∀ ⦃a b : 𝕜⦄,
        0 ≤ a →
          0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
⊢ y ∈ s →
    ∀ ⦃a b : 𝕜⦄,
      0 ≤ a → 0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
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
toFun✝¹ : E → ℝ
map_zero'✝¹ : toFun✝¹ 0 = 0
add_le'✝¹ : ∀ (r s : E), toFun✝¹ (r + s) ≤ toFun✝¹ r + toFun✝¹ s
neg'✝¹ : ∀ (r : E), toFun✝¹ (-r) = toFun✝¹ r
smul'✝¹ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹ }.toFun x
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le'✝ : ∀ (r s : E), toFun✝ (r + s) ≤ toFun✝ r + toFun✝ s
neg'✝ : ∀ (r : E), toFun✝ (-r) = toFun✝ r
smul'✝ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹, smul' := smul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹, smul' := smul'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ }

Tactic:
congr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a →
              0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
y

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a →
              0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
y : E
⊢ y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y