mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)

Tactic:
rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩

Goal state after:
case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
K : Set X
i : ι
hi : {f | MapsTo ⇑f (K, i).1 (U (K, i).2)} ⊆ s
hK : IsCompact (K, i).1
hpi : p (K, i).2
⊢ s ∈ 𝓝 (const X c)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
α : 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
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0

Tactic:
filter_upwards [h] with _ hn

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✝‖
⊢ ‖f a✝‖ ≤ 0
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
h : ∀ (x : X), Continuous[inst✝², inst✝¹] fun y ↦ g (x, y)
G : X → C(Y, Z) := fun x ↦ { toFun := fun y ↦ g (x, y), continuous_toFun := ⋯ }
this : Continuous[inst✝³, _] G
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

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

Goal state before:
pp: case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | m - t • x ∈ { carrier := range fun x ↦ t • ↑x • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }} ↔
    m ∈ t • {m | m - x ∈ { carrier := range fun x ↦ ↑x • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }}

Tactic:
Set.range_smul

Goal state after:
case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | m - t • x ∈ { carrier := t • range fun i ↦ ↑i • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }} ↔
    m ∈ t • {m | m - x ∈ { carrier := range fun x ↦ ↑x • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : y ∈ Icc (-1) 1
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
by
  rw [← neg_le_neg_iff, ← arcsin_neg,
    arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg,
    neg_le_neg_iff]

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

Goal state before:
pp: x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x

Tactic:
sin_zero

Goal state after:
x : ℝ
⊢ 0 ≤ x ↔ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
by
  by_cases h₀ : z = 0; · simp [h₀, Real.pi_div_two_pos.ne]
  constructor
  · intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]
  · obtain ⟨x, y⟩ := z
    rintro ⟨rfl : x = 0, hy : 0 < y⟩
    rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

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

Goal state before:
pp: case negSucc
x : ℝ
a✝ : ℕ
⊢ -(↑(a✝ + 1) * log x) = -↑(a✝ + 1) * log x

Tactic:
Nat.cast_add_one,

Goal state after:
case negSucc
x : ℝ
a✝ : ℕ
⊢ -((↑a✝ + 1) * log x) = -(↑a✝ + 1) * log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ {0}ᶜ ∈ cobounded ℂ

Tactic:
exact eventually_ne_cobounded _

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him]
    rw [iff_true, arg_of_re_neg_of_im_neg hre him]
    exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

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

Goal state before:
pp: θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)

Tactic:
rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]

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

Goal state before:
pp: θ : ℝ
⊢ (↑θ).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)

Tactic:
convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2

Goal state after:
case e'_1
θ : ℝ
⊢ θ + 2 * π = θ - 2 * ↑(-1) * π

case e'_2
θ : ℝ
⊢ Set.Ioc (-3 * π) (-π) = Set.Ioc ((2 * ↑(-1) - 1) * π) ((2 * ↑(-1) + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
⊢ a - b ≠ ↑π

Tactic:
by
  intro h
  have h' : a = b + π := by
    simp [← h]
  have h_sign' := h_sign
  rw [h', Real.Angle.sign_add_pi] at h_sign'
  simp only [SignType.neg_eq_self_iff] at h_sign'
  contradiction

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

Goal state before:
pp: x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
refine (abs_rpow_le_abs_rpow x y).trans ?_
  by_cases hx : x = 0
  · by_cases hy : y = 0 <;> simp [hx, hy, zero_le_one]
  · rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

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

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y

Tactic:
Real.norm_eq_abs

Goal state after:
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ |x ^ y| = |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: s r : ℝ
hs : 0 < s
r' : ℝ := max r 1
hr : 0 < r'
H : 0 < s / r'
x : ℝ
hx : 0 ≤ x
⊢ (fun x ↦ (x ^ (s / r')) ^ r') x = (fun x ↦ x ^ s) x

Tactic:
simp only [← rpow_mul hx, div_mul_cancel₀ _ hr.ne']

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

Goal state before:
pp: p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ cexp (Complex.log x.1 * x.2)

Tactic:
suffices IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ from
    mem_nhds_iff.mpr ⟨_, fun x hx ↦ by simp_all [cpow_def_of_ne_zero], this, hp_fst⟩
  rw [isOpen_compl_iff]
  exact isClosed_eq continuous_fst continuous_const

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

Goal state before:
pp: a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)

Tactic:
rw [cpow_def_of_ne_zero ha]

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

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

Tactic:
rw [rpow_sub' h, rpow_one]

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

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

Tactic:
rw [rpow_sub' h, rpow_one]

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

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ 1 < rexp (log x * y) ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0

Tactic:
one_lt_exp_iff,

Goal state after:
x y : ℝ
hx : 0 < x
⊢ 0 < log x * y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x y : ℝ≥0
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)
  rw [tsub_add_cancel_of_le hy.le] at hm
  refine eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩
  simp only [one_div]
  simpa only [NNReal.rpow_inv_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn),
    NNReal.rpow_natCast] using hm.le.trans (pow_right_mono₀ hy.le (m.le_succ.trans hn))

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

Goal state before:
pp: x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| * t < 1

Tactic:
have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)

Goal state after:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rcases hx.eq_or_lt with rfl | h

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

case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)

pp: case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)

Tactic:
· rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq,
      ← rpow_natCast, ← rpow_mul h]
    simp

Goal state after:
case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = √x ^ r

Tactic:
rw [sqrt_eq_rpow, ← rpow_mul hx]

Goal state after:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ a ^ ↑(Int.negOfNat n) = (a ^ n)⁻¹

Tactic:
Real.rpow_intCast,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ a ^ Int.negOfNat n = (a ^ n)⁻¹
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : (algebraMap S R) a = 0
⊢ SameRay R v 0

Tactic:
exact zero_right _

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)

Tactic:
use 0, 1
    simp

Goal state after:
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
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]

Goal state after:
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
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x
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 ∧ x ≠ 0

Tactic:
rw [SameRay.sameRay_comm]

Goal state after:
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 y x ∧ x ≠ 0
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]

Goal state after:
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 y x
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r

Tactic:
rwa [zero_smul, zero_add, hab, 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
ι : Type u_5
inst✝ : Fintype ι
p : ι → P
h : affineSpan k (range p) = ⊤
i : ι
⊢ 0 < Fintype.card ι

Tactic:
exact Fintype.card_pos_iff.mpr ⟨i⟩

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
⊢ ⊥ < affineSpan k s ↔ s.Nonempty

Tactic:
bot_lt_iff_ne_bot,

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
⊢ affineSpan k s ≠ ⊥ ↔ s.Nonempty
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ x, 1 < ‖x‖
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
have : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
    exact Bornology.IsVonNBounded.of_boundedSpace

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
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
match_scalars <;> simp

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

Goal state before:
pp: case f
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
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
x✝ : ι
| w x✝ • (p x✝ -ᵥ b₁ - (p x✝ -ᵥ b₂))

Tactic:
vsub_sub_vsub_cancel_left

Goal state after:
case f
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
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
x✝ : ι
| w x✝ • (b₂ -ᵥ b₁)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
rw [add_comm] at hab hfx ⊢
  exact hf.lt_left_of_right_lt' hy hx hb ha hab hfx

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

Goal state before:
pp: case a.f
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
x✝ : ι
| w x✝ • (p x✝ -ᵥ b₁ - (p x✝ -ᵥ b₂))

Tactic:
vsub_sub_vsub_cancel_left

Goal state after:
case a.f
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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
x✝ : ι
| w x✝ • (b₂ -ᵥ b₁)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1.inr
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), y + z = (fun x ↦ x -ᵥ p₁) p₃

Tactic:
use 0, Submodule.zero_mem _, p₃ -ᵥ p₁

Goal state after:
case h
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun x ↦ x -ᵥ p₁) p₃
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c t = 0

Tactic:
by
  simp [affineCombinationLineMapWeights, hi, hj]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ vectorSpan k (s ×ˢ t) = (vectorSpan k s).prod (vectorSpan k t)

Tactic:
rw [vectorSpan_def, Set.prod_vsub_prod_comm]

Goal state after:
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
hs : s.Nonempty
ht : t.Nonempty
⊢ Submodule.span k ((s -ᵥ s) ×ˢ (t -ᵥ t)) = (vectorSpan k s).prod (vectorSpan k t)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

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

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:
· simp [Finset.eq_empty_of_isEmpty s]

Goal state after:
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)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
inst✝ : Fintype ι
p : ι → P
⊢ (∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0) → AffineIndependent k p

Tactic:
· intro h s w hw hs i hi
    rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs
    rw [← Finset.sum_indicator_subset _ (Finset.subset_univ s)] at hw
    replace h := h ((↑s : Set ι).indicator w) hw hs i
    simpa [hi] using h

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

Goal state before:
pp: case neg
ι : 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
i : ι
h : ¬i = i0
⊢ l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
· simp [hwdef, h]

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 ι
x : E
r : ℝ≥0
⊢ {y | ∀ b ∈ s, NNReal.mk ((p b) (y - x)) ⋯ ≤ r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) ≤ ↑r}

Tactic:
←
    NNReal.coe_le_coe,

Goal state after:
𝕜 : 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
r : ℝ≥0
⊢ {y | ∀ b ∈ s, ↑(NNReal.mk ((p b) (y - x)) ⋯) ≤ ↑r} = {x_1 | ∀ i ∈ s, (p i) (x_1 - x) ≤ ↑r}
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -p.ball x r = p.ball (-x) r

Tactic:
ext
  rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

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

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 V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔ AffineIndependent k fun p ↦ ↑p

Tactic:
rw [affineIndependent_set_iff_linearIndependent_vsub k
      (Set.mem_union_left _ (Set.mem_singleton p₁))]

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 V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (LinearIndependent k fun (v : ↑s) ↦ ↑v) ↔
    LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' s) \ {p₁}))) ↦ ↑v
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Subsingleton ι
i : ι
q : P
⊢ univ.Subsingleton

Tactic:
apply subsingleton_of_subsingleton

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
ε : ℝ
hε : ε > 0
k : 𝕜
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0

Tactic:
← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀),

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r ε : ℝ
hε : ε > 0
k : 𝕜
hp : k • p.closedBall 0 r ∈ 𝓝 0
hk₀ : 0 < ‖k‖
hk : ‖k‖ * r < ε
⊢ p.closedBall 0 (‖k‖ * r) ∈ 𝓝 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
inst✝¹ : Fintype ι
ι₂ : Type u_5
inst✝ : Fintype ι₂
p : ι → P
ha : AffineIndependent k p
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k univ (p ∘ ⇑e)) w₂ = (affineCombination k univ p) w₁
⊢ (Set.range ⇑e).indicator (extend (⇑e) w₂ 0) = w₁

Tactic:
by
  simpa using ha.indicator_extend_eq_of_affineCombination_comp_embedding_eq hw₁ hw₂ e h

Goal state after: