mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos x * cosh y - sin x * (sinh y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
mul_assoc

Goal state after:
x y : ℂ
⊢ cos x * cosh y - sin x * (sinh y * I) = cos x * cosh y - sin x * (sinh y * I)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖Real.exp x - 1 - x‖ = ‖↑(Real.exp x) - 1 - ↑x‖

Tactic:
by exact_mod_cast Complex.norm_real _

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: n : ℕ
z : ℂ
⊢ cexp (↑n * (z * I)) = cexp (↑n * z * I)

Tactic:
mul_assoc

Goal state after:
n : ℕ
z : ℂ
⊢ cexp (↑n * (z * I)) = cexp (↑n * (z * I))
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ Ico n j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
rw [mem_Ico] at hm

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case hbc
x : ℝ
hx : |x| ≤ 1
⊢ |x| ^ 4 ≤ 1

pp: case hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1

Tactic:
· exact pow_le_one₀ (abs_nonneg _) hx

Goal state after:
case hab
x : ℝ
hx : |x| ≤ 1
⊢ x ^ 2 ≤ 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ -↑(x / 2) = ↑(-x / 2)

Tactic:
norm_cast; exact neg_div' 2 x

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ Real.exp x.re = Real.exp y.re ↔ x.re = y.re

Tactic:
Real.exp_eq_exp

Goal state after:
x y : ℂ
⊢ x.re = y.re ↔ x.re = y.re
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
⊢ ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ max C₀ C₁ * ‖g x‖

Tactic:
filter_upwards [eventually_ge_atTop n₁] with n hn

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
hn : n₁ ≤ n
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inl
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ 0

pp: case inr
n : ℕ
hn : 0 < n
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ n

Tactic:
· simpa using continuous_exp.continuousAt.norm.isBoundedUnder_le

Goal state after:
case inr
n : ℕ
hn : 0 < n
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x ↦ 1) =O[l] fun x ↦ rexp (f x)) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) l f

Tactic:
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ ‖↑m‖ = 0 ↔ m ∈ S

Tactic:
norm_mk_eq_zero_iff_mem_closure,

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ m ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S ↔ m ∈ S
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖(mk' S) m‖ = sInf ((fun x ↦ ‖m + x‖) '' ↑S)

Tactic:
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg_eq_neg,
    neg_coe_set (H := S), infDist_eq_iInf]
  simp only [dist_eq_norm', sub_neg_eq_add, add_comm]

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

Goal state before:
pp: ⊢ 4 * cos (π / 5) ^ 2 - 2 * cos (π / 5) - 1 = 0

Tactic:
set θ := π / 5 with hθ
  set c := cos θ
  set s := sin θ
  suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
  have hs : s ≠ 0 := by
    rw [ne_eq, sin_eq_zero_iff, hθ]
    push Not
    intro n hn
    replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
    lia
  suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
  calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable fun b ↦ ↑(a i) * ↑b ^ i * r ^ b

Tactic:
mul_assoc

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable fun b ↦ ↑(a i) * (↑b ^ i * r ^ b)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ ‖0‖ ≤ C * r ^ n

Tactic:
rw [norm_zero]

Goal state after:
case pos
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ y ∈ mk ⁻¹' {mk x} ↔ y ∈ pathComponent x

Tactic:
rw [mem_preimage, mem_singleton_iff, eq_comm, mem_pathComponent_iff]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ mk x = mk y ↔ Joined x y
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ γ : Path x y
x' y' : X
hx : x' = x
hy : y' = y
⊢ γ 0 = x'

Tactic:
by simp [hx]

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

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round 2⁻¹) * p| = |p| / 2

Tactic:
round_two_inv,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑1 * p| = |p| / 2
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 : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i

Tactic:
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) := by
    refine antitone_nat_of_succ_le (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, one_mul,
      ← sub_eq_add_neg, sub_le_iff_le_add]
    gcongr
    exact hfm (by lia)

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 : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i
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 ↦ arcsin (f x)) l (𝓝[≤] arcsin x)

Tactic:
by
  refine ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
  exact monotone_arcsin hy

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

Goal state before:
pp: x y : ℂ
⊢ |x.arg - y.arg| < 2 * π

Tactic:
by
  grind [arg_lt_arg_add_two_pi x y, arg_lt_arg_add_two_pi y x]

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

Goal state before:
pp: z : ℂ
⊢ ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π

Tactic:
not_or,

Goal state after:
z : ℂ
⊢ ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ log (cexp x) = x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
by
  rw [log_exp_eq_re_add_toIocMod, toIocMod, ofReal_sub, sub_mul, ← add_sub_assoc]
  simp [mul_assoc]

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

Goal state before:
pp: case negSucc
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x

Tactic:
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]

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

Goal state before:
pp: case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ log 1 = 0

Tactic:
log_one

Goal state after:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

Tactic:
by simp [hx]

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
by
  rw [inv_cpow_eq_ite, if_neg hx]

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 ((if x.arg = π then log x else (starRingEnd ℂ) (log 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 0 else cexp ((starRingEnd ℂ) (log x) * n)

Tactic:
split_ifs with hcx hn hx <;> rfl

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

Goal state before:
pp: z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
exact arg_mem_Ioc _

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

Goal state before:
pp: case empty
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ x ∈ ∅, 0 ≤ f x
⊢ a ^ ∑ x ∈ ∅, f x = ∏ x ∈ ∅, a ^ f x

Tactic:
| empty =>

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

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ (-θ).sign = 1 ∧ (-ψ).sign = 1

Tactic:
grind [sign_neg, neg_neg]

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

Goal state before:
pp: case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = ‖0‖ ^ w.re / rexp (arg 0 * w.im)

Tactic:
rw [norm_zero]

Goal state after:
case inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x ^ ↑y‖ = ‖x‖ ^ y

Tactic:
by
  rw [norm_cpow_of_imp] <;> simp

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

Goal state before:
pp: case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

Tactic:
rw [← hx, zero_rpow (ne_of_gt hz)]
    exact rpow_pos_of_pos (by rwa [← hx] at hxy) _

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

Goal state before:
pp: case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ ∅, ↑(f i) ^ r = ↑(∏ i ∈ ∅, f i) ^ r

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hf : ∀ i ∈ ∅, f i ≠ ∞
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
| empty =>

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
| empty =>

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
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
x✝ : z ∈ openSegment 𝕜 x x
a b : 𝕜
left✝¹ : 0 < a
left✝ : 0 < b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}

Tactic:
simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
⊢ Icc x y ⊆ [x -[𝕜] y]

Tactic:
by
  rintro z ⟨hxz, hyz⟩
  obtain rfl | h := (hxz.trans hyz).eq_or_lt
  · rw [segment_same]
    exact hyz.antisymm hxz
  rw [← sub_nonneg] at hxz hyz
  rw [← sub_pos] at h
  refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩
  · rw [← add_div, sub_add_sub_cancel, div_self h.ne']
  · rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
      div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]

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
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ Convex 𝕜 [x -[𝕜] y]

Tactic:
rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab
  refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
  · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
  · match_scalars <;> noncomm_ring

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

Tactic:
linear_combination (norm := noncomm_ring) a * habp + b * habq + hab

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

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • (s₁ + s₂)

Tactic:
rw [smul_add]

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ balancedCore 𝕜 t

Tactic:
by
  rw [balancedCore_eq_iInter ht]
  refine subset_iInter₂ fun a ha ↦ ?_
  rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]
  apply hst
  rw [norm_inv]
  exact inv_le_one_of_one_le₀ ha

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
b : 𝕜
ha' : a ⊆ b • W
⊢ b • closure[inst✝³] W ⊆ b • V

Tactic:
closure_subset_iff_isClosed.mpr hW₂,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
b : 𝕜
ha' : a ⊆ b • W
⊢ b • W ⊆ b • V
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
φ : G →* ι →ᵤ M := { toFun := swap (DFunLike.coe ∘ F), map_one' := ⋯, map_mul' := ⋯ }
⊢ Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))

Tactic:
exact continuous_of_continuousAt_one φ hf

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

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

Tactic:
rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
    direction_affineSpan]

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
p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P 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
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P 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
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ
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
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi,
      ← Set.insert_sdiff_singleton, Set.image_insert_eq, Set.image_insert_eq]

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
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k (insert (p i -ᵥ p i) ((fun x ↦ x -ᵥ p i) '' p '' (s \ {i})))
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₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ (s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂

Tactic:
simp_rw [weightedVSubOfPoint_apply]

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
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ ∑ i ∈ s, w₁ i • (p₁ i -ᵥ b) = ∑ i ∈ s, w₂ i • (p₂ i -ᵥ b)
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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ((map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)

Tactic:
simp_rw [weightedVSubOfPoint_apply]

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
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ∑ i ∈ map e s₂, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (w ∘ ⇑e) i • ((p ∘ ⇑e) i -ᵥ b)
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
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i

Tactic:
refine h i hi ?_

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
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ w i ≠ 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case empty
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ (∅.sup p) x = ↑(∅.sup fun i ↦ NNReal.mk ((p i) x) ⋯)

Tactic:
| empty =>

Goal state after: