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

Goal state before:
pp: case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
· suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
      simp [-zsmul_eq_mul, coe_real_preimage_closedBall_eq_iUnion,
        iUnion_inter, iUnion_ite, this, hε]
    intro z
    simp only [Real.closedBall_eq_Icc] at hs ⊢
    rcases eq_or_ne z 0 with (rfl | hz)
    · simp
    simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_notMem]
    rintro y ⟨⟨hy₁, hy₂⟩, hy₀⟩
    obtain ⟨hy₃, hy₄⟩ := hs hy₀
    rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
    · rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
      · have : ↑z * p ≤ -p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]
      · have : p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]
    · simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
      linarith
    · rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
      · have : -p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]
      · have : ↑z * p ≤ p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2

Tactic:
rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]

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

Goal state before:
pp: ⊢ arccos '' Icc (-1) 1 = Icc 0 π

Tactic:
simpa using cosPartialEquiv.symm.image_source_eq_target

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

Goal state before:
pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.arg = z.arg

Tactic:
by
  simpa [toIocMod_eq_self, two_mul] using z.arg_mem_Ioc

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

Goal state before:
pp: case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = π

Tactic:
← arg_neg_one,

Goal state after:
case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (-1).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ log ((starRingEnd ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ) (log x)

Tactic:
simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]

Goal state after:
x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : (False ∨ sin ((θ + ψ) / 2) = 0) ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
false_or,

Goal state after:
case mp
θ ψ : ℝ
Hcos : sin ((θ + ψ) / 2) = 0 ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
y : ℂ
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · rcases eq_or_ne y 0 with rfl | hy <;> simp [*, zero_zpow]
  · rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]

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

Goal state before:
pp: x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]
  assumption_mod_cast

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

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt arg x

Tactic:
by
  have h₀ : ‖x‖ ≠ 0 := by
    rw [norm_ne_zero_iff]
    exact slitPlane_ne_zero h
  rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h
  rcases h with (hx_re | hx_im | hx_im)
  exacts [(Real.continuousAt_arcsin.comp
          (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_re_pos hx_re).symm,
    (Real.continuous_arccos.continuousAt.comp
            (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
      (arg_eq_nhds_of_im_neg hx_im).symm,
    (Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
      (arg_eq_nhds_of_im_pos hx_im).symm]

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

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

Tactic:
have h_sign' := h_sign

Goal state after:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = ↑π
h' : a = b + ↑π
h_sign' : a.sign = b.sign
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
this : |θ.toReal + ψ.toReal| = π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s

Tactic:
refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)
  obtain ⟨z, hz, rfl⟩ := hθ
  exact continuousAt_sign (hs _ hz).1 (hs _ hz).2

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

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

Tactic:
log_mul ‹_› ‹_›,

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp ((log x + log y) * z) = rexp (log x * z) * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: b : ℂ
hb : b ≠ 0
⊢ (fun x ↦ 0 ^ x) =ᶠ[𝓝 b] 0

Tactic:
by
  suffices ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [zero_cpow hx, Pi.zero_apply]
  exact IsOpen.eventually_mem isOpen_ne hb

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

Goal state before:
pp: case refine_2
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg| * |z.2.im| ≤ π * C

Tactic:
exact
      mul_le_mul (abs_le.2 ⟨(neg_pi_lt_arg _).le, arg_le_pi _⟩) hz.le (_root_.abs_nonneg _)
        Real.pi_pos.le

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

Goal state before:
pp: case neg
y z : ℝ
hyz : 0 < y + z
hx : 0 ≠ ∞
hy' : ¬0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
have hz' : 0 < z := by linarith

Goal state after:
case neg
y z : ℝ
hyz : 0 < y + z
hx : 0 ≠ ∞
hy' : ¬0 < y
hz' : 0 < z
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.top
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ ∞
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

Tactic:
rcases hz with hz | hz

Goal state after:
case inl.top.inl
z : ℝ
hxy : 0 ≤ ∞
hz : z < 0
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.top.inr
z : ℝ
hxy : 0 ≤ ∞
hz : 0 < z
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

Tactic:
rcases hz with hz | hz

Goal state after:
case inl.coe.inl
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : z < 0
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

case inl.coe.inr
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : 0 < z
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.top
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

Tactic:
rcases hz with hz | hz

Goal state after:
case inr.inr.top.inl
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : z < 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

case inr.inr.top.inr
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : 0 < z
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

Tactic:
rcases hz with hz | hz

Goal state after:
case inr.inr.coe.top.inl
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : z < 0
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

case inr.inr.coe.top.inr
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : 0 < z
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb : 1 ≤ 1
a✝ : ℝ
⊢ ∀ ⦃b : ℝ⦄, a✝ ≤ b → (fun x ↦ 1 ^ x) a✝ ≤ (fun x ↦ 1 ^ x) b

Tactic:
_

Goal state after:
hb : 1 ≤ 1
a✝ b✝ : ℝ
⊢ a✝ ≤ b✝ → (fun x ↦ 1 ^ x) a✝ ≤ (fun x ↦ 1 ^ x) b✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb : 1 ≤ 1
a✝ b✝ : ℝ
⊢ a✝ ≤ b✝ → (fun x ↦ 1 ^ x) a✝ ≤ (fun x ↦ 1 ^ x) b✝

Tactic:
_

Goal state after:
hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) a✝¹ ≤ (fun x ↦ 1 ^ x) b✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝ : ℝ
⊢ ∀ ⦃b : ℝ⦄, a✝ ≤ b → (fun x ↦ 1 ^ x) b ≤ (fun x ↦ 1 ^ x) a✝

Tactic:
_

Goal state after:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝ b✝ : ℝ
⊢ a✝ ≤ b✝ → (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝ b✝ : ℝ
⊢ a✝ ≤ b✝ → (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝

Tactic:
_

Goal state after:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ b = a ^ n

Tactic:
rw [h.1, Real.rpow_natCast]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

Tactic:
simp [enorm, nnnorm_rpow_of_nonneg hx, coe_rpow_of_nonneg _ hy]

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:
simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = y + y
⊢ x = y

Tactic:
← two_smul k y,

Goal state after:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_2
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₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₂ / (r₁ + r₂)) • (v₁ + v₂)

pp: case inr.inr.refine_3
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₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)

Tactic:
· rw [div_eq_inv_mul, mul_smul, smul_add, ← H, ← add_smul, add_comm r₂, inv_smul_smul₀ h₁₂.ne']

Goal state after:
case inr.inr.refine_3
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₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ / (r₁ + r₂)) • (v₁ + v₂)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine ⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
⊢ (∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : 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
⊢ y ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

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

Goal state before:
pp: case mp
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
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
⊢ p ∈ s₁ → p ∈ s₂

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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
⊢ p ∈ s₂ → p ∈ s₁

Tactic:
· intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq2
    rw [← hd]
    exact vsub_mem_direction hp hq1

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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
⊢ p ∈ s₂ → p ∈ s₁
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
hs : s.Nonempty
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun x ↦ r • x) y ∈ balancedHull 𝕜 s
⊢ (fun x ↦ r • x) y ∈ t

Tactic:
exact ht.smul_mem hr (h hy)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
⊢ x ∈ t → (fun x ↦ 0 • x) x ∈ s

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
x : E
a✝ : x ∈ t
⊢ (fun x ↦ 0 • x) x ∈ 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
inst✝ : AffineSpace V P
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ p x h

Tactic:
suffices ∃ (hx : x ∈ affineSpan k s), p x hx from this.elim fun hx hc ↦ hc
  -- TODO: `induction h using affineSpan_induction` gives the error:
  -- extra targets for '@affineSpan_induction'
  -- It seems that the `induction` tactic has decided to ignore the clause
  -- `using affineSpan_induction` and use `Exists.rec` instead.
  refine affineSpan_induction h ?mem ?smul_vsub_vadd
  · exact fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩
  · exact fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
⊢ x ∈ univ →
    ∀ ⦃y : E⦄, y ∈ univ → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝ : x ∈ univ
⊢ ∀ ⦃y : E⦄, y ∈ univ → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝ : x ∈ univ
y : E
⊢ y ∈ univ → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝¹ : x ∈ univ
y : E
a✝ : y ∈ univ
⊢ x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝¹ : x ∈ univ
y : E
a✝ : y ∈ univ
⊢ x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ) x y

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝² : x ∈ univ
y : E
a✝¹ : y ∈ univ
a✝ : x ≠ y
⊢ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝² : x ∈ univ
y : E
a✝¹ : y ∈ univ
a✝ : x ≠ y
a b : 𝕜
⊢ 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior univ

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝³ : x ∈ univ
y : E
a✝² : y ∈ univ
a✝¹ : x ≠ y
a b : 𝕜
a✝ : 0 < a
⊢ 0 < b → a + b = 1 → a • x + b • y ∈ interior univ
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝³ : x ∈ univ
y : E
a✝² : y ∈ univ
a✝¹ : x ≠ y
a b : 𝕜
a✝ : 0 < a
⊢ 0 < b → a + b = 1 → a • x + b • y ∈ interior univ

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁴ : x ∈ univ
y : E
a✝³ : y ∈ univ
a✝² : x ≠ y
a b : 𝕜
a✝¹ : 0 < a
a✝ : 0 < b
⊢ a + b = 1 → a • x + b • y ∈ interior univ
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁴ : x ∈ univ
y : E
a✝³ : y ∈ univ
a✝² : x ≠ y
a b : 𝕜
a✝¹ : 0 < a
a✝ : 0 < b
⊢ a + b = 1 → a • x + b • y ∈ interior univ

Tactic:
_

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ interior univ
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✝ : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ interior s

Tactic:
apply h.openSegment_subset hx hy hxy

Goal state after:
𝕜 : 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✝ : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ x ∈ t • interior s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]
  exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one_of_one_lt₀ ht)

Goal state after: