mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ = ↑π - 2 • ψ
⊢ |θ.cos| = |ψ.sin|

Tactic:
← two_nsmul_coe_div_two,

Goal state after:
θ ψ : Angle
h : 2 • θ = 2 • ↑(π / 2) - 2 • ψ
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a ↦ ‖a‖)) z - π)

Tactic:
simp [him]

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

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

Tactic:
sign_nonpos_iff,

Goal state after:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ (-↑θ).sin ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (fun x ↦ rexp (log b * x)) atBot atTop

Tactic:
refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_

Goal state after:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ + -ψ).sign ≠ 1

Tactic:
← hθ',

Goal state after:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ + -ψ).sign ≠ (-θ).sign
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ h
    simp [Real.rpow_eq_zero_iff_of_nonneg, h]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ ‖t ^ (a + b)‖ ≤ t ^ c

Tactic:
Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
t : ℝ
ht : 1 ≤ t
⊢ t ^ (a + b) ≤ t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ (a + b)‖ ≤ ↑t ^ c

Tactic:
Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))

Goal state after:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n ↦ ↑n ^ a
hg : g =O[atTop] fun n ↦ ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ↑t ^ (a + b) ≤ ↑t ^ c
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (↑x ^ ↑y) ^ z = ↑(x ^ y) ^ z

pp: case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

pp: case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π

Tactic:
ofReal_cpow hx

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (↑x ^ ↑y) ^ z = (↑x ^ ↑y) ^ z

case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
obtain rfl | hz := eq_or_ne z 0

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

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

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)

Goal state after:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ x ^ z

Tactic:
rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)

Goal state after:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)

Tactic:
rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)

Goal state after:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ rexp (log x * y) ≤ rexp (log x * z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)
⊢ 0 < (↑(x, y).1, (x, y).2).1.re

Tactic:
ofReal_re

Goal state after:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)
⊢ 0 < (x, y).1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
| top =>

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

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

Tactic:
| top =>

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

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

Tactic:
| top =>

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

Goal state before:
pp: case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rw [max_eq_left hxy, max_eq_left (by gcongr)]

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

Goal state before:
pp: case top
y : ℝ
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

Tactic:
| top =>

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

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

Tactic:
rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: case top
y z : ℝ
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
| top =>

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ Antitone fun x ↦ b ^ x

Tactic:
rcases lt_or_eq_of_le hb₁ with hb₁ | rfl
  case inl => exact (strictAnti_rpow_of_base_lt_one hb₀ hb₁).antitone
  case inr => intro _ _ _; simp

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

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

Tactic:
| top =>

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
p : P₂
v : V₂
⊢ v +ᵥ p = e.symm.symm (e.linear.symm v +ᵥ e.symm p)

Tactic:
rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
        LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ⇑f '' [a -[𝕜] b] ↔ x ∈ [f a -[𝕜] f b]

Tactic:
simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
this : c + q • (y - c) = c + p • (x - c)
⊢ (1 - p) • c + p • x ∈ {c}

Tactic:
obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
Hx : x = x - c + c
Hy : y = y - c + c
p0 : 0 ≤ 0
p1 : 0 ≤ 1
q0 : 0 ≤ 0
q1 : 0 ≤ 1
H : (1 - 0) • c + (0 • (y - c) + 0 • c) = (1 - 0) • c + (0 • (x - c) + 0 • c)
this : c + 0 • (y - c) = c + 0 • (x - c)
⊢ (1 - 0) • c + 0 • x ∈ {c}
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddRightMono 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ZeroLEOneClass 𝕜
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] = {c}

Tactic:
refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_
  simp [singleton_subset_iff, left_mem_segment]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ openSegment 𝕜 x y ⊆ insert ((lineMap x y) c) (openSegment 𝕜 x ((lineMap x y) c) ∪ openSegment 𝕜 ((lineMap x y) c) y)

Tactic:
simp only [openSegment_eq_image_lineMap, ← mapsTo_iff_image_subset]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c : 𝕜
⊢ MapsTo (⇑(lineMap x y)) (Ioo 0 1)
    (insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1))
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_le h]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ Icc x y
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
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ +ᵥ p₃ ∈ s

Tactic:
convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ 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
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ = 1 • (p₁ -ᵥ p₂)
Module: Mathlib.Analysis.Convex.Basic

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

Tactic:
by
  simpa only [← image_smul, ← image_vadd, image_image] using! (hs.smul c).vadd z

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
⊢ (affineSpan k s).direction ≤ vectorSpan k s

Tactic:
refine Submodule.span_le.2 ?_
    rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩
    simp only [SetLike.mem_coe]
    rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
    exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
⊢ v ∈ (sInf t).direction

Tactic:
← vadd_mem_iff_mem_direction v ((mem_sInf_iff p t).mpr 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
⊢ v +ᵥ p ∈ sInf t
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
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
⊢ (fun x ↦ a • x) y ∈ balancedCoreAux 𝕜 s

Tactic:
obtain rfl | h := eq_or_ne a 0

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
y : E
hy : y ∈ balancedCoreAux 𝕜 s
ha : ‖0‖ ≤ 1
⊢ (fun x ↦ 0 • x) y ∈ balancedCoreAux 𝕜 s

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
⊢ (fun x ↦ a • x) y ∈ balancedCoreAux 𝕜 s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
obtain rfl | h := eq_or_ne a 0

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 • insert 0 (interior A) ⊆ insert 0 (interior A)

case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)
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
p : P
d₁ d₂ : Submodule k V
⊢ mk' p d₁ ≤ mk' p d₂ ↔ d₁ ≤ d₂

Tactic:
simp_rw [SetLike.le_def, mem_mk']
  refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ h hx⟩
  simpa using h (show (x +ᵥ p) -ᵥ p ∈ d₁ by simpa using hx)

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
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ ⊥ < affineSpan k s

Tactic:
IsSimpleOrder.bot_lt_iff_eq_top

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
inst✝ : Subsingleton P
⊢ affineSpan k s = ⊤ ↔ affineSpan k s = ⊤
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✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
x : E
h : IsVonNBounded 𝕜 (x +ᵥ s)
⊢ IsVonNBounded 𝕜 s

Tactic:
by simpa using h.vadd (-x)

Goal state after:
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✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U s

Tactic:
refine Absorbs.mono_right ?_ hs

Goal state after:
𝕜 : 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✝ : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → Bornology.IsVonNBounded 𝕜 s

Tactic:
· rintro ⟨a, ha⟩
    exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Goal state after:
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✝¹¹ : PartialOrder β✝
inst✝¹⁰ : Module 𝕜✝ E✝
inst✝⁹ : Module 𝕜✝ β✝
inst✝⁸ : LinearOrder E✝
s✝ : Set E✝
f✝ : E✝ → β✝
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : x < y
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
exact hf hx hy h ha hb hab

Goal state after:
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✝¹¹ : PartialOrder β✝
inst✝¹⁰ : Module 𝕜✝ E✝
inst✝⁹ : Module 𝕜✝ β✝
inst✝⁸ : LinearOrder E✝
s✝ : Set E✝
f✝ : E✝ → β✝
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : x < y
⊢ f (a • x + b • y) < a • f x + b • f y

Tactic:
exact hf hx hy h ha hb hab

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
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯) ≤ ↑a

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
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup fun i ↦ NNReal.mk ((p i) x) ⋯) ≤ a
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_6
V : Type u_7
P : Type u_8
inst✝⁴ : CommRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_9
inst✝ : DecidableEq ι
s : Finset ι
p : ι → P
w : ι → k
i : ι
hi : i ∈ s
r : k
⊢ (AffineMap.lineMap (p i) ((affineCombination k s p) w)) r =
    (AffineMap.lineMap ((affineCombination k s p) (Pi.single i 1)) ((affineCombination k s p) w)) r

Tactic:
Finset.affineCombination_piSingle _ _ _ hi

Goal state after:
k : Type u_6
V : Type u_7
P : Type u_8
inst✝⁴ : CommRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_9
inst✝ : DecidableEq ι
s : Finset ι
p : ι → P
w : ι → k
i : ι
hi : i ∈ s
r : k
⊢ (AffineMap.lineMap (p i) ((affineCombination k s p) w)) r = (AffineMap.lineMap (p i) ((affineCombination k s p) w)) r
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
⊢ map f (v +ᵥ s) = f.linear v +ᵥ map f s

Tactic:
rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
  congr 1
  ext
  exact f.map_vadd _ _

Goal state after:
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
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0

Tactic:
let f : ι → V := fun i => w i • (p i -ᵥ p i1)

Goal state after:
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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
⊢ w i = 0