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

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
  have h : ∀ x : X, Continuous fun y => g (x, y) := by
    intro x
    obtain ⟨x₀, rfl⟩ := hf.surjective x
    exact (Gf x₀).continuous
  let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
  have : Continuous G := by
    rw [hf.continuous_iff]
    exact Gf.continuous
  exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

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

Goal state before:
pp: p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖

Tactic:
simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_2
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
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (γ₂ p.1).extend (2 * ↑p.2 - 1)

Tactic:
change
      Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))

Goal state after:
case refine_2
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
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ((fun p ↦ (γ₂ p.1).extend p.2) ∘ Prod.map id fun x ↦ 2 * ↑x - 1)
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

Tactic:
have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
      simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]

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

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

Tactic:
arcsin_of_one_le hx,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ π / 2 - π / 2 = 0
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 (-π) π
this : (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg = z.arg + ↑N * (2 * π)
⊢ (↑‖z‖ * (cos (↑z.arg + ↑N * (2 * ↑π)) + sin (↑z.arg + ↑N * (2 * ↑π)) * I)).arg ∈ Ioc (-π) π

Tactic:
rwa [this]

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

Goal state before:
pp: z : ℂ
h₀ : z ≠ 0
⊢ 0 * ‖z‖ ≤ z.im ↔ 0 ≤ z.im

Tactic:
zero_mul

Goal state after:
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ z.im ↔ 0 ≤ z.im
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x / y| = rexp (log x - log y)

Tactic:
exp_sub,

Goal state after:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x / y| = rexp (log x) / rexp (log y)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hbdd
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, ‖↑⌊x⌋₊ - x‖ ≤ ‖1‖

Tactic:
apply Eventually.mono _ (fun x h ↦ norm_le_norm_of_abs_le_abs h)

Goal state after:
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, |↑⌊x⌋₊ - x| ≤ |1|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
⊢ log (∏ᶠ (a : α), f a) = ∑ᶠ (a : α), log (f a)

Tactic:
by
  classical
  have H : (fun i ↦ log (f i)).support = f.mulSupport := by
    grind [mem_mulSupport, mem_support, log_eq_zero]
  have H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a) := by
    simp [HasFiniteMulSupport, HasFiniteSupport, H]
  simp only [finprod_def, finsum_def]
  by_cases h' : HasFiniteMulSupport f
  · simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]
  · simp [h', mt H'.mpr h']

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

Goal state before:
pp: x y : ℂ
⊢ cexp x = cexp y ↔ cexp (x - y) = 1

Tactic:
exp_sub,

Goal state after:
x y : ℂ
⊢ cexp x = cexp y ↔ cexp x / cexp y = 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = rexp (log (x + y) - log x)

Tactic:
exp_sub,

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = rexp (log (x + y)) / rexp (log x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ 0 * sin ((θ - ψ) / 2) = 0

Tactic:
zero_mul

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ → cos θ = cos ψ

Tactic:
· rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
    rintro (⟨k, H⟩ | ⟨k, H⟩)
    · rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
    rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π - (↑θ + ↑ψ) = 0
⊢ ↑θ + ↑ψ = ↑π

Tactic:
sub_eq_zero

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑π = ↑θ + ↑ψ
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 0 * cos ((θ + ψ) / 2) = 0

Tactic:
zero_mul

Goal state after:
case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π = sphere 0 1

Tactic:
ext; simpa using norm_eq_one_iff'.symm

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

Goal state before:
pp: case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ 0 = 0 * ↑b ^ r

Tactic:
zero_mul

Goal state after:
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
⊢ θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑π

Tactic:
induction ψ using Real.Angle.induction_on
  exact sin_eq_real_sin_iff_eq_or_add_eq_pi

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

Goal state before:
pp: ⊢ Function.Antiperiodic sin ↑π

Tactic:
by
  intro θ
  induction θ using Real.Angle.induction_on
  exact Real.sin_antiperiodic _

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

Goal state before:
pp: θ : ℝ
⊢ |(-↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
by
  refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
  by_cases hnegpi : θ = π; · simp [hnegpi, Real.pi_pos.le]
  rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
rw [arg_real_mul _ hr, ← exp_mul_I, arg_exp_mul_I]

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

Goal state before:
pp: θ : Angle
h : θ ≠ ↑π
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
  · simp [ht, toReal_neg_iff_sign_neg.1 ht]
  · simp [sign, ht, ← sin_toReal]
  · rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]

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

Goal state before:
pp: r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun x ↦ x ^ r) l)).prod = (List.map toReal l).prod ^ r
⊢ (List.map (fun x ↦ x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Tactic:
rw [List.map_map] at this ⊢

Goal state after:
r : ℝ
l : List ℝ≥0
this : (List.map (toReal ∘ fun x ↦ x ^ r) l).prod = (List.map toReal l).prod ^ r
⊢ (List.map ((fun x ↦ x ^ r) ∘ toReal) l).prod = (List.map toReal l).prod ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by
  rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

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

Goal state before:
pp: y z : ℝ
x : ℝ≥0
hx : ↑x ≠ 0
h'x : ↑x ≠ ∞
h : x = 0
⊢ False

Tactic:
simp [h] at hx

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

Goal state before:
pp: x y : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
⊢ max x y ^ p = max (x ^ p) (y ^ p)

Tactic:
rcases le_total x y with hxy | hxy
  · rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hxy hp)]
  · rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hxy hp)]

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

Goal state before:
pp: x y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ by rw [H]⟩
  rcases hx₁.lt_or_gt with h | h
  · exact (strictAnti_rpow_of_base_lt_one hx₀ h).injective H
  · exact (strictMono_rpow_of_base_gt_one h).injective H

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

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

Tactic:
by
  rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
Fintype.not_linearIndependent_iff

Goal state after:
case neg
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: P₁ : Type u_2
V₁ : Type u_6
inst✝³ : AddCommGroup V₁
inst✝² : AffineSpace V₁ P₁
R' : Type u_10
inst✝¹ : CommRing R'
inst✝ : Module R' V₁
c p : P₁
⊢ (homothety c (-1)) p = (pointReflection R' c) p

Tactic:
simp [homothety_apply, Equiv.pointReflection_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ i, ↑i)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: case h₁
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
⊢ f.linear = g.linear

Tactic:
apply LinearMap.pi_ext
    intro i x
    have s₁ := h i x
    have s₂ := f.map_vadd 0 (Pi.single i x)
    have s₃ := g.map_vadd 0 (Pi.single i x)
    rw [vadd_eq_add, add_zero] at s₂ s₃
    replace h₂ := h i 0
    simp only [Pi.single_zero] at h₂
    rwa [s₂, s₃, h₂, vadd_right_cancel_iff] at s₁

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩
  rcases h with ⟨r, hr, rfl⟩
  exact SameRay.sameRay_pos_smul_right x hr

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 ≤ b_1 ∧ 0 < a_1 + b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z

Tactic:
use a, b, ha, hb

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z

Tactic:
use a, b, ha, hb

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
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 z : E
⊢ x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x)

Tactic:
refine ⟨sameRay_of_mem_segment, fun 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 z : E
h : SameRay 𝕜 (x - y) (z - x)
⊢ x ∈ [y -[𝕜] z]
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)

Tactic:
rw [sUnion_eq_iUnion]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ i, ↑i)
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s

Tactic:
balancedHull,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s ⊆ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q ∈ {p}

Tactic:
Set.mem_singleton_iff

Goal state after:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ ↑s₁ ∩ ↑s₂
q : P
⊢ q ∈ ↑s₁ ∩ ↑s₂ ↔ q = p
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✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
this : ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s = ⋃ r, ⋃ (_ : ‖r‖ ≤ 1 ∧ r ≠ 0), r • s
⊢ IsOpen[inst✝¹] (balancedHull 𝕜 s)

Tactic:
balancedHull,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : IsOpen[inst✝¹] s
hzero : 0 ∈ s
this : ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s = ⋃ r, ⋃ (_ : ‖r‖ ≤ 1 ∧ r ≠ 0), r • s
⊢ IsOpen[inst✝¹] (⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s)
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ i, ↑i)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : ConvexOn 𝕜 (f '' s) g
hf : StrictConvexOn 𝕜 s f
hg' : StrictMonoOn g (f '' s)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • f x + b • f y) ≤ a • (g ∘ f) x + b • (g ∘ f) y

Tactic:
· exact hg.right (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab

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

Goal state before:
pp: case hb
𝕜 : 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✝¹ : IsOrderedAddMonoid β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ r

pp: case hb
𝕜 : 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✝¹ : IsOrderedAddMonoid β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
· exact hx.2.le

Goal state after:
case hb
𝕜 : 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✝¹ : IsOrderedAddMonoid β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r
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
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
mem_vectorSpan_pair

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
p₁ p₂ : P
v : V
⊢ (∃ r, r • (p₁ -ᵥ p₂) = v) ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
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
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ ∑ i ∈ Finset.subtype pred s, w ↑i • (p ↑i -ᵥ b) = ∑ i ∈ s with pred i, w i • (p i -ᵥ b)

Tactic:
← sum_subtype_eq_sum_filter

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
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ ∑ i ∈ Finset.subtype pred s, w ↑i • (p ↑i -ᵥ b) = ∑ x ∈ Finset.subtype pred s, w ↑x • (p ↑x -ᵥ b)
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✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ 0 * f 0 = 0

Tactic:
zero_mul

Goal state after:
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✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ 0 = 0
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
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
⊢ ∀ x ∈ s, w x • (p x -ᵥ p i) = 0

Tactic:
intro i2 hi2

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
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0