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

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
have hcos : Real.cos θ < 0 := by
        rw [← neg_pos, ← Real.cos_add_pi]
        refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith

Goal state after:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ rexp (expOrderIso.symm ⟨|x|, ⋯⟩) = |x|

Tactic:
← coe_expOrderIso_apply,

Goal state after:
x : ℝ
hx : x ≠ 0
⊢ ↑(expOrderIso (expOrderIso.symm ⟨|x|, ⋯⟩)) = |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp (log x + 1) ≤ rexp (rexp (log x))
⊢ rexp 1 * x ≤ rexp x

Tactic:
exp_add,

Goal state after:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp (log x) * rexp 1 ≤ rexp (rexp (log x))
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x * y| = rexp (log x + log y)

Tactic:
exp_add,

Goal state after:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x * y| = rexp (log x) * rexp (log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x

Tactic:
rw [← log_inv]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ

Tactic:
rw [← coe_nsmul, two_nsmul, add_halves]

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

Goal state before:
pp: ⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
two_nsmul_neg_pi_div_two

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

Goal state before:
pp: ⊢ 2 • ↑π = 0

Tactic:
by simp [← natCast_mul_eq_nsmul]

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

Goal state before:
pp: ⊢ 2 * ↑π * I ≠ 0

Tactic:
by simp [Real.pi_ne_zero, I_ne_zero]

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

Goal state before:
pp: x : ℂ
n : ℤ
y : ℂ
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
n : ℤ
y : ℂ
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ x ^ (↑n * y) = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

Tactic:
exp_add,

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

Goal state before:
pp: ⊢ Real.sin 0 = 0

Tactic:
Real.sin_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)

Goal state after:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * cexp (↑x.arg * I + ↑y.arg * I)

Tactic:
exp_add,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (cexp (↑x.arg * I) * cexp (↑y.arg * I))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

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

Tactic:
by
  rw [(atTop_basis' 0).tendsto_right_iff]
  intro b hb
  filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx
  simpa (disch := positivity) [Real.rpow_inv_le_iff_of_pos] using hx

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

Goal state before:
pp: θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs

Goal state after:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case inr
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ (fun x ↦ f x ^ (-r)) =Θ[l] fun x ↦ g x ^ (-r)

Tactic:
exact rpow_pos hf hg h <| by linarith

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

Goal state before:
pp: x : ℂ
y : ℝ
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
y : ℝ
⊢ 0 ^ ↑y = ↑(‖0‖ ^ y) * (↑(Real.cos (arg 0 * y)) + ↑(Real.sin (arg 0 * y)) * I)

case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
simpa using rpow_add_intCast hx y n

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

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log x * z + log y * z) = rexp (log x * z) * y ^ z

Tactic:
exp_add,

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log x * z) * rexp (log y * z) = rexp (log x * z) * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Tactic:
· rw [← neg_neg p, rpow_neg, inv_pos]
    exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

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

Goal state before:
pp: case inl.inl
y : ℝ
⊢ 0 ^ y = 0 ^ 0 ↔ y = 0 ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ 0 = 0)

pp: case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
· simp [zero_rpow_def]

Goal state after:
case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (0, z)) fun x ↦ rexp (-(x.1.arg * x.2.im))

Tactic:
rcases exists_gt |im z| with ⟨C, hC⟩

Goal state after:
case refine_2
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (0, z)) fun x ↦ rexp (-(x.1.arg * x.2.im))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ∞ ∧ y < 0

Tactic:
cases x with

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = ∞ ↔ x = 0 ∧ y < 0 ∨ x = ∞ ∧ 0 < y

Tactic:
cases x with

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
cases x with

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
cases x with

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
cases x with

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

Goal state before:
pp: case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

Tactic:
simp only [rpow_zero, inv_one]

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

Goal state before:
pp: x : ℝ
⊢ √x = x ^ (1 / 2)

Tactic:
obtain h | h := le_or_gt 0 x
  · rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq,
      ← rpow_natCast, ← rpow_mul h]
    simp
  · have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring
    rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

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

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

Tactic:
cases x with

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

Goal state before:
pp: a b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (a ^ b) r

Tactic:
rcases ha with ⟨rfl⟩

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (↑m ^ b) r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: a : ℝ≥0
b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (a ^ b) r

Tactic:
rcases ha with ⟨rfl⟩

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (↑m ^ b) r
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✝ : SMulPosMono α β
⊢ Monotone ⇑(algebraMap α β)

Tactic:
by
  simpa [Algebra.smul_def] using smul_one_mono (α := α) β

Goal state after:
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
hv : v ≠ 0
r : R
hr : r ≠ 0
⊢ SameRay R v (r • v) ↔ 0 < r

Tactic:
by
  simp only [sameRay_smul_right_iff, hv, or_false, hr.symm.le_iff_lt]

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:
rw [hv₂p, vadd_vadd]

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.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x - y) (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + -y) (s + -t)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
by
  refine ⟨fun hz => ?_, ?_⟩
  · obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)
    obtain rfl | hb' := hb.eq_or_lt
    · rw [add_zero] at hab
      rw [hab, one_mul, zero_mul, add_zero] at hz
      exact (hz.1.ne rfl).elim
    · exact ⟨a, b, ha, hb', hab, rfl⟩
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    obtain rfl | ha' := ha.eq_or_lt
    · rw [zero_add] at hab
      rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
    · exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ Convex 𝕜 {x | f x ≤ B}

Tactic:
rw [convex_iff_segment_subset]
  rintro x hx y hy z ⟨a, b, ha, hb, hs, rfl⟩
  calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]

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

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

Tactic:
← 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
s : Set P
h : affineSpan k s = ⊤
⊢ (affineSpan k s).direction = ⊤
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
⊢ ∀ (r : 𝕜), 1 ≤ ‖r‖ → (fun x ↦ a • x) y ∈ r • s

Tactic:
intro r hr

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ (fun x ↦ a • x) y ∈ r • s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ vectorSpan k (insert p ps) = vectorSpan k ps

Tactic:
← 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
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ (affineSpan k (insert p ps)).direction = (affineSpan k ps).direction
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
· intro U hU
    rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
    refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)
    exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ f (0 • x + b • y) ≤ 0 • f x + b • f y

Tactic:
subst b

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
ha : 0 ≤ 0
hb : 0 ≤ 1
⊢ f (0 • x + 1 • y) ≤ 0 • f x + 1 • f y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: 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
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ ⟨u, hu⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
    ⟨v, hv⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
      ⟨w, hw⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

Tactic:
· exact AffineSubspace.smul_vsub_vadd_mem _ _

Goal state after:
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
⊢ ⊥ x = ↑⊥

Tactic:
coe_bot,

Goal state after:
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
⊢ 0 x = ↑⊥
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mp
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
⊢ (∃ y ∈ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s.direction, y + z = p -ᵥ p₁) → ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rintro ⟨v₁, hv₁, v₂, hv₂, hp⟩

Goal state after:
case mp
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₁ ∈ k ∙ (p₂ -ᵥ p₁)
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : 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 = 0 ∨ ∃ i ∈ ∅, (∅.sup p) x = (p i) x

pp: case inr
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x

Tactic:
· left; rfl

Goal state after:
case inr
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
hs : s.Nonempty
⊢ (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) 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
inst✝ : AffineSpace V P
s₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂

Tactic:
← 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
inst✝ : AffineSpace V P
s₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ (affineSpan k (s₁ ∪ s₂)).direction = (affineSpan k s₁).direction ⊔ (affineSpan k s₂).direction
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₂
s : Set P₁
hf : Function.Surjective ⇑f
h : affineSpan k s = ⊤
⊢ affineSpan k (⇑f '' s) = ⊤

Tactic:
← AffineSubspace.map_span,

Goal state after:
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₂
s : Set P₁
hf : Function.Surjective ⇑f
h : affineSpan k s = ⊤
⊢ AffineSubspace.map f (affineSpan k s) = ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case inr
ι : 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 : ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
        Finsupp.mem_span_image_iff_linearCombination,
        Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0),
        Finset.weightedVSubOfPoint_apply]
      let w' := Set.indicator (↑s) w
      have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
      use Finsupp.onFinset s w' hwx, Set.subset_univ _
      rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]
      · apply Finset.sum_congr rfl
        intro i hi
        simp [w', Set.indicator_apply, if_pos hi]
      · exact fun _ => zero_smul k _

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)

Tactic:
← direction_affineSpan,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ (affineSpan k s₁).direction = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ (affineSpan k s₁).direction = vectorSpan k s₂ ∧ (affineSpan k s₁ = ⊥ ↔ s₂ = ∅)

Tactic:
← direction_affineSpan,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    (affineSpan k s₁).direction = (affineSpan k s₂).direction ∧ (affineSpan k s₁ = ⊥ ↔ s₂ = ∅)