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))
⊢ Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖

Tactic:
apply summable_norm_mul_geometric_of_norm_lt_one (k := k) hr

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))
⊢ (fun n ↦ ↑((n + k).choose k)) =O[atTop] fun n ↦ ↑(n ^ k)
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 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε

Tactic:
infEDist_cthickening

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ pathComponentIn univ x = pathComponent x

Tactic:
by
  simp [pathComponentIn, pathComponent, JoinedIn, Joined, exists_true_iff_nonempty]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
hγ : range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected univ

Tactic:
← hf.range_eq

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (range f)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
p✝ : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |p / 2| ≤ p / 2
⊢ ‖↑(p / 2)‖ = |p / 2|

pp: case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = |x|

Tactic:
· simp [abs_div]

Goal state after:
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Tactic:
apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp

Goal state after:
x : ℝ
hx0 : ¬x < 0
⊢ 2 ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
by rw [← log_abs x, ← log_abs (-x), abs_neg]

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

Goal state before:
pp: x : ℝ
⊢ log x⁻¹ = -log x

Tactic:
by
  by_cases hx : x = 0; · simp [hx]
  rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]

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

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

Tactic:
← prod_toList,

Goal state after:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ log s.toList.prod = (Multiset.map (fun x ↦ log x) s).sum
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ cobounded ℂ ⊓ 𝓟 {0}ᶜ = cobounded ℂ

Tactic:
inf_eq_left,

Goal state after:
⊢ cobounded ℂ ≤ 𝓟 {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
intro Hsin

Goal state after:
case mp
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : (n * 2 + 1) % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Tactic:
rw [add_comm, Int.add_mul_emod_self_right] at this

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ Function.Antiperiodic sin ↑π

Tactic:
intro θ

Goal state after:
θ : Angle
⊢ (θ + ↑π).sin = -θ.sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ Function.Antiperiodic cos ↑π

Tactic:
intro θ

Goal state after:
θ : Angle
⊢ (θ + ↑π).cos = -θ.cos
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ Function.Injective toReal

Tactic:
intro θ

Goal state after:
θ : Angle
⊢ ∀ ⦃a₂ : Angle⦄, θ.toReal = a₂.toReal → θ = a₂
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ ∀ ⦃a₂ : Angle⦄, θ.toReal = a₂.toReal → θ = a₂

Tactic:
ψ

Goal state after:
θ ψ : Angle
⊢ θ.toReal = ψ.toReal → θ = ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]

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

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

Tactic:
induction θ using Real.Angle.induction_on with | _ θ
  simp [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr]

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

Goal state before:
pp: ⊢ Function.Periodic tan ↑π

Tactic:
intro θ

Goal state after:
θ : Angle
⊢ (θ + ↑π).tan = θ.tan
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π =
    if 0 ≤ a✝.re then Real.arcsin (a✝.im / ‖a✝‖)
    else if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π

Tactic:
if_neg hre.not_ge,

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π =
    if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ (if 0 ≤ a✝.re then Real.arcsin (a✝.im / ‖a✝‖)
    else if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π) =
    Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
if_neg hre.not_ge,

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ (if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π) =
    Real.arcsin ((-a✝).im / ‖a✝‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ (if 0 ≤ z.re then Real.arcsin (z.im / ‖z‖)
    else if 0 ≤ z.im then Real.arcsin ((-z).im / ‖z‖) + π else Real.arcsin ((-z).im / ‖z‖) - π) =
    Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
if_neg hre.not_ge,

Goal state after:
case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ (if 0 ≤ z.im then Real.arcsin ((-z).im / ‖z‖) + π else Real.arcsin ((-z).im / ‖z‖) - π) =
    Real.arcsin ((-z).im / ‖z‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
h : 0 ≤ θ.sign
⊢ ↑θ.toReal = θ

Tactic:
coe_toReal

Goal state after:
θ : Angle
h : 0 ≤ θ.sign
⊢ θ = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
h : θ.sign = -1
⊢ ↑θ.toReal = θ

Tactic:
coe_toReal

Goal state after:
case inl
θ : Angle
h : θ.sign = -1
⊢ θ = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0

Tactic:
simpa only [eventually_imp_distrib_right, not_imp_not, Imp.swap (a := b.re = 0)] using hl

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s

Tactic:
refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ x⁻¹ ^ (-s) = (fun x ↦ x ^ s) x

Tactic:
inv_rpow hx.out.le,

Goal state after:
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ (x ^ (-s))⁻¹ = (fun x ↦ x ^ s) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π

Tactic:
· rw [← ofReal_log hx, ← ofReal_mul, ofReal_im]; exact Real.pi_pos.le

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

Goal state before:
pp: p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
rw [ne_iff_lt_or_gt] at hp

Goal state after:
p : ℝ × ℝ
hp : p.1 < 0 ∨ 0 < p.1
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
⊢ ∞ ^ 0 = 1

Tactic:
dsimp only [(· ^ ·), Pow.pow, rpow]

Goal state after:
case top
⊢ (match ∞, 0 with
    | some x, y => if x = 0 ∧ y < 0 then ∞ else ↑(x.rpow y)
    | none, y => if 0 < y then ∞ else if y = 0 then 1 else 0) =
    1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 0 = 1

Tactic:
dsimp only [(· ^ ·), Pow.pow, rpow]

Goal state after:
case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 0 < 0 then ∞ else ↑(x✝.rpow 0)) = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case ha
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ 0 ≤ log x

Tactic:
exact log_nonneg hx

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

Goal state before:
pp: x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x ^ y) = ↑x ^ y

Tactic:
dsimp only [(· ^ ·), Pow.pow, rpow]

Goal state after:
x : ℝ≥0
h : x ≠ 0
y : ℝ
⊢ some (x.rpow y) = if x = 0 ∧ y < 0 then ∞ else ↑(x.rpow y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1

Tactic:
convert! rpow_le_rpow_of_exponent_le hx hz
  exact (rpow_zero x).symm

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
by
  rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]

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

Goal state before:
pp: case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero, h, this, NNReal.rpow_mul]

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

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ^ ε / ε

Tactic:
log_zero,

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ 0 ≤ 0 ^ ε / ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
⊢ ‖log 0‖ ≤ 0 ^ ε / ε

Tactic:
log_zero,

Goal state after:
case inl
ε : ℝ
hε : 0 < ε
⊢ ‖0‖ ≤ 0 ^ ε / ε
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ midpoint 𝕜 x y ∈ ⇑(AffineMap.lineMap x y) '' Ioo 0 1

Tactic:
exact ⟨⅟2, ⟨invOf_pos.mpr two_pos, invOf_lt_one one_lt_two⟩, rfl⟩

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ Ioo x y = Ioo (min x y) (max x y)

Tactic:
max_eq_right h.le,

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ Ioo x y = Ioo (min x y) y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ 0 ∈ ↑s -ᵥ ↑s

Tactic:
by
    obtain ⟨p, hp⟩ := h
    exact vsub_self p ▸ vsub_mem_vsub hp hp

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 : AffineSubspace k P
h : (↑s).Nonempty
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)

Tactic:
exact vsub_set_subset_vectorSpan k _

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 : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s -ᵥ ↑s = (fun x ↦ x -ᵥ p) '' ↑s

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
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
⊢ ↑s -ᵥ ↑s ⊆ (fun x ↦ x -ᵥ p) '' ↑s

case refine_2
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
⊢ (fun x ↦ x -ᵥ p) '' ↑s ⊆ ↑s -ᵥ ↑s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ y ∈ Ioc x y

Tactic:
right_mem_Ioc

Goal state after:
case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ x < y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ a ∈ [x -[{ t // 0 ≤ t }] y]

Tactic:
refine ⟨⟨t₁, t₁_nonneg⟩, ⟨t₂, t₂_nonneg⟩, zero_le, zero_le, ?_, ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ ⟨t₁, t₁_nonneg⟩ + ⟨t₂, t₂_nonneg⟩ = 1

case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
t₁ t₂ : 𝕜
t₁_nonneg : 0 ≤ t₁
t₂_nonneg : 0 ≤ t₂
t_add : t₁ + t₂ = 1
hta : t₁ • ↑x + t₂ • ↑y = ↑a
⊢ ⟨t₁, t₁_nonneg⟩ • x + ⟨t₂, t₂_nonneg⟩ • y = a
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s

Tactic:
refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
  rw [affineSpan_le]
  exact convexHull_subset_affineSpan s

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
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ Balanced 𝕜 ((convexHull 𝕜) s)

Tactic:
rw [balanced_iff_smul_mem] at hs ⊢
    refine fun a ha x hx => convexHull_min ?_ this hx a ha
    exact fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)

Goal state after:
Module: Mathlib.Topology.Algebra.UniformConvergence

Goal state before:
pp: α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
⊢ (𝓝 1).HasBasis p fun i ↦ {f | ∀ (x : α), toFun f x ∈ b i}

Tactic:
convert! UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one

Goal state after:
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), toFun x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G {x | x.2 / x.1 ∈ b x✝¹}
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 : P
hp : p ∈ ↑s₁
⊢ s₁.direction < s₂.direction

Tactic:
rw [lt_iff_le_and_exists] at 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₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
p : P
hp : 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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

case refine_2
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
⊢ f (-x) = f x

Tactic:
by rw [← neg_one_smul 𝕜, smul, norm_neg, ← smul, one_smul]

Goal state after:
Module: Mathlib.Analysis.Seminorm

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

Tactic:
rw [Finset.sup_cons, Finset.sup_cons, coe_sup, Pi.sup_apply, NNReal.coe_max, NNReal.coe_mk, ih]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
⊢ (affineCombination k s p) w = p i

Tactic:
by
  have h1 : ∑ i ∈ s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
  rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),
    weightedVSubOfPoint_apply]
  convert! zero_vadd V (p i)
  refine sum_eq_zero ?_
  intro i2 hi2
  by_cases h : i2 = i
  · simp [h]
  · simp [hw0 i2 hi2 h]

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

Goal state before:
pp: case right
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
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
rw [hp, vadd_vadd]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
by
  classical
  refine Finset.sup_le_iff.mpr ?_
  intro i hi
  rw [Finset.sum_eq_sum_sdiff_singleton_add hi, le_add_iff_nonneg_left]
  exact bot_le

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ (affineSpan k s₁ ⊔ affineSpan k s₂).direction = (affineSpan k s₁).direction ⊔ (affineSpan k s₂).direction

Tactic:
direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)

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

Goal state before:
pp: case mpr
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 : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∃ fs_1,
    ↑fs_1 ⊆ s ∧ ∃ w_1, ∑ i ∈ fs_1, w_1 i = ∑ i ∈ fs, w i ∧ ∑ i ∈ fs, w i • (p ↑i -ᵥ b) = ∑ i ∈ fs_1, w_1 i • (p i -ᵥ b)

Tactic:
refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩

Goal state after:
case mpr.refine_1
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 : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i ∈ map (Function.Embedding.subtype fun x ↦ x ∈ s) fs, (fun i ↦ if h : i ∈ s then w ⟨i, h⟩ else 0) i = ∑ i ∈ fs, w i

case mpr.refine_2
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 : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i ∈ fs, w i • (p ↑i -ᵥ b) =
    ∑ i ∈ map (Function.Embedding.subtype fun x ↦ x ∈ s) fs, (fun i ↦ if h : i ∈ s then w ⟨i, h⟩ else 0) i • (p i -ᵥ b)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ ↑(comap f ⊤) = ↑⊤

Tactic:
exact preimage_univ (f := f)

Goal state after: