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

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ rexp (2 * ↑π * Complex.I * ξ).re ≤ rexp (-π)

Tactic:
Real.exp_le_exp,

Goal state after:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ (2 * ↑π * Complex.I * ξ).re ≤ -π
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h₂f
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
peel f_bound with z hz _

Goal state after:
case h₂f.h.h
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
⊢ Real.log ‖f z‖ ≤ Real.log M
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ (GeneralLinearGroup.scalar n).range ≤ f.ker

Tactic:
MonoidHom.range_le_ker_iff

Goal state after:
n : Type u_1
R : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
M : Type u_3
inst✝ : Monoid M
f : GL n R →* M
hf : f.comp (GeneralLinearGroup.scalar n) = 1
⊢ f.comp (GeneralLinearGroup.scalar n) = 1
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
⊢ 0 ≤ Real.log (R * ‖c - u‖⁻¹)

Tactic:
apply log_abs _ ▸ log_nonneg

Goal state after:
case neg
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
⊢ 1 ≤ |R * ‖c - u‖⁻¹|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr

Tactic:
← Complex.ofReal_mul,

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑(√(↑g).discr * √(↑g).discr)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: w : ℂ
⊢ ↑ofComplex w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯

Tactic:
split_ifs with hw
  · exact ofComplex_apply ⟨w, hw⟩
  · change (Function.invFunOn UpperHalfPlane.coe Set.univ w) = _
    simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]
    rintro ⟨a, rfl⟩
    exact (a.im_pos.not_ge (by simpa using hw)).elim

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: this : Continuous fun t ↦ Complex.I * ↑t
⊢ Continuous
    (UpperHalfPlane.coe ∘
      (Ioi 0).domRestrict fun t ↦
        if hw : 0 < (↑I * ↑t).im then { coe := ↑I * ↑t, coe_im_pos := hw } else Classical.choice ⋯)

Tactic:
exact (this.comp continuous_subtype_val).congr (by simp +contextual)

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
have hcb : c < b := add_div_two_lt_right.2 hlt

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
this : ↑√z.im ≠ 0
⊢ (↑z.re + ↑√z.im * ↑√z.im * Complex.I) / ↑√z.im = ↑z * (↑√z.im)⁻¹

Tactic:
← Complex.ofReal_mul,

Goal state after:
z : ℍ
this : ↑√z.im ≠ 0
⊢ (↑z.re + ↑(√z.im * √z.im) * Complex.I) / ↑√z.im = ↑z * (↑√z.im)⁻¹
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0

Tactic:
rw [mdifferentiable_iff] at hf
  have := hf.analyticOnNhd isOpen_upperHalfPlaneSet
  ext w
  convert! this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos
  · rw [Function.comp_apply, ofComplex_apply]
  · exact (Complex.isConnected_of_upperHalfPlane subset_rfl (by grind)).isPreconnected
  · contrapose! hτ
    rw [eventually_nhdsWithin_iff, ← isOpenEmbedding_coe.map_nhds_eq, eventually_map] at hτ
    rw [eventually_nhdsWithin_iff]
    filter_upwards [hτ] with a ha
    simpa using ha

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 =
    1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

Tactic:
add_assoc,

Goal state after:
z w : ℍ
⊢ 1 + (sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2 + sinh (arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))) ^ 2) =
    1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
by
  simp only [cosh, div_eq_mul_inv]
  convert!
    ((hasStrictDerivAt_exp x).sub (hasStrictDerivAt_id x).fun_neg.cexp).mul_const (2 : ℂ)⁻¹ using 1
  rw [id, mul_neg_one, sub_eq_add_neg, neg_neg]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ rexp (log z.im) / rexp (log w.im) ≤ rexp (dist z w)

Tactic:
← Real.exp_sub,

Goal state after:
z w : ℍ
⊢ rexp (log z.im - log w.im) ≤ rexp (dist z w)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, Units.instTopologicalSpaceUnits] ⇑upperRightHom

Tactic:
simp only [continuous_induced_rng, Function.comp_def, upperRightHom_apply,
    Units.embedProduct_apply, Units.inv_mk, continuous_prodMk, MulOpposite.unop_op]
  constructor <;>
  · refine continuous_matrix fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)

Tactic:
refine le_trans ?_ (le_trans (map_mono t) this)

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map (Ultrafilter.extend f) ↑b'
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: P : TopCat → Prop
⊢ ∀ (X : CompHausLike P), P X.toTop → True

Tactic:
simp only [implies_true]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: case ht
G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := ⋯
V : Set X := ⋯
hU : IsCompact U
hV : IsCompact V
⊢ IsClosed ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

Tactic:
exact (hU.prod hV).isClosed.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case funProp.discharger
g : SL(2, ℝ)
τ : ℍ
⊢ ↑(↑(g, τ).1 1 0) * ↑(g, τ).2 + ↑(↑(g, τ).1 1 1) ≠ 0

Tactic:
exact denom_ne_zero g τ

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ ∀ x ∈ sphere 0 |r|, log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
· intro x hx
        rw [add_comm]
        apply posLog_norm_sum_le

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt (fun x ↦ -a) 0 < meromorphicOrderAt f 0

Tactic:
meromorphicOrderAt_const

Goal state after:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
⊢ IntegrableOn (fun x ↦ cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
apply (intervalIntegrable_iff_integrableOn_Ioc_of_le two_pi_pos.le).1
  simpa [cartanKernel, norm_sub_rev, CircleIntegrable] using circleIntegrable_log_norm_sub_const 1

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0

Tactic:
meromorphicOrderAt_const

Goal state after:
case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0

Tactic:
meromorphicOrderAt_const

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (α : ℝ) (β : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β

Tactic:
MeasureTheory.intervalIntegral_intervalIntegral_swap

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (y : ℝ) (x : ℝ) in 0..2 * π, F x y =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β

f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ IntegrableOn (Function.uncurry F) (uIoc 0 (2 * π) ×ˢ uIoc 0 (2 * π)) volume
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:

Tactic:
(2 * π)⁻¹ * ∫ α in 0..2 * π, F α β
        _ = circleAverage (log ‖f (circleMap 0 R β) - ·‖) 0 1 := by
          simp [F, circleAverage, Cartan.cartanKernel]
        _ = log⁺ ‖f (circleMap 0 R β)‖ := by
          simp [norm_sub_rev]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|

Tactic:
have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ∃ b_1, b ≤ b_1 ∧ 1 < a * |logCounting D b_1|
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
a✝ : α
l✝ : List α
head : Pairwise (p a✝) l✝
tail : Triplewise p l✝
ih : Triplewise q l✝
⊢ Triplewise q (a✝ :: l✝)

Tactic:
exact .cons (head.imp h) ih

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons.refine_2
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ p head tail[i] tail[j]

Tactic:
simpa using! h 0 (i + 1) (j + 1) (by lia) (by lia) (by lia)

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
p₁ p₂ p₃ : P
⊢ List.Sbtw R [p₁, p₂, p₃] ↔ Sbtw R p₁ p₂ p₃

Tactic:
by
  simp only [List.Sbtw, wbtw_triple, ne_eq, pairwise_cons, mem_cons, not_mem_nil, or_false,
    forall_eq_or_imp, forall_eq, IsEmpty.forall_iff, implies_true, Pairwise.nil, and_self, and_true]
  exact ⟨fun ⟨hw, ⟨h₁₂, h₁₃⟩, h₂₃⟩ ↦ ⟨hw, Ne.symm h₁₂, h₂₃⟩,
         fun h ↦ ⟨h.1, ⟨h.2.1.symm, h.left_ne_right⟩, h.2.2⟩⟩

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y z : V
⊢ Sbtw R (-x) (-y) (-z) ↔ Sbtw R x y z

Tactic:
by
  simp only [← zero_sub, sbtw_const_sub_iff]

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

Goal state before:
pp: case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : Nontrivial P
p₁ : P
h : List.Sbtw R [p₁]
hl : ¬[p₁] = []
p₂ : P
hp₂p₁ : p₂ ≠ p₁
⊢ ∃ p₁_1 p₂, p₁_1 ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁_1 p₂)) l' = [p₁]

Tactic:
exact ⟨p₁, p₂, hp₂p₁.symm, [0], by simp [sortedLT_iff_pairwise]⟩

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x✝ : α
⊢ (∃ a ∈ s, f a = x✝) → ∃ a ∈ s, x✝ ∈ t a

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
x : ι
hx : x ∈ s
⊢ ∃ a ∈ s, f x ∈ t a
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
a : α
b : β
h : g a = some b
⊢ f a = some b

Tactic:
· exact gf _ _ h

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : AddCommMonoidWithOne R
⊢ (Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard

Tactic:
delta trace
  simp [toPEquiv_apply, ← Set.ncard_coe_finset, Function.fixedPoints, Function.IsFixedPt]

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑K → 0 ≤ ⟪b, y⟫_ℝ
⊢ b ∈ map f K

Tactic:
rwa [K.relative_hyperplane_separation]

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

Goal state before:
pp: case inr.inr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
this : ∀ {y z : P} (r₁ r₂ : R), 0 < r₁ → 0 < r₂ → r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x) → r₂ ≤ r₁ → Wbtw R x y z ∨ Wbtw R x z y
hr : ¬r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y

pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
· rw [or_comm]
    apply this r₂ r₁ hr₂ hr₁ h.symm (Std.le_of_not_ge hr)

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
hr : r₂ ≤ r₁
⊢ Wbtw R x y z ∨ Wbtw R x z y
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : ProperCone ℝ F
C₂ : PointedCone ℝ E
h₂_simp : C₂.IsSimplicial
h₂_gen : Submodule.span ℝ ↑C₂ = ⊤
⊢ map (↑(TensorProduct.comm ℝ E F)) (C₂.minTensorProduct ↑C₁) =
    map (↑(TensorProduct.comm ℝ E F)) (C₂.maxTensorProduct ↑C₁)

Tactic:
minTensorProduct_eq_max_of_simplicial_generating_left C₂ C₁ h₂_simp h₂_gen

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : ProperCone ℝ F
C₂ : PointedCone ℝ E
h₂_simp : C₂.IsSimplicial
h₂_gen : Submodule.span ℝ ↑C₂ = ⊤
⊢ map (↑(TensorProduct.comm ℝ E F)) (C₂.maxTensorProduct ↑C₁) =
    map (↑(TensorProduct.comm ℝ E F)) (C₂.maxTensorProduct ↑C₁)
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a = f a

Tactic:
rw [← add_smul, yac, one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
⊢ IsExposed 𝕜 A (B ∩ C)

Tactic:
rintro ⟨w, hwB, hwC⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
w : E
hwB : w ∈ B
hwC : w ∈ C
⊢ ∃ l, B ∩ C = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ ⋃ x, ⋃ i, ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y = ⋃ i, ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y

Tactic:
exact iUnion_comm _

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure ((convexHull ℝ) (extremePoints ℝ s)) = s

Tactic:
by
  apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
  by_contra hs
  obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
  obtain ⟨l, r, hlr, hrx⟩ :=
    geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
  have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
  obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn
  obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩
  linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
    h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(StdSimplex.duple x y ha hb hab).weights.support ⊆ s

Tactic:
StdSimplex.weights_duple,

Goal state after:
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ↑(single x a + single y b).support ⊆ s