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

Goal state before:
pp: ⊢ Filter.map Subtype.val atTop = atTop

Tactic:
map_val_Ioi_atTop

Goal state after:
⊢ atTop = atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ
⊢ (IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖rexp (f x)‖ / ‖rexp (g x)‖) ↔
    IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (f - g)

Tactic:
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ uniformity (M ⧸ S) = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | dist p.1 p.2 < ε}

Tactic:
by
    rw [uniformity_eq_comap_nhds_one_left, (nhds_one_hasBasis.comap _).eq_biInf]
    simp only [dist, preimage_ofPred_eq, norm_eq_groupSeminorm]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s

Tactic:
simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this : Summable fun n ↦ ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n
n : ℕ
⊢ ↑n ^ k * r ^ n = ↑((n + k).descFactorial k) * r ^ n - ∑ i ∈ Finset.range k, ↑(a i) * ↑n ^ i * r ^ n

Tactic:
simp [ha n, add_mul, sum_mul]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ f x ⤳ f (γ' 0)

Tactic:
hγ',

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ f x ⤳ γ 0
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ f (γ' 1) ⤳ f y

Tactic:
hγ',

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ γ 1 ⤳ f y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ γ' 1 ⤳ y

Tactic:
rw [← hf.specializes_iff, hγ', γ.target]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x : (i : ι) → Z i
hx : ∀ (i : ι), x i ∈ s i
hjoin : ∀ (i : ι) ⦃y : Z i⦄, y ∈ s i → JoinedIn (s i) (x i) y
⊢ IsPathConnected (univ.pi s)

Tactic:
exact ⟨x, by simpa, fun y hy ↦ .pi fun i ↦ hjoin i (by grind)⟩

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
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (min 0 0) = a

Tactic:
rw [min_self, γ.extend_zero]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (IccExtend ⋯ f 0) (IccExtend ⋯ f 1) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t

Tactic:
· rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
      rcases this t.2 with ⟨w, hw₁, hw₂⟩
      rw [IccExtend_of_mem _ _ hw₁] at hw₂
      exact ⟨_, hw₂⟩

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

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

Tactic:
simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
    Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)

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

Goal state before:
pp: case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x

pp: case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x

Tactic:
· rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]

Goal state after:
case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
· rw [not_le] at hx₂
    rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
    nlinarith

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
⊢ Tendsto (fun x ↦ arccos (f x)) l (𝓝[≤] arccos x)

Tactic:
refine ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h

Goal state after:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : y ∈ Ici x
⊢ arccos y ∈ Iic (arccos x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
Angle.coe,

Goal state after:
ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
sum_map_toList

Goal state after:
s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ (Multiset.map (fun x ↦ log x) s).sum = (Multiset.map (fun x ↦ log x) s).sum
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case 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, hr.not_ge, hi.le, hi.ne, not_le.2 hi, add_comm]

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

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

Tactic:
angle_eq_iff_two_pi_dvd_sub,

Goal state after:
case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ = -↑ψ → cos θ = cos ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
exact cpow_zero _

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

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ

Tactic:
angle_eq_iff_two_pi_dvd_sub,

Goal state after:
case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
by
  rcases le_or_gt 0 (re z) with hre | hre
  · simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or]
  simp only [hre.not_ge, false_or]
  rcases le_or_gt 0 (im z) with him | him
  · simp only [him.not_gt]
    rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
      Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
      abs_of_nonneg him, abs_im_lt_norm]
    exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]
  · simp only [him]
    rw [iff_true, arg_of_re_neg_of_im_neg hre him]
    exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

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

Goal state before:
pp: case mpr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π

Tactic:
have h' : θ.toReal ≠ π := by simp [h]

Goal state after:
case mpr
θ : Angle
h : θ ≠ ↑π
h' : θ.toReal ≠ π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z

Tactic:
simp [Real.cos]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

Tactic:
← norm_cpow_real

Goal state after:
x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
continuousAt_congr (rpow_eq_nhds_of_neg hp)

Goal state after:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
⊢ y ^ z ≤ x ^ z

Tactic:
by
  have := hx.trans_le hxy
  rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]
  on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)
  all_goals positivity

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

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
by
  simp [hz.not_gt, mul_rpow_eq_ite]

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

Goal state before:
pp: case inl
ε : ℝ
hε : 0 < ε
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ^ ε / ε

pp: case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε

Tactic:
· rw [log_zero, zero_rpow hε.ne', zero_div]

Goal state after:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y z : M
hy : SameRay R y z
hx : SameRay R 0 z
⊢ SameRay R (0 + y) z

pp: case inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z

Tactic:
· rwa [zero_add]

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
⊢ SameRay R (x + y) z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
rcases eq_or_ne c₁ 0 with hc₁ | hc₁

Goal state after:
case 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
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ = 0
⊢ SameRay R (c₁ • v) (c₂ • v)

case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
⊢ SameRay R (c₁ • v) (c₂ • v)
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) ↔ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

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

case neg.refine_2
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
h : ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
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
⊢ f.linear = 0 ↔ ∃ q, f = const k P1 q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
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
h : f.linear = 0
⊢ ∃ q, f = const k P1 q

case refine_2
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
h : ∃ q, f = const k P1 q
⊢ f.linear = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V1
inst✝⁵ : AffineSpace V1 P1
inst✝⁴ : AddCommGroup V2
inst✝³ : AffineSpace V2 P2
inst✝² : Module k V1
inst✝¹ : Module k V2
inst✝ : SMulCommClass k k V2
f g : P1 →ᵃ[k] P2
c : k
p : P1
⊢ ((lineMap f g) c) p = (lineMap (f p) (g p)) c

Tactic:
by
  simp [AffineMap.lineMap_apply]

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]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ {c}

Tactic:
intro z ⟨hzt, hzs⟩

Goal state after:
𝕜 : 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]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
⊢ z ∈ {c}
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
· exact Or.inr (ht hy ha hb hab)

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✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ s

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (z + x) + b • (fun x ↦ z + x) y' ∈ (fun x ↦ z + x) '' s

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x ↦ z + x) (a • x + b • y') = a • (z + x) + b • (fun x ↦ z + x) y'
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (x + z) + b • (fun x ↦ x + z) y' ∈ (fun x ↦ x + z) '' s

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x ↦ x + z) (a • x + b • y') = a • (x + z) + b • (fun x ↦ x + z) y'
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩
  intro h x hx y hy a b ha hb hab
  obtain rfl | hxy := eq_or_ne x y
  · rwa [Convex.combo_self hab]
  · exact h hx hy hxy ha hb hab

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

Goal state before:
pp: 𝕜 : 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
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab
  refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩
  rw [Convex.combo_affine_apply hab, hy'f]

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

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ a * x + b * y ∈ Ioc x y

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Goal state after:
case refine_2.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 * x + b * y ∈ Ioc x y

case refine_2.inr
𝕜 : 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
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Goal state after:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r

case inr
𝕜 : Type u_1
β : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 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 ∈ Ico 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

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Goal state after:
case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
hz : 0 * x + b * y ∈ Ico x y
⊢ ∃ a b_1, 0 < a ∧ 0 ≤ b_1 ∧ a + b_1 = 1 ∧ a * x + b_1 * y = 0 * x + b * y

case refine_1.inr
𝕜 : 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 ∈ Ico x y
ha' : 0 < a
⊢ ∃ 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:
← SetLike.mem_coe

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.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : vectorSpan k s ≤ s₁.direction
⊢ v ∈ s₁.direction

Tactic:
SetLike.le_def

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
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ s₁.direction