mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z < ε

Tactic:
by
  refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le)
    (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
      rw [← add_div, div_self (add_pos hε hδ).ne']).imp
    fun y hy => ?_
  rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
  rw [← div_lt_one (add_pos hε hδ)] at h
  exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ (∃ z ∈ s, dist x z < ε + δ) → ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
rintro ⟨z, hz, hxz⟩

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℤ
⊢ cos (↑n * (2 * ↑π) + ↑π) = -1

Tactic:
by
  simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)
  · simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]
  · exact smul_closedBall' hc x r

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
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen[inst✝] U}
⊢ IsOpen[induced (restrict K) compactOpen] {f | MapsTo (⇑f) K U}

Tactic:
convert! isOpen_induced (isOpen_setOfPred_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)

Goal state after:
case e'_3
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : U ∈ {U | IsOpen[inst✝] U}
⊢ {f | MapsTo (⇑f) K U} = restrict K ⁻¹' {f | MapsTo (⇑f) univ U}
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ¬Summable f

Tactic:
have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 := by
    filter_upwards [h.eventually_const_le hl] with _ hn hc
    rw [hc, _root_.div_zero] at hn
    linarith

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
⊢ ¬Summable f
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 : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C * (‖z‖ ^ n / ‖w‖ ^ n)

Tactic:
← mul_comm_div

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 : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
this : 0 < ↑N
⊢ x = y

Tactic:
rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico,
    div_left_inj' this.ne', Nat.cast_inj, (val_injective N).eq_iff] at hxy

Goal state after:
case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_
  rw [Filter.EventuallyEq, eventually_nhds_iff]
  exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ { toFun := (fun t ↦ if t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * t) else (Path.pi γ₁).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      t i =
    (Path.pi fun i ↦
        { toFun := (fun t ↦ if t ≤ 1 / 2 then (γ₀ i).extend (2 * t) else (γ₁ i).extend (2 * t - 1)) ∘ Subtype.val,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ })
      t i

Tactic:
simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]

Goal state after:
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ (if ↑t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * ↑t) else (Path.pi γ₁).extend (2 * ↑t - 1)) i =
    if ↑t ≤ 1 / 2 then (γ₀ i).extend (2 * ↑t) else (γ₁ i).extend (2 * ↑t - 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) - f (2 * n + 1) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x

Tactic:
sub_le_iff_le_add

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 + f (2 * n) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + 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 + f (2 * n + 2) - f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
sub_le_iff_le_add

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 + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + f (2 * n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x

Tactic:
by rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]

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

Goal state before:
pp: x : ℂ
⊢ ‖x‖ * Real.sin x.arg = x.im

Tactic:
by
  simpa [-norm_mul_cos_add_sin_mul_I] using! congr_arg im (norm_mul_cos_add_sin_mul_I x)

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
zsmul_eq_mul

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + ↑N * (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mpr
x : ℝ
⊢ x = 0 ∨ x = 1 ∨ x = -1 → log x = 0

Tactic:
rintro (rfl | rfl | rfl)

Goal state after:
case mpr.inl
⊢ log 0 = 0

case mpr.inr.inl
⊢ log 1 = 0

case mpr.inr.inr
⊢ log (-1) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (x * ↑r) = ↑(Real.log r) + log x

Tactic:
by rw [mul_comm, log_ofReal_mul hr hx]

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

Goal state before:
pp: s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ log s.prod = (Multiset.map (fun x ↦ log x) s).sum

Tactic:
rw [← prod_toList, log_list_prod (by simp_all), sum_map_toList]

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

Goal state before:
pp: case refine_1
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑(Real.log ‖x‖)) x

pp: case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x

Tactic:
· refine continuous_ofReal.continuousAt.comp ?_
    refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt
    exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h

Goal state after:
case refine_2
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (fun x ↦ ↑x.arg * I) x
Module: Mathlib.Tactic.Qify

Goal state before:
pp: a b : ℤ
⊢ a = b ↔ ↑a = ↑b

Tactic:
simp only [Int.cast_inj]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ - -⌊(-π + 2 * π - θ) / (2 * π)⌋ • (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
zsmul_eq_mul

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
this : θ ≠ ψ + ↑π
⊢ 2 • θ = 2 • ψ ↔ θ = ψ

Tactic:
simp [this, two_nsmul_eq_iff]

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

Goal state before:
pp: case inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
· obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]
    have hsa' : (-θ + -ψ).sign ≠ 1 := by
      rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
    convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1
    all_goals simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

Goal state after:
case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Goal state after:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x ↦ ↑a ^ ↑x) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Goal state after:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x ↦ ↑a ^ ↑x) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

pp: case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x

Tactic:
· have : z ≠ 0 := by linarith
    simp [this]

Goal state after:
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
← rpow_eq_rpow_iff hz,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z = (y ^ z⁻¹) ^ z ↔ x ^ z = y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
← rpow_eq_rpow_iff hz,

Goal state after:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ (x ^ z⁻¹) ^ z = y ^ z ↔ x = y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1

Tactic:
grind [rpow_rpow_inv_eq_iff]

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

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

Tactic:
have : x ≠ 0 := fun h => by simp [h] at hx

Goal state after:
case coe
y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ∞
this : x ≠ 0
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
have : x ≠ 0 := fun h => by simp [h] at hx
    simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

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

Goal state before:
pp: case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z

pp: case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

Tactic:
· rw [rpow_zero, one_mul, zero_add]

Goal state after:
case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1

Tactic:
grind [rpow_rpow_inv_eq_iff]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x ^ (↑n * (↑n)⁻¹) = x

Tactic:
mul_inv_cancel₀ (by positivity),

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ x ^ 1 = x
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
p₁ p₂ : P
⊢ p₂ -ᵥ midpoint R p₂ p₁ = ⅟2 • (p₂ -ᵥ p₁)

Tactic:
left_vsub_midpoint

Goal state after:
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
p₁ p₂ : P
⊢ ⅟2 • (p₂ -ᵥ p₁) = ⅟2 • (p₂ -ᵥ 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 = x ↔ x = y

Tactic:
midpoint_eq_left_iff

Goal state after:
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
⊢ x = y ↔ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ f x = f.linear x +ᵥ f 0

Tactic:
by rw [← f.map_vadd, vadd_eq_add, add_zero]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = ⇑f - fun x ↦ f 0

Tactic:
by
  rw [decomp]
  simp only [map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

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

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

Tactic:
convert! H using 1 <;> simp [sub_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0

Tactic:
rintro ⟨r, hr, rfl⟩
    simp [hx, hr.le, hr.ne']

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

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

Tactic:
rintro a ⟨h₀, h₁⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
rcases lt_trichotomy a c with (hac | rfl | hca)

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)
Module: Mathlib.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 : Submodule k V
x : V
⊢ x ∈ (↑s).direction ↔ x ∈ s

Tactic:
simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ((convexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ≠ ∅ ↔ s.Nonempty
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ≠ ∅ ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ≠ ∅ ↔ 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:
segment_eq_image₂,

Goal state after:
𝕜 : 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)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = [(x₁, y) -[𝕜] (x₂, y)]
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)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = [(x₁, y) -[𝕜] (x₂, y)]

Tactic:
segment_eq_image₂,

Goal state after:
𝕜 : 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)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
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:
segment_eq_image₂,

Goal state after:
𝕜 : 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)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = [(x, y₁) -[𝕜] (x, y₂)]
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)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} = [(x, y₁) -[𝕜] (x, y₂)]

Tactic:
segment_eq_image₂,

Goal state after:
𝕜 : 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)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Tactic:
refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)

Goal state after:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)