mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z

Tactic:
obtain ⟨hx, hy⟩ := hxy.mem
  obtain ⟨hx, hy⟩ := hyz.mem
  simp_all only [joinedIn_iff_joined]
  exact hxy.trans hyz

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
⊢ Inseparable ⇑f ⇑g ↔ Inseparable f g

Tactic:
by
  simp only [inseparable_iff_specializes_and, specializes_coe]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C

Tactic:
enter [

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ |x - ↑(round x)|

Tactic:
rw [abs_sub_round_eq_min, le_inf_iff]

Goal state after:
case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ fract x ∧ r ≤ 1 - fract x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + 1 * f (2 * n) + -1 * 1 * f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x

Tactic:
neg_one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + 1 * f (2 * n) + -f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -1 * 1 * f (2 * n + 1) + -1 * (-1 * 1) * f (2 * n + 1 + 1)

Tactic:
neg_one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -f (2 * n + 1) + - -1 * f (2 * n + 1 + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + 1 * f (2 * n) + -1 * 1 * f (2 * n + 1)

Tactic:
neg_one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + 1 * f (2 * n) + -f (2 * n + 1)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -1 * 1 * f (2 * n + 1) + -1 * (-1 * 1) * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
neg_one_mul,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -f (2 * n + 1) + - -1 * f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ rexp (log x) = x

Tactic:
rw [exp_log_eq_abs hx.ne']

Goal state after:
x : ℝ
hx : 0 < x
⊢ |x| = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ x ≤ rexp (log x)

Tactic:
rw [h_zero, log, dif_pos rfl, exp_zero]

Goal state after:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.re < 0 ∧ z.im = 0 ↔ z.arg = π

Tactic:
arg_eq_pi_iff

Goal state after:
z : ℂ
⊢ z.re < 0 ∧ z.im = 0 ↔ z.re < 0 ∧ z.im = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1

Tactic:
rw [le_sub_iff_add_le]

Goal state after:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt
  · simp
  · exact (log_le_sub_one_of_pos hx).trans (by linarith)

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

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

Tactic:
simpa [hn] using hx

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

Goal state before:
pp: θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
apply iff_of_eq

Goal state after:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ (θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π) = (θ = ↑(π / 2) ∨ θ = ↑(-π / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
two_nsmul_toReal_eq_two_mul

Goal state after:
θ : Angle
⊢ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
      mem_nhdsWithin_of_mem_nhds this] with _ him hre

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [← coe_toReal θ, ← coe_toReal ψ, ← coe_add] at h

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case calc.step
x : ℝ
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
obtain hx | hx := (abs_nonneg x).eq_or_lt'

Goal state after:
case calc.step.inl
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0

Tactic:
exact Real.rpow_eq_zero_iff_of_nonneg x.2

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

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

Tactic:
refine (continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt

Goal state after:
a b : ℝ
h : b ≠ 0
⊢ ↑b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
exact coe_rpow_of_ne_zero hx _

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x ^ 1 = x

Tactic:
by
  cases x
  · exact dif_pos zero_lt_one
  · change ite _ _ _ = _
    simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]
    exact fun _ => zero_le_one.not_gt

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

Goal state before:
pp: x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z

Tactic:
convert! rpow_le_rpow_of_exponent_ge hx1 hx2 hz

Goal state after:
x z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ∞) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ f i ^ r * (∏ i ∈ s, f i) ^ r = (f i * ∏ x ∈ s, f x) ^ r

Tactic:
← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..

Goal state after:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ∞) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ (f i * ∏ i ∈ s, f i) ^ r = (f i * ∏ x ∈ s, f x) ^ r

case insert.hy
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ∞) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ ∏ i ∈ s, f i ≠ ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by
  nth_rw 1 [← rpow_one x]
  nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne']
  rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v : Ray R M
⊢ u • v = v

Tactic:
by
  induction v using Module.Ray.ind
  rw [smul_rayOfNeZero, ray_eq_iff]
  exact SameRay.sameRay_pos_smul_left _ hu

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f : P1 →ᵃ[k] P2
⊢ Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑f

Tactic:
obtain ⟨p⟩ := (inferInstance : Nonempty P1)
  have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd]
  rw [h, Equiv.comp_surjective, Equiv.surjective_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ m 0 • x = -m 1 • y

Tactic:
rwa [neg_smul]

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
s : Set E
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s

Tactic:
simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

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

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

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : 0 ∈ s
x : V
⊢ x ∈ ↑s.direction ↔ x ∈ s

Tactic:
Submodule.mem_toAffineSubspace,

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : 0 ∈ s
x : V
⊢ x ∈ s.direction ↔ x ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Goal state after:
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
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
refine balancedCore_subset_balancedCoreAux.antisymm ?_
  refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)
  exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

Goal state after:
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
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s ∧ Balanced 𝕜 s) id

Tactic:
refine
    (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NormedDivisionRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed[inst✝³] s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed[inst✝³] i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s
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 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

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

Goal state after:
𝕜 : 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 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃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
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)

Tactic:
· rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy a b ha hb hab => ?_⟩
    rw [← neg_le_neg_iff]
    simp_rw [neg_add, Pi.neg_apply, smul_neg, neg_neg]
    exact h hx hy ha hb hab

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 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✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ p (a • x) + q (a • x) = ‖a‖ * (p x + q x)

Tactic:
by simp only [map_smul_eq_mul, map_smul_eq_mul, mul_add]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ⨅ i, ↑(r • 1) * (p i + q (x✝ - i)) = ⨅ u, ↑(r • 1) * p u + ↑(r • 1) * q (x✝ - u)

Tactic:
mul_add

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

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₁
inst✝³ : AffineSpace V₁ P₁
V₂ : Type u_8
P₂ : Type u_9
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P₁
f g : P₁ →ᵃ[k] P₂
h_agree : EqOn (⇑f) (⇑g) s
q : P₁
hq : q ∈ s
x : P₁
hx : x ∈ s
y : V₁
hy : y ∈ vectorSpan k s
⊢ f (y +ᵥ x) = g (y +ᵥ x)

Tactic:
simp [h_agree hx, linear_eqOn_vectorSpan h_agree hy]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ ⨆ p, ↑p x✝ = ⊥ x✝

Tactic:
Real.iSup_of_isEmpty

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ 0 = ⊥ x✝
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case inl
ι : 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
inst✝ : Nonempty ι
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hs : Subsingleton k
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
have hnv := Module.subsingleton k V

Goal state after:
case inl
ι : 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
inst✝ : Nonempty ι
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hs : Subsingleton k
hnv : Subsingleton V
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : IsDomain k
inst✝ : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
x✝ : ∃ z, z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
z : kˣ
hz : z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
⊢ z⁻¹ • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁

Tactic:
simp [← hz]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : IsDomain k
inst✝ : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
x✝ : ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
z : kˣ
hz : z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ z⁻¹ • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂

Tactic:
simp [← hz]

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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0

Tactic:
rw [Finset.weightedVSub_indicator_subset _ _ (Finset.subset_univ s)] at hs

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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i, w i = 0 → (univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (univ.weightedVSub p) ((↑s).indicator w) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]

Tactic:
have hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁ := by
    simp [sub_smul, hp₁, hp₂]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case mp.inl
ι : 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
v : V
p : ι → P
hι : IsEmpty ι
⊢ v ∈ vectorSpan k ∅ → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
vectorSpan_empty,

Goal state after:
case mp.inl
ι : 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
v : V
p : ι → P
hι : IsEmpty ι
⊢ v ∈ ⊥ → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
⊢ LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v

Tactic:
let f : (fun p : P => (p -ᵥ p₁ : V)) '' (s \ {p₁}) → { x : s // x ≠ ⟨p₁, hp₁⟩ } := fun x =>
      ⟨⟨(x : V) +ᵥ p₁, Set.mem_of_mem_sdiff (hv x)⟩, fun hx =>
        Set.notMem_of_mem_sdiff (hv x) (Subtype.ext_iff.1 hx)⟩

Goal state after:
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 : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩
hv : ∀ (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))), ↑v +ᵥ p₁ ∈ s \ {p₁}
f : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁})) → { x // x ≠ ⟨p₁, hp₁⟩ } := fun x ↦ ⟨⟨↑x +ᵥ p₁, ⋯⟩, ⋯⟩
⊢ LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v