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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
· rw [cthickening_zero, thickening_closure, add_zero]

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ✝ : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
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
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
⊢ ∃ a, ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i

Tactic:
refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩

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
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
⊢ ‖f a✝‖ ≤ 0

Tactic:
by_contra! h

Goal state after:
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h✝ : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
h : 0 < ‖f a✝‖
⊢ False
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : t ≤ 1 / 2
⊢ (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)

Tactic:
obtain _ | ht₀ := le_total t 0
  · repeat rw [extend_of_le_zero _ (by linarith)]
  · rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: ⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)

Tactic:
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective

Goal state after:
⊢ IsDiscrete ↑(castAddHom ℝ).range
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx
    apply Complex.ext <;> simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

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

Goal state before:
pp: case inr.left
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Odd (2 * n + 1)
⊢ ∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ f (2 * n + 1)

Tactic:
rw [sub_le_iff_le_add, add_comm]
      exact lower.trans (le_add_of_nonneg_right (I (2 * n + 1)))

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

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|

Tactic:
exact le_abs_self _

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im

Tactic:
by rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

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

Goal state before:
pp: case refine_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
obtain ⟨x, y⟩ := z

Goal state after:
case refine_2
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
obtain ⟨x, y⟩ := z

Goal state after:
case neg.mpr
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re < 0 ∧ { re := x, im := y }.im = 0 → { re := x, im := y }.arg = π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
obtain ⟨x, y⟩ := z

Goal state after:
case neg.mpr
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → { re := x, im := y }.arg = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Tactic:
obtain ⟨x, y⟩ := z

Goal state after:
case neg.mpr
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → { re := x, im := y }.arg = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1

Tactic:
rw [← log_neg_eq_log x] at h

Goal state after:
case mp.inl
x : ℝ
h : log (-x) = 0
x_lt_zero : x < 0
⊢ -x = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
simp [hr, Real.pi_ne_zero]

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

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

Tactic:
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]

Goal state after:
θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
by
  rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h
  exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

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

Goal state before:
pp: ⊢ sign 0 = 0

Tactic:
sign,

Goal state after:
⊢ SignType.sign (sin 0) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑π).sign = 0

Tactic:
sign,

Goal state after:
⊢ SignType.sign (↑π).sin = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (-θ).sign = -θ.sign

Tactic:
sign,

Goal state after:
θ : Angle
⊢ SignType.sign (-θ).sin = -SignType.sign θ.sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + ↑π).sign = -θ.sign

Tactic:
sign,

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

Goal state before:
pp: θ : Angle
⊢ SignType.sign (θ + ↑π).sin = -θ.sign

Tactic:
sign,

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

Goal state before:
pp: θ : Angle
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
sign,

Goal state after:
θ : Angle
⊢ SignType.sign θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal < 0 ↔ θ.sign = -1

Tactic:
sign,

Goal state after:
θ : Angle
⊢ θ.toReal < 0 ↔ SignType.sign θ.sin = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
sign,

Goal state after:
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = SignType.sign θ.sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑(π / 2)).sign = 1

Tactic:
sign,

Goal state after:
⊢ SignType.sign (↑(π / 2)).sin = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑(-π / 2)).sign = -1

Tactic:
sign,

Goal state after:
⊢ SignType.sign (↑(-π / 2)).sin = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sign

Tactic:
sign,

Goal state after:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ SignType.sign (↑θ).sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ (-↑θ).sign ≤ 0

Tactic:
sign,

Goal state after:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ SignType.sign (-↑θ).sin ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π → a = b

Tactic:
intro h
    rcases h with h1 | h2
    · exact h1
    · have : a.sign = (b + π).sign := by aesop
      rw [Real.Angle.sign_add_pi] at this
      have := congr_arg (· = b.sign) this
      aesop

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0

Tactic:
exact (log_neg_iff hb₀).mpr hb₁

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
generalize arg x * y = z

Goal state after:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
generalize arg x * y = z

Goal state after:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rw [rpow_def, rpow_def, Complex.ofReal_add,
    Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx), Complex.ofReal_intCast,
    Complex.cpow_intCast, ← Complex.ofReal_zpow, mul_comm, Complex.re_ofReal_mul, mul_comm]

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

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

Tactic:
← rpow_mul

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (y * (1 / y)) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
← rpow_mul

Goal state after:
y : ℝ
hy : y ≠ 0
x : ℝ≥0
⊢ x ^ (1 / y * y) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ p.1 ≠ 0

Tactic:
exact hp.ne'

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

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

Tactic:
rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]

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

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ (x ^ 2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
by
  rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
    ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
  · linarith [pi_pos, neg_pi_lt_arg x]
  · exact (arg_neg_iff.2 hx).le

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p : P1
c : k
⊢ (lineMap p p) c = p

Tactic:
by
  simp [lineMap_apply]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ (lineMap p₀ p₁) 0 = p₀

Tactic:
by
  simp [lineMap_apply]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
⊢ (lineMap p₀ p₁) 1 = p₁

Tactic:
by
  simp [lineMap_apply]

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₀ p₁ : P1
c : k
⊢ f ((lineMap p₀ p₁) c) = (lineMap (f p₀) (f p₁)) c

Tactic:
by
  simp [lineMap_apply]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s

Tactic:
· rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩
    exact h hy ha hb hab

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
⊢ StarConvex 𝕜 x {x}

Tactic:
rintro y (rfl : y = x) a b _ _ hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
y : E
a b : 𝕜
a✝¹ : 0 ≤ a
a✝ : 0 ≤ b
hab : a + b = 1
⊢ a • y + b • y ∈ {y}
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Semiring 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : PartialOrder 𝕜
𝕜' : Type u_5
inst✝⁵ : Semiring 𝕜'
inst✝⁴ : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomSurjective σ
F' : Type u_6
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜' F'
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : 0 ≤ σ r
t : 𝕜
hb : 0 ≤ σ t
hab : σ r + σ t = 1
⊢ 0 ≤ r

Tactic:
by simp_all [(@hσ 0 r).mp]

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
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₂
  have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
  rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
    AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂
  exact subsingleton_of_univ_subsingleton h₂

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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x ↦ x -ᵥ p i) '' p '' (s \ {i}))

Tactic:
conv_lhs =>
    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}))) =
    Submodule.span k ((fun x ↦ x -ᵥ p i) '' p '' (s \ {i}))
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
x : E
⊢ p 0 + q (x - 0) ≤ q x

Tactic:
by
        simp only [map_zero, zero_add, sub_zero]; rfl

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

Goal state before:
pp: 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
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥

Tactic:
simp [pointwise_vadd_eq_map, map_bot]

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

Goal state before:
pp: ι : 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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)

Tactic:
convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)

Goal state after:
ι : 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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w =
    (Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun x ↦ p ↑x) fun i ↦ w ↑i
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

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✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ⇑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ⇑(φ.restrict hEF)

Tactic:
intro x y h
  simp only [Subtype.ext_iff, AffineMap.restrict.coe_apply] at h ⊢
  exact hφ h

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s, w x = 0
hw₁ : ∑ x ∈ s, w x • x = 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
rw [← sum_attach] at hw₀ hw₁

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s.attach, w ↑x = 0
hw₁ : ∑ x ∈ s.attach, w ↑x • ↑x = 0
⊢ ∀ x ∈ s, w x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2
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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, w i ∈ I
hi0 : ∀ i ∉ fs, w i = 0
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I (s.face h)

Tactic:
let w' : Fin (m + 1) → k := w ∘ fs.orderEmbOfFin h

Goal state after:
case refine_2
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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, w i ∈ I
hi0 : ∀ i ∉ fs, w i = 0
w' : Fin (m + 1) → k := w ∘ ⇑(fs.orderEmbOfFin h)
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I (s.face h)
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
| nhdsKer (⋃ x ∈ s ×ˢ t, {x})

Tactic:
nhdsKer_biUnion

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
| ⋃ i ∈ s ×ˢ t, nhdsKer {i}
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
| nhdsKer (⋃ x ∈ univ.pi s, {x})

Tactic:
nhdsKer_biUnion

Goal state after:
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
| ⋃ i ∈ univ.pi s, nhdsKer {i}
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mpr.inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 {x}
hx : x ∈ interior {x}
⊢ {x}.Nontrivial

Tactic:
rw [interior_singleton] at hx

Goal state after:
case mpr.inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 {x}
hx : x ∈ ∅
⊢ {x}.Nontrivial
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: case mpr.inl
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 {x}
hx : x ∈ ∅
⊢ {x}.Nontrivial

Tactic:
exact hx.elim

Goal state after: