mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n) - f (2 * n + 1)

Tactic:
le_sub_iff_add_le

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n + 1) ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩,
    sin_neg, neg_le_neg_iff]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x

Tactic:
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]

Goal state after:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x

case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x

case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - x ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
⊢ Tendsto (fun x ↦ arccos (f x)) l (𝓝[≤] arccos x)

Tactic:
refine ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
  push _ ∈ _ at hy ⊢
  exact antitone_arccos hy

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ rexp 1 * x ≤ rexp x

Tactic:
by_cases hx0 : x ≤ 0
  · apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)
  · have h := add_one_le_exp (log x)
    rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_ge hx0), mul_comm] at h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log (x / x) = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
⊢ log (0 / 0) = 0

case inr
x : ℝ
hx : x ≠ 0
⊢ log (x / x) = 0
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case inr
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ g x ∈ closedBall 0 ε

Tactic:
calc
    _ = ‖g x‖ := by simp
    _ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
    _ ≤ c / (c / ε) := by gcongr
    _ = ε := div_div_cancel₀ hc0.ne'

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖(f₁ x - f₂ x) • g x‖) l (𝓝 0)

Tactic:
norm_smul

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖f₁ x - f₂ x‖ * ‖g x‖) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (x / x).arg = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
⊢ (0 / 0).arg = 0

case inr
x : ℂ
hx : x ≠ 0
⊢ (x / x).arg = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (cexp x) = x

Tactic:
rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1

Tactic:
le_sub_iff_add_le

Goal state after:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * -I) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -(↑(Real.log ‖x‖) + ↑x.arg * -I) else -(↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
neg_add,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * -I) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + -(↑x.arg * -I) else -↑(Real.log ‖x‖) + -(↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

Tactic:
rw [← prod_map_toList, log_list_prod (by simp_all)]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ (List.map (fun x ↦ log x) (List.map (fun i ↦ f i) s.toList)).sum = ∑ i ∈ s, log (f i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
two_nsmul_eq_pi_iff

Goal state after:
θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = ↑(-π / 2) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
· simp [Set.preimage, h]

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

Goal state before:
pp: x : ℂ
⊢ x⁻¹.arg = if x.arg = π then π else -x.arg

Tactic:
rw [← arg_conj, inv_def, mul_comm]
  by_cases hx : x = 0
  · simp [hx]
  · exact arg_real_mul (conj x) (by simp [hx])

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

Goal state before:
pp: case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ ↑a ^ r * cexp (log ↑b * r) = ↑a ^ r * ↑b ^ r

Tactic:
← cpow_def_of_ne_zero hb''

Goal state after:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ ↑a ^ r * ↑b ^ r = ↑a ^ r * ↑b ^ r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = 0 ↔ θ = 0

Tactic:
← toReal_zero

Goal state after:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0
Module: Mathlib.Tactic.Qify

Goal state before:
pp: a b : ℤ
⊢ a ≠ b ↔ ↑a ≠ ↑b

Tactic:
by
  simp only [ne_eq, Int.cast_inj]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin

Tactic:
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a : Angle
h : 2 • a = 2 • a
h_ne : 0 ≠ 0
h1 : a = a ∨ a = a + ↑π
h_sign : a.sign = 0
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
h' : a = b + ↑π
h_sign' : b.sign = 0
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
this : a.sign = -b.sign
⊢ a = b

Tactic:
have := congr_arg (· = b.sign) this

Goal state after:
case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
this✝ : a.sign = -b.sign
this : (a.sign = b.sign) = (-b.sign = b.sign)
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log (-x) * y) * cos (y * π) +
      ((↑(rexp (log (-x) * y) * sin (y * π))).re * 0 - (↑(rexp (log (-x) * y) * sin (y * π))).im * Complex.I.im) =
    rexp (log x * y) * cos (y * π)

Tactic:
Complex.ofReal_im,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log (-x) * y) * cos (y * π) + ((↑(rexp (log (-x) * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ x ^ y) atTop atTop

Tactic:
by
  rw [Filter.tendsto_atTop_atTop]
  intro b
  obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b
  use c.toNNReal
  intro a ha
  exact mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
⊢ 0 x ≤ g x → ‖f x‖ ≤ c * ‖g x‖ → ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖

Tactic:
hgx

Goal state after:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
⊢ ‖f x‖ ≤ c * ‖g x‖ → ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun n ↦ ↑n ^ c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)
  filter_upwards [eventually_ge_atTop 1] with t ht
  replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr ht
  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]
  exact Real.rpow_le_rpow_of_exponent_le ht h

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x‖ ^ y.re / rexp ((↑x).arg * y.im) = x ^ y.re

Tactic:
simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑x = 0 → y.re = 0 → y = 0

Tactic:
simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
⊢ 0 ^ y = if y = 0 then 1 else 0

Tactic:
split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod

ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ (Multiset.map (fun x ↦ f x ^ r) s).prod = (Multiset.map f s).prod ^ r

Tactic:
obtain ⟨l⟩ := s

Goal state after:
case mk
ι : Type u_1
s : Multiset ι
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, 0 ≤ f i
⊢ (Multiset.map (fun x ↦ f x ^ r) (Quot.mk (⇑(List.isSetoid ι)) l)).prod =
    (Multiset.map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

Tactic:
rwa [arg_nonneg_iff]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ -(⅟2 • (p₁ -ᵥ p) + ⅟2 • (p₂ -ᵥ p)) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
neg_add,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p : P
⊢ -(⅟2 • (p₁ -ᵥ p)) + -(⅟2 • (p₂ -ᵥ p)) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inl
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
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -m 1 • y

Tactic:
neg_smul

Goal state after:
case neg.refine_2.inr.inr.inl
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
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -(m 1 • y)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
⊢ insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y]

Tactic:
by
  simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment,
    openSegment_subset_segment, true_and]
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_
  · rintro rfl
    rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
  · rintro rfl
    rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
  · exact ⟨a, b, ha', hb', hab, rfl⟩

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
x y x✝¹ : E
x✝ : x✝¹ ∈ [x -[𝕜] y]
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = x✝¹
⊢ (fun θ ↦ (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

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
x y x✝¹ : E
x✝ : x✝¹ ∈ openSegment 𝕜 x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = x✝¹
⊢ (fun θ ↦ (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

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
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
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
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ x_1, (∃ x ∈ Icc 0 1, (AffineMap.lineMap a b) x = x_1) ∧ f x_1 = x) ↔
    ∃ x_1 ∈ Icc 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x

Tactic:
exists_exists_and_eq_and,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ a_1 ∈ Icc 0 1, f ((AffineMap.lineMap a b) a_1) = x) ↔ ∃ x_1 ∈ Icc 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ x_1, (∃ x ∈ Ioo 0 1, (AffineMap.lineMap a b) x = x_1) ∧ f x_1 = x) ↔
    ∃ x_1 ∈ Ioo 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x

Tactic:
exists_exists_and_eq_and,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ a_1 ∈ Ioo 0 1, f ((AffineMap.lineMap a b) a_1) = x) ↔ ∃ x_1 ∈ Ioo 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 1 = id k P1

Tactic:
ext p
  simp [homothety_apply]

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 0 = const k P1 c

Tactic:
ext p
  simp [homothety_apply]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div, div_self hab.ne']

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div, div_self hab.ne']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ (a + b) • x - a • y < b • x

Tactic:
rw [add_smul, sub_lt_iff_lt_add']

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ a • x + b • x < a • y + b • x
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s

Tactic:
starConvex_iff_segment_subset,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ (∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x 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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

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
⊢ Submodule.span k (↑(s₁ ⊓ s₂) -ᵥ ↑(s₁ ⊓ s₂)) ≤ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊓ Submodule.span k (↑s₂ -ᵥ ↑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
S : AffineSpace V P
t : Set (AffineSubspace k P)
⊢ (sInf t).direction ≤ ⨅ s ∈ t, s.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

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
t : Set (AffineSubspace k P)
⊢ Submodule.span k (↑(sInf t) -ᵥ ↑(sInf t)) ≤ ⨅ s ∈ t, Submodule.span k (↑s -ᵥ ↑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
S : AffineSpace V P
t : Set (AffineSubspace k P)
⊢ (sInf t).direction ≤ ⨅ s ∈ t, s.direction

Tactic:
by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

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
h : s₁ ≤ s₂
⊢ s₁.direction ≤ s₂.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

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
h : s₁ ≤ s₂
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ≤ Submodule.span k (↑s₂ -ᵥ ↑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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

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
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊔ Submodule.span k (↑s₂ -ᵥ ↑s₂) ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ 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
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k ps

Tactic:
Set.insert_eq_of_mem h,

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
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k ↑(affineSpan k ps) = affineSpan k ps