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

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ dist (f₁ x • g x) (f₂ x • g x)) l (𝓝 0)

Tactic:
dist_eq_norm,

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖f₁ x • g x - f₂ x • g x‖) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ arg 1 = 0

Tactic:
by simp [arg, zero_le_one]

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ log (- -↑n)

Tactic:
neg_neg

Goal state after:
n : ℕ
⊢ 0 ≤ log ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = - -z.arg

pp: case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

pp: case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π

Tactic:
neg_neg

Goal state after:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = z.arg

case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
log_one,

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 - log x < 1 / x
⊢ |log x * x| < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log (a * l.prod) = log a + (List.map (fun x ↦ log x) l).sum

Tactic:
log_mul h.1 this,

Goal state after:
case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log a + log l.prod = log a + (List.map (fun x ↦ log x) l).sum
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + - -(↑x.arg * I) else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
neg_neg

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x.arg ≠ π
⊢ log x⁻¹ = -log x

Tactic:
by rw [log_inv_eq_ite, if_neg hx]

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ cexp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
rw [exp_eq_one_iff]

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) ↔ ∃ n, x = ↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: k N : ℕ
hN : N ≠ 0
⊢ cexp (2 * ↑π * I * ↑k / ↑N) = 1 ↔ N ∣ k

Tactic:
rw [exp_eq_one_iff]

Goal state after:
k N : ℕ
hN : N ≠ 0
⊢ (∃ n, 2 * ↑π * I * ↑k / ↑N = ↑n * (2 * ↑π * I)) ↔ N ∣ k
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ |z.im| < ‖z‖

pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Tactic:
abs_im_lt_norm

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ |z.im| < ‖z‖

pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Tactic:
abs_im_lt_norm

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
intro θ
  induction θ using Real.Angle.induction_on
  exact Real.sin_antiperiodic _

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

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

Tactic:
simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]

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

Goal state before:
pp: θ : Angle
| θ.sin

Tactic:
rw [← coe_toReal θ, sin_coe]

Goal state after:
θ : Angle
| Real.sin θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ if b = 0 then if x = 0 then 1 else 0 else rexp (log b * x) * cos (x * π)) atTop (𝓝 0)

Tactic:
hb.ne,

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ if False then if x = 0 then 1 else 0 else rexp (log b * x) * cos (x * π)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, ↑x < a ^ y

Tactic:
filter_upwards [hc'] with a ha

Goal state after:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z

Tactic:
exact rpow_pos_of_pos (by rwa [← hx] at hxy) _

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

Goal state before:
pp: case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1

Tactic:
exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

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

Goal state before:
pp: M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ ↑M ^ P = ↑M ^ P

Tactic:
← ENNReal.rpow_eq_pow

Goal state after:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ (↑M).rpow P = (↑M).rpow P
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ cexp (↑π * I * p.2)) (x, y)

Tactic:
· fun_prop

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

Goal state before:
pp: case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)

Tactic:
· fun_prop

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

Goal state before:
pp: case inr
x y z : ℝ
hy : 0 < y
h : log x < z * log y
hx : 0 < x
⊢ x < y ^ z

Tactic:
· exact (lt_rpow_iff_log_lt hx hy).2 h

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

Goal state before:
pp: z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x ↦ x ^ z) x < (fun x ↦ x ^ z) y

Tactic:
lift x to ℝ≥0 using ne_top_of_lt hxy

Goal state after:
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x ↦ x ^ z) ↑x < (fun x ↦ x ^ z) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
    simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos] <;>
    linarith

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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 y : M
⊢ SameRay R (- -x) (-y) ↔ SameRay R x (-y)

Tactic:
neg_neg

Goal state after:
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 y : M
⊢ SameRay R x (-y) ↔ SameRay R x (-y)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = f 0 + f (x + y)

Tactic:
by rw [h0, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ - -↑((equiv R M) v) = ↑((equiv R M) v)

Tactic:
neg_neg

Goal state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
inst✝⁵ : PartialOrder R✝
inst✝⁴ : IsStrictOrderedRing R✝
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ M
inst✝ : Module R✝ N
x y : M
R : Type u_4
v : RayVector R M
⊢ ↑((equiv R M) v) = ↑((equiv R M) v)
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:
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:
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:
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:
simp [lineMap_apply]

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

Goal state before:
pp: case e_6
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
c : k
⊢ (lineMap 1 0) (1 - c) = c

Tactic:
simp [lineMap_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : IsOrderedRing 𝕜
inst✝³ : IsDomain 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
inst✝ : Nontrivial 𝕜
⊢ LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]

Tactic:
rw [LinearIndependent.pair_add_smul_add_smul_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : CommRing 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : IsOrderedRing 𝕜
inst✝³ : IsDomain 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
inst✝ : Nontrivial 𝕜
⊢ LinearIndependent 𝕜 ![x, y] ∧ -1 * s ≠ t * -1
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
coe_direction_eq_vsub_set_right 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
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x ↦ x -ᵥ p) '' ↑s ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) (⇑f '' s) ⊆ ⇑f '' (convexHull 𝕜) s

Tactic:
· exact convexHull_min (Set.image_mono (subset_convexHull 𝕜 s))
      ((convex_convexHull 𝕜 s).affine_image f)

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
⊢ ⊥.direction = ⊥

Tactic:
rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]

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
Q : AffineSubspace k P
⊢ (↑Q).Nonempty ↔ Q ≠ ⊥

Tactic:
rw [nonempty_iff_ne_empty]

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
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ f ((fun x ↦ a • x) y) ∈ s

Tactic:
map_smul

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ a • f y ∈ 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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
⊢ False

Tactic:
have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ False
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ (fun x ↦ (a * y) • x) z ∈ U

Tactic:
refine hrVU _ _ ?_ hz

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a * y‖ < r
Module: Mathlib.Topology.MetricSpace.Equicontinuity

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

Tactic:
intro ε hε
    exact H _ (dist_mem_uniformity hε)

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

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

Tactic:
neg_neg

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)
Module: Mathlib.Analysis.Convex.Function

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

Tactic:
neg_neg

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y < f (a • x + b • y)
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₂
p : P₁
direction : Submodule k V₁
q : P₂
⊢ q ∈ map f (mk' p direction) ↔ q ∈ mk' (f p) (Submodule.map f.linear direction)

Tactic:
simp only [mem_map, mem_mk', Submodule.mem_map]

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₂
p : P₁
direction : Submodule k V₁
q : P₂
⊢ (∃ y, y -ᵥ p ∈ direction ∧ f y = q) ↔ ∃ y ∈ direction, f.linear y = q -ᵥ f p
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
r : k
p : ι → P
⊢ ((1 - r) • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +
        r • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₂) +ᵥ
      Classical.choice ⋯ =
    ((s.weightedVSubOfPoint p (Classical.choice ⋯)) ((1 - r) • w₁) +
        (s.weightedVSubOfPoint p (Classical.choice ⋯)) (r • w₂)) +ᵥ
      Classical.choice ⋯

Tactic:
map_smul

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (DFunLike.coe '' range p) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)

Tactic:
← range_comp,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range (DFunLike.coe ∘ p)) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(#{i₁, i₂}) ≠ 0

Tactic:
rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(1 + 1) ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
⊢ centroid k s p = centroid k univ fun x ↦ ↑x

Tactic:
let f' : ps → ι := fun x => f ⟨x, hps ▸ x.property⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
⊢ centroid k s p = centroid k univ fun x ↦ ↑x
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
⊢ centroid k s p = centroid k univ fun x ↦ ↑x

Tactic:
have hf' : ∀ x, f' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ centroid k s p = centroid k univ fun x ↦ ↑x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂

Tactic:
exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)

Goal state after: