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

Goal state before:
pp: x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|

Tactic:
simp only [le_antisymm_iff, le_norm_iff, Real.norm_eq_abs]

Goal state after:
x : ℝ
⊢ ‖↑x‖ ≤ |x - ↑(round x)| ∧ ∀ (m : ℝ), ↑m = ↑x → |x - ↑(round x)| ≤ |m|
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|

Tactic:
rw [norm_smul, mul_comm]
    exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = ↑1 * cexp (↑z.arg * I)

Tactic:
ofReal_one,

Goal state after:
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = 1 * cexp (↑z.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ¬x < 1 ↔ 1 ≤ x

Tactic:
not_lt

Goal state after:
x : ℝ
hx : 0 < x
⊢ 1 ≤ x ↔ 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ ¬1 < x ↔ x ≤ 1

Tactic:
not_lt

Goal state after:
case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ≤ 1 ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ (log x).im ≤ π

Tactic:
by simp only [log_im, arg_le_pi]

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

Goal state before:
pp: n : ℕ
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
⊢ log ↑0 = (Nat.factorization 0).sum fun p t ↦ ↑t * log ↑p

case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
⊢ 0 < x → -y < x → 1 + y / x = (rexp ∘ fun x ↦ log (x + y) - log x) x

Tactic:
hx₀

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
⊢ -y < x → 1 + y / x = (rexp ∘ fun x ↦ log (x + y) - log x) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h

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

Goal state before:
pp: case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
· rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]

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

Goal state before:
pp: case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rintro ⟨θ, rfl⟩
    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
    · convert! toIocMod_mem_Ioc _ _ _
      ring
    · rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]

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

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

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

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

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

Tactic:
rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ←
        Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
    · exact False.elim (hx (ext hr hi))
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
        Real.Angle.coe_zero, zero_add]

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

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

Tactic:
nth_rw 1 [← coe_toReal θ]
  rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]
  refine
    ⟨fun h => by linarith, fun h =>
      ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff₀' (zero_lt_two' ℝ)).1 h⟩⟩

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

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

Tactic:
intro θ
  induction θ using Real.Angle.induction_on
  rw [← coe_add, tan_coe, tan_coe]
  exact Real.tan_periodic _

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

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
⊢ 0 ≤ x → b ^ (1 / y) ≤ x → x ^ y ∈ Set.Ici b

Tactic:
hx₀

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
⊢ b ^ (1 / y) ≤ x → x ^ y ∈ Set.Ici b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ y ∈ Set.Ici b

Tactic:
filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx

Goal state after:
y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
hx : b ^ (1 / y) ≤ x
⊢ x ^ y ∈ Set.Ici b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z

Tactic:
← h,

Goal state after:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
⊢ 0 < x → 1 ≤ x → rexp x / x ^ n ≤ rexp x / x ^ s

Tactic:
hx₀

Goal state after:
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
⊢ 1 ≤ x → rexp x / x ^ n ≤ rexp x / x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s b : ℝ
hb : 0 < b
x : ℝ
⊢ 0 ≤ x → ((fun x ↦ x ^ b) ∘ fun x ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s

Tactic:
hx₀

Goal state after:
s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun x ↦ x ^ b) ∘ fun x ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < 0

Tactic:
neg_lt_zero

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π
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)]

Goal state after:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z

Tactic:
← h,

Goal state after:
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ (Multiset.map (fun x ↦ f x ^ r) s).prod = (Multiset.map f s).prod ^ r

Tactic:
by
  obtain ⟨l⟩ := s
  simpa using Real.list_prod_map_rpow' l f hs r

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

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

Tactic:
by_cases h : x = 0
    · rcases lt_trichotomy y 0 with (H | H | H) <;>
        simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
    · have A : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - ↑p ^ (-s) ≠ 0

Tactic:
refine sub_ne_zero_of_ne fun H ↦ ?_
  have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs
  simp only at this
  rw [← H, norm_one] at this
  norm_num at this

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

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

Tactic:
by
  rcases lt_trichotomy z 0 with (H | H | H)
  · cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]
  · simp [H]
  · cases x
    · simp [H, ne_of_gt]
    simp [← coe_rpow_of_nonneg _ (le_of_lt H)]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
⊢ ∀ {x y z : RayVector R M},
    SameRay R ↑((equiv R M) x) ↑((equiv R M) y) →
      SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)

Tactic:
intro x y z hxy hyz

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑((equiv R M) x) ↑((equiv R M) y)
hyz : SameRay R ↑((equiv R M) y) ↑((equiv R M) z)
⊢ SameRay R ↑((equiv R M) x) ↑((equiv R M) z)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
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 : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : (r₁ - r₂ * r) • x = 0
⊢ x = 0

Tactic:
smul_eq_zero

Goal state after:
case inr.inr
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 : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ - r₂ * r = 0 ∨ x = 0
⊢ x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = g_linear v +ᵥ g p
h : f = g
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add } = { toFun := g, linear := g_linear, map_vadd' := g_add }

Tactic:
obtain ⟨p⟩ := (AddTorsor.nonempty : Nonempty P1)
    congr with v
    apply vadd_right_cancel (f p)
    rw [← f_add, h, ← g_add]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p : P1
h : ⇑f.linear = ⇑(Equiv.vaddConst (f p)).symm ∘ ⇑f ∘ ⇑(Equiv.vaddConst p)
⊢ Function.Injective (⇑f ∘ ⇑(Equiv.vaddConst p)) ↔ Function.Injective ⇑f

Tactic:
Equiv.injective_comp

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
p : P1
h : ⇑f.linear = ⇑(Equiv.vaddConst (f p)).symm ∘ ⇑f ∘ ⇑(Equiv.vaddConst p)
⊢ Function.Injective ⇑f ↔ Function.Injective ⇑f
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]
  simp_rw [eq_comm (a := x)]
  exact exists_nonneg_left_iff_sameRay (R := R) hy

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
⊢ StarConvex 𝕜 (z + c • x) ((fun x ↦ z + c • x) '' s)

Tactic:
have h := (hs.smul c).add_left z

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
h : StarConvex 𝕜 (z + c • x) ((fun x ↦ z + x) '' (c • s))
⊢ StarConvex 𝕜 (z + c • x) ((fun x ↦ z + c • x) '' s)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ 1

Tactic:
by rw [← hab]; exact le_add_of_nonneg_left ha

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ↑x - ↑x ∈ ↑s

Tactic:
← h,

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
s : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ↑x - ↑x ∈ ↑s -ᵥ ↑s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
mem_direction_iff_eq_vsub ⟨p, hp⟩

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 : AffineSubspace k P
v : V
hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s
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
s : Set E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x ↦ z + x) ⁻¹' s)

Tactic:
by
  intro x hx y hy a b ha hb hab
  have h := hs hx hy ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

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

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (v₁ +ᵥ p₂) -ᵥ p₄ - v₂ ∈ vectorSpan k s

Tactic:
vadd_vsub_assoc

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun x ↦ c • x) t s

Tactic:
rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x ↦ c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x ↦ c • x) t 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 : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
by
  refine balancedCore_subset_balancedCoreAux.antisymm ?_
  refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)
  exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

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

Goal state before:
pp: case smul_vsub_vadd
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : u ∈ affineSpan k s), p u hx) →
      (∃ (hx : v ∈ affineSpan k s), p v hx) →
        (∃ (hx : w ∈ affineSpan k s), p w hx) → ∃ (hx : c • (u -ᵥ v) +ᵥ w ∈ affineSpan k s), p (c • (u -ᵥ v) +ᵥ w) hx

Tactic:
· exact fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h✝ : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ x + y = x + 0

Tactic:
← h,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h✝ : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ x = x + 0
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 : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x ↦ x -ᵥ p) '' (s \ {p}))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_sdiff_singleton, 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
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x ↦ x -ᵥ p) '' (s \ {p}))) = Submodule.span k ((fun x ↦ x -ᵥ p) '' (s \ {p}))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

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

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
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v

Tactic:
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

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
⊢ (∅.sup p) x = ↑(∅.sup fun i ↦ NNReal.mk ((p i) x) ⋯)

Tactic:
rw [Finset.sup_empty, Finset.sup_empty, coe_bot, _root_.bot_eq_zero, Pi.zero_apply]

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 = ↑0
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
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
vadd_vsub_assoc

Goal state after:
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
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁)
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ ⨅ u, p u + q (0 • x - u) = ‖0‖ * ⨅ u, p u + q (x - u)

case inr
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✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)