mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + 0 * I + ↑π * I) * y)

Tactic:
zero_mul,

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

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ cexp ↑(log x * ↑y).re * (cos ↑(log x * ↑y).im + sin ↑(log x * ↑y).im * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
mul_comm (log x)

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ cexp ↑(↑y * log x).re * (cos ↑(↑y * log x).im + sin ↑(↑y * log x).im * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x‖ ^ y.re / rexp (0 * y.im) = x ^ y.re

Tactic:
zero_mul,

Goal state after:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖↑x‖ ^ y.re / rexp 0 = x ^ y.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
by
  rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]

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

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

Tactic:
by
  ext; exact Real.rpow_add_intCast' (mod_cast x.2) h

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

Goal state before:
pp: case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]

Goal state after:
case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2)) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)

Tactic:
simp only [div_eq_mul_inv, ← Real.exp_neg]

Goal state after:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1

Tactic:
by
  convert! rpow_lt_rpow_of_exponent_lt hx hz
  exact (rpow_zero x).symm

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

Goal state before:
pp: case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

Tactic:
rcases _root_.em (y = 0) with (rfl | hy)

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ 0 ^ 0 < 1 ↔ 0 = 0 ∧ 0 ≠ 0 ∨ 1 < 0 ∧ 0 < 0 ∨ 0 < 1 ∧ 0 < 0

case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

Tactic:
rcases _root_.em (y = 0) with (rfl | hy)

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ 1 < 0 ^ 0 ↔ 1 < 0 ∧ 0 < 0 ∨ 0 < 0 ∧ 0 < 1 ∧ 0 < 0

case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
by
  rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]; positivity

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

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

Tactic:
abs_of_pos ht,

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

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ √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]

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hx0 : x = 0

Goal state after:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = midpoint R y x

Tactic:
by
  rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ z ∈ [x -[𝕜] y]

Tactic:
refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 ≤ a • 1

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : PartialOrder 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : ZeroLEOneClass 𝕜
inst✝⁶ : Module 𝕜 E
R : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : Module R E
inst✝² : Module R 𝕜
inst✝¹ : IsScalarTower R 𝕜 E
inst✝ : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 ≤ b • 1
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ : P
⊢ (ofLinearEquiv A p₀ p₁).trans (ofLinearEquiv B p₁ p₂) = ofLinearEquiv (A ≪≫ₗ B) p₀ p₂

Tactic:
by
  ext x
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : ZeroLEOneClass 𝕜
inst✝⁷ : Module 𝕜 E
R : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : Module R E
inst✝³ : Module R 𝕜
inst✝² : IsScalarTower R 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x y

Tactic:
refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : ZeroLEOneClass 𝕜
inst✝⁷ : Module 𝕜 E
R : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : Module R E
inst✝³ : Module R 𝕜
inst✝² : IsScalarTower R 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < a • 1

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : ZeroLEOneClass 𝕜
inst✝⁷ : Module 𝕜 E
R : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : Module R E
inst✝³ : Module R 𝕜
inst✝² : IsScalarTower R 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < b • 1
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case e'_2
𝕜 : 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
⊢ c + q • (y - c) = (1 - q) • c + (q • (y - c) + q • c)

Tactic:
simp [sub_smul]

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

Goal state before:
pp: case e'_3
𝕜 : 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
⊢ c + p • (x - c) = (1 - p) • c + (p • (x - c) + p • c)

Tactic:
simp [sub_smul]

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:
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.Analysis.Convex.Segment

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
a b : 𝕜
left✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun x ↦ b • x) x = a • x + (fun x ↦ b • x) y

Tactic:
rw [hx, ← add_smul, hab, one_smul]

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

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
zero_mul,

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x + 0 ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 * x + y ∈ Ioc x y

Tactic:
zero_mul,

Goal state after:
case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 + y ∈ Ioc x y
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
⊢ StarConvex 𝕜 y (Iic x)ᶜ

Tactic:
by
  refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_
  rw [mem_compl_iff, mem_Iic] at hz ⊢
  contrapose hz
  refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le
  calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

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

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
hz : 0 * x + y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

Tactic:
zero_mul,

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
hz : 0 + y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ x + 0 * y ∈ Ico x y

Tactic:
zero_mul,

Goal state after:
case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 < a
hb : 0 ≤ 0
hab : a = 1
⊢ x + 0 ∈ Ico x y
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • f x + b • f y ≤ a • B + b • B

Tactic:
gcongr <;> assumption

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
s : AffineSubspace k P
hs : s ∈ t
hv : ∀ i ∈ t, v ∈ i.direction
⊢ v ∈ s.direction

Tactic:
exact hv s hs

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ -x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x ∈ s

Tactic:
refine hs.smul_mem ?_ ha

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a⁻¹ • b‖ ≤ 1
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 t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • t

Tactic:
refine subset_iInter₂ fun a ha ↦ ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • t
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
x : E
s : Set E
⊢ IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Tactic:
by
  simp only [← singleton_union, isVonNBounded_union, isVonNBounded_singleton, true_and]

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
hx_fstsnd : x.1 + x.2 ⊆ U
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)

Tactic:
refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd

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
hx_fstsnd : x.1 + x.2 ⊆ U
y : E
x✝ : y ∈ t
⊢ Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)
Module: Mathlib.Analysis.Convex.Strict

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

Tactic:
by rw [← h, add_zero]

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✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z ↦ c + z) ⁻¹' s
y : E
hy : y ∈ (fun z ↦ c + z) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • g x + g (b • y)) = f (a • g x + b • g y)

Tactic:
g.map_smul

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • g x + b • g y) = f (a • g x + b • g y)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCancelCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z ↦ c + z) ⁻¹' s
y : E
hy : y ∈ (fun z ↦ c + z) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ ⨅ u, p u + q (0 • x - u) = 0 * ⨅ u, p u + q (x - u)

Tactic:
zero_mul,

Goal state after:
case inl
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ ⨅ u, p u + q (0 • x - u) = 0
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₂
⊢ (fun x1 x2 ↦ x1 + x2) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_closedBall, add_sub_add_comm]

Goal state after:
𝕜 : 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₂
Module: Mathlib.Analysis.Seminorm

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

Tactic:
by
  let := AddGroupSeminorm.toSeminormedAddCommGroup p.toAddGroupSeminorm
  simp [ball_eq_metric]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 (0 * r) ⊆ 0 • p.ball 0 r

Tactic:
zero_mul,

Goal state after:
case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 0 ⊆ 0 • p.ball 0 r
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: case intro
ι : 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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂

Tactic:
← b.affineCombination_coord_eq_self q₁,

Goal state after:
case intro
ι : 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✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₁) = q₂
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
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).basisOf = b.basisOf

Tactic:
ext
  simp

Goal state after: