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

Goal state before:
pp: case mp.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk (⇑(pathSetoid X)) x = Quot.mk (⇑(pathSetoid X)) y

Tactic:
exact Quotient.sound (PathConnectedSpace.joined x y)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
refine congr_arg _ (Subtype.ext ?_)

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ ↑⟨2 * ↑(σ t), ⋯⟩ = ↑(σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

Tactic:
refine congr_arg _ (Subtype.ext ?_)

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * ↑(σ t) - 1, ⋯⟩ = ↑(σ ⟨2 * ↑t, ⋯⟩)
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)

Tactic:
rintro st hst
    simp [hst]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
⊢ Continuous[inst✝, _] f → Continuous[inst✝, _] g → Continuous[inst✝, _] fun t ↦ (f t).trans (g t)

Tactic:
by
  intro hf hg
  apply continuous_uncurry_iff.mp
  exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)

Tactic:
refine ⟨min (m % n) (n - m % n), ?_⟩

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
h : ¬x = 0
⊢ rexp (log |x|) = rexp (log x)

Tactic:
exp_log_eq_abs h,

Goal state after:
case neg
x : ℝ
h : ¬x = 0
⊢ rexp (log |x|) = |x|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

pp: case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
· simp [h₀, Real.pi_div_two_pos.ne]

Goal state after:
case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ

Tactic:
by
  rw [← coe_nsmul, two_nsmul, add_halves]

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

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (cexp '' cexp ⁻¹' s)

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (s ∩ range cexp)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hr : x.re = 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr]

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

Goal state before:
pp: case inr.inl.inr.inl
x : ℂ
hr : x.re = 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr]

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

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hr : x.re = 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
simp [hr]

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

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * (↑k * π) + π
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
←
        mul_assoc

Goal state after:
θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * ↑k * π + π
⊢ θ + ψ = 2 * ↑k * π + π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b⁻¹) ^ r = ↑a ^ r / ↑b ^ r

Tactic:
mul_cpow_ofReal_nonneg ha (inv_nonneg_of_nonneg hb),

Goal state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ ↑a ^ r * ↑b⁻¹ ^ r = ↑a ^ r / ↑b ^ r
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
simp [hr]

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

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).cos = (↑x✝).sin

Tactic:
exact Real.cos_sub_pi_div_two _

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

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
simp [hr]

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

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

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: case inl.inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: case inl.inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = -1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: case inl.inr.inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 0
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

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

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

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

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: case inl.inr.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

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

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: case inl.inr.inr.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h✝ : ψ.sign = 1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

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

Goal state before:
pp: x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
by
  rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
  · have : z ≠ 0 := by linarith
    simp [this]
  nth_rw 2 [← NNReal.rpow_one x]
  exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

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 ≠ ∞
this : x ≠ 0
⊢ ↑x ^ (y + z) = ↑x ^ y * ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero this, NNReal.rpow_add this]

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

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
lift x to ℝ≥0 using hx
  by_cases h : y = ∞
  · exact Eventually.of_forall fun n => h.symm ▸ le_top
  · lift y to ℝ≥0 using h
    have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)
    refine this.congr (Eventually.of_forall fun n => ?_)
    rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
by_cases hx : x = ⊤

Goal state after:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ ContinuousAt (fun a ↦ a ^ y) x

case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ∞
⊢ ContinuousAt (fun a ↦ a ^ y) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ z ↔ log x < z * log y

Tactic:
by
  rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
w z : ℂ
h : w.re ≤ z.re
⊢ ‖↑n ^ w‖ ≤ ‖↑n ^ z‖

Tactic:
simp_rw [norm_natCast_cpow_of_pos hn]
  exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast hn) h

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

Goal state before:
pp: a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a⁻¹ ^ (↑n / ↑d)

Tactic:
rw [← Real.rpow_neg_eq_inv_rpow, hb.neg_to_eq rfl rfl]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : Module k V1
inst✝² : AffineSpace V1 P1
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0

Tactic:
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 1) p = (id k P1) p

Tactic:
simp [homothety_apply]

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

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 0) p = (const k P1 c) p

Tactic:
simp [homothety_apply]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * 1 + b * (aq + bq) = 1

Tactic:
habq,

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * 1 + b * 1 = 1
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : Semiring 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : PartialOrder 𝕜
𝕜' : Type u_5
inst✝⁵ : Semiring 𝕜'
inst✝⁴ : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomSurjective σ
F' : Type u_6
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜' F'
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, σ s ≤ σ t ↔ s ≤ t
f : E →ₛₗ[σ] F'
⊢ Convex 𝕜' (⇑f '' s)

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
  obtain ⟨r, rfl⟩ : ∃ r : 𝕜, σ r = a := RingHomSurjective.is_surjective ..
  obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..
  refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
    ?_, by simp⟩
  apply_fun σ using Function.Injective.of_eq_imp_le (hσ.mp ·.le)
  simpa

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ [x -[𝕜] y] ⊆ s.pi fun i ↦ [x i -[𝕜] y i]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : Set ι
x y : (i : ι) → M i
⊢ openSegment 𝕜 x y ⊆ s.pi fun i ↦ openSegment 𝕜 (x i) (y i)

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
⊢ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ (convexHull 𝕜) s → a • x ∈ (convexHull 𝕜) s

Tactic:
refine fun a ha x hx => convexHull_min ?_ this hx a ha

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex 𝕜 {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ s ⊆ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) 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
hU : IsClosed[inst✝¹] U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
by_cases h : (0 : E) ∈ U

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∈ U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∉ U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ IsVonNBounded 𝕜 S

Tactic:
rw [(nhds_basis_balanced 𝕜 E).isVonNBounded_iff]

Goal state after:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ ∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
p p₁ p₂ : P
⊢ p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₂ p₁) r = p

Tactic:
rw [Set.pair_comm, mem_affineSpan_pair_iff_exists_lineMap_eq]

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
p₁ : ι → P
p₂ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁) w -ᵥ p₂

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

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
p₂ : ι → P
p₁ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂) w

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
p : P₁
direction : Submodule k V₁
q : P₂
r : V₁
hr : r ∈ direction
he : f.linear r = q -ᵥ f p
⊢ (r +ᵥ p) -ᵥ p ∈ direction

Tactic:
simp [hr]

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

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₁
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
⊢ EqOn (⇑f.linear) (⇑g.linear) (s -ᵥ s)

Tactic:
rintro - ⟨x, hx, y, hy, rfl⟩

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₁
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
x : P₁
hx : x ∈ s
y : P₁
hy : y ∈ s
⊢ f.linear ((fun x1 x2 ↦ x1 -ᵥ x2) x y) = g.linear ((fun x1 x2 ↦ x1 -ᵥ x2) x y)
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
⊢ EqOn ⇑f ⇑g ↑(affineSpan k s)

Tactic:
rintro - ⟨x, hx, y, hy, rfl⟩

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

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

Tactic:
simp [hr]

Goal state after:
Module: Mathlib.Analysis.Seminorm

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

Tactic:
simp [hr]

Goal state after:
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
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(#{i₂} + 1) ≠ 0

Tactic:
card_singleton

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(1 + 1) ≠ 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), x_1 ∈ {y | 0 (y - x) < r}

Tactic:
simp [hr]

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
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ (affineSpan k s₁).direction = (affineSpan k s₂).direction

Tactic:
exact h.direction_eq

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).ball e r = s✝.inf' hs fun i ↦ (p i).ball e r
⊢ ((Finset.cons a✝ s✝ h✝).sup' ⋯ p).ball e r = (Finset.cons a✝ s✝ h✝).inf' ⋯ fun i ↦ (p i).ball e r

Tactic:
| cons _ _ _ hs ih =>

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
e : E
r : ℝ
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs : s✝.Nonempty
ih : (s✝.sup' hs p).closedBall e r = s✝.inf' hs fun i ↦ (p i).closedBall e r
⊢ ((Finset.cons a✝ s✝ h✝).sup' ⋯ p).closedBall e r = (Finset.cons a✝ s✝ h✝).inf' ⋯ fun i ↦ (p i).closedBall e r

Tactic:
| cons _ _ _ hs ih =>

Goal state after: