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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ (fun n ↦ ↑((n + k).choose k)) =O[atTop] fun n ↦ ↑(n ^ k)

Tactic:
apply isBigO_iff.2 ⟨2 ^ k, ?_⟩

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑((x + k).choose k)‖ ≤ 2 ^ k * ‖↑(x ^ k)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cexp (-(↑π * I)) = -1

Tactic:
by
  simp [Complex.exp_neg]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ cthickening ε (thickening δ {x}) = Metric.closedBall x (ε + δ)

Tactic:
cthickening_thickening hε hδ,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
x : E
⊢ cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
hx✝ : x ∈ F
hy✝ : y ∈ F
h : Joined ⟨x, hx✝⟩ ⟨y, hy✝⟩
hx : x ∈ F
hy : y ∈ F
⊢ Joined ⟨y, hy✝⟩ ⟨x, hx✝⟩

Tactic:
exact h.symm

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : R0Space Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ⇑g ⤳ ⇑f

Tactic:
exact h.symm

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
x : ↑s
y : ↑t
| mkD (t.domRestrict (f ↑x)) g

Tactic:
mkD_of_continuousOn (this x x.2)

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
x : ↑s
y : ↑t
| { toFun := t.domRestrict (f ↑x), continuous_toFun := ⋯ }
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b : ι → X
γ : (t : ι) → Path (a t) (b t)
h : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ t).extend

Tactic:
by
  apply h.comp (continuous_id.prodMap continuous_projIcc)
  exact zero_le_one

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

Tactic:
exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
← this,

Goal state after:
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico 0 (0 + 1)

Tactic:
exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

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

Goal state before:
pp: f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, f x * (-1) ^ x

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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

Goal state before:
pp: f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq fun n ↦ ∑ x ∈ Finset.range n, f x * (-1) ^ x

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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

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

Tactic:
← arcsin_neg,

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

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

Tactic:
← arcsin_neg,

Goal state after:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ arcsin (-y) ≤ -x ↔ sin x ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log (‖r‖ * ‖x‖)) + ↑(↑r * x).arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
arg_real_mul _ hr,

Goal state after:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ ↑(Real.log (‖r‖ * ‖x‖)) + ↑x.arg * I = ↑(Real.log r) + (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x = rexp (log x)

Tactic:
rw [exp_log hx]

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

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ x

Tactic:
· exact (log_le_sub_one_of_pos hx).trans (by linarith)

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

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

Tactic:
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]

Goal state after:
case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
⊢ log (a * l.prod) = log a + (List.map (fun x ↦ log x) l).sum
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑(↑n * π * 2 - ψ) = -↑ψ

Tactic:
coe_sub,

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑(↑n * π * 2) - ↑ψ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ map cexp (comap re atTop) = cobounded ℂ

Tactic:
by
  rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]
  exact eventually_ne_cobounded _

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ

Tactic:
coe_sub,

Goal state after:
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π

Tactic:
coe_sub,

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = -↑(π / 2 - ψ)
⊢ ↑θ + ↑ψ = ↑π

Tactic:
coe_sub,

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) - ↑θ = -(↑(π / 2) - ↑ψ)
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π

Tactic:
exact h.symm

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

Goal state before:
pp: z : ℂ
hre : z.re = 0
⊢ z = 0 ↔ z.im = 0

Tactic:
simp [Complex.ext_iff, hre]

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
· have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]
    simp [hre, this, or_comm, le_iff_eq_or_lt]

Goal state after:
case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hi : x.im < 0
⊢ (-x).arg = -Real.arccos (x.re / ‖x‖) + π

Tactic:
arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)

Goal state after:
x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π
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 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Tactic:
split_ifs with hx hn ha ha

Goal state after:
case pos
x n : ℂ
hx : x = 0
hn : n = 0
ha : x.arg = π
⊢ 1 = 1

case neg
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬x.arg = π
⊢ 1 = 1

case pos
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : x.arg = π
⊢ 0 = 0

case neg
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬x.arg = π
⊢ 0 = 0

case pos
x n : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ = (cexp ((starRingEnd ℂ) (log x) * n))⁻¹

case neg
x n : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(x.arg + π) = ↑x.arg + ↑π

Tactic:
Real.Angle.coe_add

Goal state after:
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑x.arg + ↑π = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
arg_real_mul _ hr,

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-π) θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (↑z.arg).toReal = z.arg

Tactic:
Real.Angle.toReal_coe_eq_self_iff_mem_Ioc

Goal state after:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (↑(x.arg + y.arg)).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
Real.Angle.toReal_coe_eq_self_iff_mem_Ioc

Goal state after:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x.arg + y.arg ∈ Ioc (-π) π ↔ x.arg + y.arg ∈ Ioc (-π) π
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 t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ a * t ^ b‖ ≤ t ^ c

Tactic:
← Real.rpow_add (zero_lt_one.trans_le ht),

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ (a + b)‖ ≤ t ^ c
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
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Tactic:
← Real.rpow_add (zero_lt_one.trans_le ht),

Goal state after:
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
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ (a + b)‖ ≤ ↑t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
by
  rw [rpow_mul hx, rpow_natCast]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
by
  rw [rpow_mul hx, rpow_natCast]

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

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ y) ^ (1 / y) = x

Tactic:
rw [← rpow_mul]
  field_simp
  simp

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

Goal state before:
pp: y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x

Tactic:
rw [← rpow_mul]
  field_simp
  simp

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

Goal state before:
pp: case e'_5
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = ‖(0, z).1‖ ^ (re ∘ Prod.snd) (0, z)

Tactic:
simp [hz, Real.zero_rpow hz.ne']

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

Goal state before:
pp: case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ‖(0, z).1‖ ≠ 0 ∨ 0 < (re ∘ Prod.snd) (0, z)

Tactic:
simp [hz, Real.zero_rpow hz.ne']

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

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

Tactic:
exact (strictMono_rpow_of_base_gt_one hb).monotone

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

Goal state before:
pp: case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

pp: case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
· simp [hx, H, ne_of_lt]

Goal state after:
case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : CommSemiring α
inst✝⁶ : PartialOrder α
inst✝⁵ : Semiring β
inst✝⁴ : PartialOrder β
inst✝³ : Algebra α β
inst✝² : ZeroLEOneClass β
inst✝¹ : PosMulMono β
inst✝ : MulPosMono β
⊢ IsOrderedModule α β ↔ Monotone ⇑(algebraMap α β)

Tactic:
simp [isOrderedModule_iff_smul_one_mono, Algebra.smul_def]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)

Tactic:
← sameRay_neg_iff,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (- -x) (-y) ↔ SameRay R x (-y)
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
v : M
r : R
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

Tactic:
← sameRay_neg_iff,

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
v : M
r : R
⊢ SameRay R (- -v) (-(r • v)) ↔ r ≤ 0 ∨ v = 0
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Tactic:
smul_eq_mul,

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) * x + ((z - x) / (y - x)) • y = z
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) * x + ((z - x) / (y - x)) • y = z

Tactic:
smul_eq_mul,

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) * x + (z - x) / (y - x) * y = z
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 ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Tactic:
mem_Iio

Goal state after:
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
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ {x, y} ⊆ segment 𝕜 x y

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
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)

Tactic:
exact (subsingleton_zero_smul_set _).strictConvex

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • 1) • ⨅ u, p u + q (x✝ - u) = ⨅ u, ↑(r • 1) • p u + ↑(r • 1) • q (x✝ - u)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • 1) * ⨅ u, p u + q (x✝ - u) = ⨅ u, ↑(r • 1) * p u + ↑(r • 1) * q (x✝ - u)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case right
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
i : ι
hi : i ∈ s
⊢ w' i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
simp [w', Set.indicator_apply, if_pos hi]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c • p (x✝ - x) < r ↔ p (x✝ - x) < r / ↑c

Tactic:
smul_eq_mul,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c * p (x✝ - x) < r ↔ p (x✝ - x) < r / ↑c
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c • p (x✝ - x) ≤ r ↔ p (x✝ - x) ≤ r / ↑c

Tactic:
smul_eq_mul,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c * p (x✝ - x) ≤ r ↔ p (x✝ - x) ≤ r / ↑c
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ ∑ ι ∈ s2, f ι = 0

Tactic:
rw [Finset.sum_insert
            (Finset.notMem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
          Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]

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
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f i1 + ∑ x ∈ s, g x = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (p.closedBall 0 r)

Tactic:
by
  rintro a ha x ⟨y, hy, hx⟩
  rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]
  calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ ≤ r := by rwa [mem_closedBall_zero] at hy

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

Goal state before:
pp: case refine_2
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i ∈ s', w0 i = 1
hw0s : (Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = (s'.weightedVSub p) w' +ᵥ p i0

Tactic:
hs',

Goal state after:
case refine_2
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i ∈ s', w0 i = 1
hw0s : (Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = (p1 -ᵥ p i0) +ᵥ p i0