mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z

Tactic:
convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
            continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1
  lift z to ℝ using him
  simpa using hre.ne

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

Goal state before:
pp: x : ℂ
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rw [norm_eq_one_iff]
  constructor
  · rintro ⟨θ, rfl⟩
    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
    · convert! toIocMod_mem_Ioc _ _ _
      ring
    · rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
  · rintro ⟨θ, _, rfl⟩
    exact ⟨θ, rfl⟩

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

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

Tactic:
iff_false,

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ ¬z.arg ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
iff_false,

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ ¬-(π / 2) ≤ z.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) - -1 * π = 0
⊢ ↑θ = ↑ψ

Tactic:
zsmul_eq_mul,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑n * (2 * π) - -1 * π = 0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
zsmul_eq_mul,

Goal state after:
θ ψ : ℝ
⊢ ↑(-toIcoDiv two_pi_pos ψ θ) * (2 * π) = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
zsmul_eq_mul,

Goal state after:
θ ψ : ℝ
⊢ ↑(-toIocDiv two_pi_pos ψ θ) * (2 * π) = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π ↔ θ = ↑π

Tactic:
← toReal_inj,

Goal state after:
θ : Angle
⊢ θ.toReal = π ↔ θ.toReal = (↑π).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π / 2 ↔ θ = ↑(π / 2)

Tactic:
← toReal_inj,

Goal state after:
θ : Angle
⊢ θ.toReal = π / 2 ↔ θ.toReal = (↑(π / 2)).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = -π / 2 ↔ θ = ↑(-π / 2)

Tactic:
← toReal_inj,

Goal state after:
θ : Angle
⊢ θ.toReal = -π / 2 ↔ θ.toReal = (↑(-π / 2)).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
zsmul_eq_mul,

Goal state after:
θ : ℝ
k : ℤ
⊢ (↑(θ - ↑k * (2 * π))).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π → a = b

pp: case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π

Tactic:
· intro h
    rcases h with h1 | h2
    · exact h1
    · have : a.sign = (b + π).sign := by aesop
      rw [Real.Angle.sign_add_pi] at this
      have := congr_arg (· = b.sign) this
      aesop

Goal state after:
case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
rw [forall_mem_cons] at h
    rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]

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

Goal state before:
pp: k a b : ℝ
ha' : a < b
⊢ Tendsto (fun x ↦ rexp (a * x) * x ^ k / rexp (b * x)) atTop (𝓝 0)

Tactic:
simp_rw [← div_mul_eq_mul_div₀, ← Real.exp_sub, ← sub_mul, ← neg_sub b a,
    mul_comm _ (_ ^ k)]

Goal state after:
k a b : ℝ
ha' : a < b
⊢ Tendsto (fun x ↦ x ^ k * rexp (-(b - a) * x)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: c : ℂ
⊢ (fun t ↦ ‖↑t ^ c‖) =ᶠ[atTop] fun t ↦ t ^ c.re

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖↑t ^ c‖ = t ^ c.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
simpa using rpow_sub_natCast hx y 1

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

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

Tactic:
simpa using rpow_sub_natCast hx y 1

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

Goal state before:
pp: a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
by
  simp only [rpow_def]
  refine Complex.continuous_re.continuousAt.comp ?_
  refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt
  norm_cast

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

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

Tactic:
cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'

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

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

Tactic:
← rpow_le_rpow_iff _ hy hz,

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ (x ^ z⁻¹) ^ z ≤ y ^ z ↔ x ≤ y ^ z

x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
⊢ ∞ ^ 0 = 1

Tactic:
· dsimp only [(· ^ ·), Pow.pow, rpow]
      simp [← none_eq_top]

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 0 = 1

Tactic:
· dsimp only [(· ^ ·), Pow.pow, rpow]
      simp [← none_eq_top]

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

Goal state before:
pp: z w : ℂ
h₁ : ¬(z, w).1 ≤ 0 ∨ ¬¬(z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

Tactic:
Classical.not_not,

Goal state after:
z w : ℂ
h₁ : ¬(z, w).1 ≤ 0 ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
rcases eq_or_ne y 0 with rfl | hy0

Goal state after:
case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
        rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
      simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
        mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑↑⟨p, hp⟩ ^ (-s)‖ ≤ 1 / 2
⊢ False

Tactic:
simp only at this

Goal state after:
p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
H : 1 = ↑p ^ (-s)
this : ‖↑p ^ (-s)‖ ≤ 1 / 2
⊢ False
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
x : Ray R M
⊢ - -x = x

Tactic:
apply ind R (by simp) x

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
⊢ 0 = a → a • x + b • y = y

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
· rintro rfl
    rw [← zero_add b, hab, one_smul, zero_smul, zero_add]

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y
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
⊢ [c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x}

Tactic:
apply segment_inter_eq_endpoint_of_linearIndependent_sub

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
⊢ LinearIndependent 𝕜 ![c + t • y - (c + x), c + s • y - (c + x)]
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
⊢ LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]

Tactic:
nontriviality 𝕜

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 𝕜 ![-1 • x + t • y, -1 • x + s • y]
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ Ioo y x = Ioo (min x y) x

Tactic:
min_eq_right h.le

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ Ioo y x = Ioo y x
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 + 0 = 1
hz : a * 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:
rw [add_zero] at hab
      rw [hab, one_mul, zero_mul, add_zero] at hz
      exact (hz.1.ne rfl).elim

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 : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv
  rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
  rw [hv]
  convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp
  rw [one_smul]

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
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (v₁ +ᵥ p₂) -ᵥ p₃ ∈ vectorSpan k s

Tactic:
hp₃,

Goal state after:
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
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (v₁ +ᵥ p₂) -ᵥ (v₂ +ᵥ p₄) ∈ vectorSpan k s
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 • B + b • B ≤ B

Tactic:
by rw [← add_smul, hs, one_smul]

Goal state after:
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
⊢ x ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, ← hy₂, 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.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
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)

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
⊢ a • y • V ⊆ U
Module: Mathlib.Analysis.LocallyConvex.Bounded

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

Tactic:
let : NontriviallyNormedField 𝕜 := ⟨h⟩

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 : TotallyBounded s
h : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h }
⊢ Bornology.IsVonNBounded 𝕜 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✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ x, 1 < ‖x‖
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
else

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 : TotallyBounded s
h : ¬∃ x, 1 < ‖x‖
⊢ Bornology.IsVonNBounded 𝕜 s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ (normSeminorm 𝕜 E).ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 ((normSeminorm 𝕜 E).ball 0 i) s

Tactic:
exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

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 → β
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
⊢ StrictConvexOn 𝕜 s f

Tactic:
refine ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
  wlog h : x < y
  · rw [add_comm (a • x), add_comm (a • f x)]
    rw [add_comm] at hab
    exact this hs hf y hy x hx hxy.symm b a hb ha hab (hxy.lt_or_gt.resolve_left h)
  exact hf hx hy h ha hb hab

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

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
i₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
· exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

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

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
i₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v

Tactic:
· exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

Goal state after:
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 : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
v : V
⊢ (s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice ⋯)) w = (s.weightedVSub p) w

Tactic:
weightedVSubOfPoint_vadd,

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
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
v : V
⊢ (s.weightedVSubOfPoint p (-v +ᵥ Classical.choice ⋯)) w = (s.weightedVSub p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

Tactic:
Seminorm.coe_sSup_eq' H,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (⨆ p, ⇑↑p) 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
p : ι → P
i : ι
⊢ centroid k {i} p = p i

Tactic:
by
  simp [centroid_def, affineCombination_apply]

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

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

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  rcases t.eq_empty_or_nonempty with rfl | ht
  · simp
  apply AffineSubspace.ext_of_direction_eq
  · simp [direction_prod_eq, Set.nonempty_iff_ne_empty.mp, hs, ht, direction_affineSpan,
      vectorSpan_prod_eq]
  · obtain ⟨x, hx⟩ := hs
    obtain ⟨y, hy⟩ := ht
    use ⟨x, y⟩
    simp [mem_affineSpan, hx, hy]

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

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
      AffineSubspace.vsub_mem_direction h h0

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction
⊢ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ p (x✝ - x) < r ↔ False

Tactic:
iff_false,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ ¬p (x✝ - x) < r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ p.closedBall x r ↔ x✝ ∈ ∅

Tactic:
Seminorm.mem_closedBall,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ p (x✝ - x) ≤ r ↔ x✝ ∈ ∅
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ p (x✝ - x) ≤ r ↔ False

Tactic:
iff_false,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ ¬p (x✝ - x) ≤ r
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)

Tactic:
rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)