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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -1 * (-1) ^ (2 * n) * f (2 * n + 1) +
      -1 * (-1 * (-1) ^ (2 * n)) * f (2 * n + 1 + 1)

Tactic:
show (-1 : E) ^ (2 * n) = 1 by simp,

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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -1 * 1 * f (2 * n + 1) + -1 * (-1 * 1) * f (2 * n + 1 + 1)
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 + (-1) ^ (2 * n) * f (2 * n) + -1 * (-1) ^ (2 * n) * f (2 * n + 1)

Tactic:
show (-1 : E) ^ (2 * n) = 1 by simp,

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 ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + 1 * f (2 * n) + -1 * 1 * f (2 * n + 1)
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 : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -1 * (-1) ^ (2 * n) * f (2 * n + 1) +
      -1 * (-1 * (-1) ^ (2 * n)) * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
show (-1 : E) ^ (2 * n) = 1 by simp,

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 : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -1 * 1 * f (2 * n + 1) + -1 * (-1 * 1) * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x

Tactic:
subst y
  exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

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

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ arcsin (-1) = -(π / 2)

Tactic:
arcsin_neg_one

Goal state after:
x : ℝ
hx : x ≤ -1
⊢ -(π / 2) = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _),

Goal state after:
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ x ≤ sin y ↔ x ≤ sin (arcsin (sin y))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ ↑π + ↑π = 0

Tactic:
rw [← two_nsmul, two_nsmul_coe_pi]

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

Goal state before:
pp: ⊢ ContinuousOn log {0}ᶜ

Tactic:
simp +unfoldPartialApp only [continuousOn_iff_continuous_domRestrict,
    domRestrict]
  conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
  exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

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

Goal state before:
pp: l : List ℝ
h : ∀ x ∈ l, x ≠ 0
⊢ log l.prod = (List.map (fun x ↦ log x) l).sum

Tactic:
by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
    have : l.prod ≠ 0 := by grind [prod_ne_zero]
    rw [log_mul h.1 this, add_right_inj, ih]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ log ↑(p ^ t)

Tactic:
← Finsupp.log_prod,

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = log (n.factorization.prod fun p t ↦ ↑(p ^ t))

case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
⊢ cexp (2 * ↑π * I * ↑k / ↑N) = 1 ↔ N ∣ k

Tactic:
by
  rw [exp_eq_one_iff]
  conv in _ = _ => rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]
  field_simp [Nat.cast_ne_zero.mpr hN]
  norm_cast
  simp [← dvd_def, Int.ofNat_dvd]

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

Goal state before:
pp: z : ℂ
⊢ ∃ n, log (cexp z) = z + ↑n * (2 * ↑π * I)

Tactic:
rw [← exp_eq_exp_iff_exists_int, exp_log]
  exact exp_ne_zero z

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

Goal state before:
pp: x : ℂ
⊢ |x⁻¹.arg| = |x.arg|

Tactic:
rw [arg_inv]

Goal state after:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      if x = 0 then if n = 0 then ((starRingEnd ℂ) 1)⁻¹ else 0⁻¹
      else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹

Tactic:
map_one,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ Real.cos 0 = 1

Tactic:
Real.cos_zero

Goal state after:
⊢ 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + ↑(π / 2)).sin = θ.cos

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact Real.sin_add_pi_div_two _

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

Goal state before:
pp: θ : Angle
⊢ (↑(π / 2) - θ).cos = θ.sin

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact Real.cos_pi_div_two_sub _

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

Goal state before:
pp: θ ψ : ℝ
⊢ ↑(toIocMod two_pi_pos ψ θ) = ↑θ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]
  refine ⟨-toIocDiv two_pi_pos ψ θ, ?_⟩
  rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]

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

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then (starRingEnd ℂ) 1 else (starRingEnd ℂ) 0
      else (starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n))

Tactic:
map_one,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else if x = 0 then if n = 0 then 1 else (starRingEnd ℂ) 0 else (starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ ↑π ≠ 0

Tactic:
by
  rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]
  exact Real.pi_ne_zero

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑x.arg + ↑y⁻¹.arg = ↑x.arg - ↑y.arg

Tactic:
arg_inv_coe_angle,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑x.arg + -↑y.arg = ↑x.arg - ↑y.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: x : ℝ
⊢ (↑x).tan = Real.tan x

Tactic:
tan,

Goal state after:
x : ℝ
⊢ (↑x).sin / (↑x).cos = Real.tan x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
⊢ x ^ 0 = 1

Tactic:
simp [rpow_def]

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

Goal state before:
pp: x : ℝ
⊢ x ^ 1 = x

Tactic:
simp [rpow_def]

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

Goal state before:
pp: x : ℝ
⊢ 1 ^ x = 1

Tactic:
simp [rpow_def]

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

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y

Tactic:
simp_rw [Real.norm_eq_abs]
  exact abs_rpow_of_nonneg hx_nonneg

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ (↑x.toNNReal ^ y).toNNReal = x.toNNReal ^ y

Tactic:
← NNReal.coe_rpow,

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ (↑(x.toNNReal ^ y)).toNNReal = x.toNNReal ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

Tactic:
rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
    not_le_zero_iff] at h₁

Goal state after:
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ (x⁻¹ * x) ^ y = 1

Tactic:
ENNReal.inv_mul_cancel h0 h_top,

Goal state after:
case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ 1 ^ y = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
hb : 1 ≤ b
⊢ Monotone fun x ↦ b ^ x

Tactic:
rcases lt_or_eq_of_le hb with hb | rfl
  case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone
  case inr => intro _ _ _; simp

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
⊢ ↑x.toNNReal ^ z = ↑(x ^ z).toNNReal

Tactic:
← NNReal.coe_rpow,

Goal state after:
x : ℝ≥0∞
z : ℝ
⊢ ↑(x.toNNReal ^ z) = ↑(x ^ z).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑m ^ b = ↑r

Tactic:
rw [hb.to_eq rfl rfl, div_eq_mul_inv, Real.rpow_natCast_mul, ← Nat.cast_pow, hm, ← hkl, ← hr,
    Nat.cast_pow, Real.pow_rpow_inv_natCast] <;> positivity

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

Goal state before:
pp: a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = (a ^ (↑n / ↑d))⁻¹

Tactic:
← NNReal.rpow_neg,

Goal state after:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a ^ (-(↑n / ↑d))
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
⊢ midpoint R (p₁ -ᵥ p₁) (p₂ -ᵥ p₃) = ⅟2 • (p₂ -ᵥ p₃)

Tactic:
vsub_self,

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
⊢ midpoint R 0 (p₂ -ᵥ p₃) = ⅟2 • (p₂ -ᵥ p₃)
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
⊢ midpoint R (p₁ -ᵥ p₂) (p₃ -ᵥ p₃) = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
vsub_self,

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
⊢ midpoint R (p₁ -ᵥ p₂) 0 = ⅟2 • (p₁ -ᵥ p₂)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
⊢ f.linear = g.linear

Tactic:
apply LinearMap.pi_ext

Goal state after:
case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
⊢ ∀ (i : ι) (x : φv i), f.linear (Pi.single i x) = g.linear (Pi.single i x)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
div_eq_inv_mul,

Goal state after:
case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = ((r₁ + r₂)⁻¹ * r₂) • (v₁ + v₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
div_eq_inv_mul,

Goal state after:
case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = ((r₁ + r₂)⁻¹ * r₁) • (v₁ + v₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
rw [div_eq_inv_mul, mul_smul, smul_add, H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

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 : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
hv₂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
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : v ∈ vectorSpan k s
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ v₂ +ᵥ p₂ ∈ spanPoints k 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 : Set P
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ (v₁ +ᵥ p₁a) -ᵥ p₂ ∈ vectorSpan k s

Tactic:
hv₂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
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ (v₁ +ᵥ p₁a) -ᵥ (v₂ +ᵥ p₂a) ∈ vectorSpan k s
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:
add_smul,

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.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : { t // 0 ≤ t }
⊢ Icc x y ⊆ [x -[{ t // 0 ≤ t }] y]

Tactic:
by
  intro a ⟨hxa, hay⟩
  rw [← Subtype.coe_le_coe] at hxa hay
  rcases Icc_subset_segment ⟨hxa, hay⟩ with ⟨t₁, t₂, t₁_nonneg, t₂_nonneg, t_add, hta⟩
  refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_le, ?_, ?_⟩ <;>
  ext <;> simpa

Goal state after:
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 : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ s ⊆ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}

Tactic:
exact fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)

Goal state after:
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}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • u • x + a • v • y ∈ (convexHull 𝕜) s

Tactic:
← smul_comm u,

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
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + a • v • y ∈ (convexHull 𝕜) s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (-((1 - a) / 2) + (a - -1) / 2) • x ∈ s

Tactic:
add_smul,

Goal state after:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ -((1 - a) / 2) • x + ((a - -1) / 2) • x ∈ 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 : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t • x ∈ interior s

Tactic:
simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁

Goal state after:
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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
refine ⟨hf.1 hx hy ha hb hab, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2
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₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_right hp]
  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₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
p : P
hp : p ∈ ↑s₁
⊢ s₁.direction < s₂.direction

Tactic:
rcases h with ⟨hle, p₂, hp₂, hp₂s₁⟩

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
p : P
hp : p ∈ ↑s₁
hle : s₁ ≤ s₂
p₂ : P
hp₂ : p₂ ∈ s₂
hp₂s₁ : p₂ ∉ s₁
⊢ s₁.direction < s₂.direction
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
p₁ p₂ : P
⊢ Submodule.span k {p₁ -ᵥ p₁, p₁ -ᵥ p₂} = k ∙ (p₁ -ᵥ p₂)

Tactic:
vsub_self,

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₂ : P
⊢ Submodule.span k {0, p₁ -ᵥ p₂} = k ∙ (p₁ -ᵥ p₂)