mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
s : Set X
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}

Tactic:
rw [coe_injective.compl_image_eq, compl_range_coe]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[instTopologicalSpace] (some '' s) ↔ IsOpen[inst✝] s

Tactic:
by
  rw [isOpen_iff_of_notMem infty_notMem_image_coe, preimage_image_eq _ coe_injective]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)

Tactic:
refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)),
    ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ i', (IsClosed[inst✝] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X),
    IsClosed[inst✝] i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : h = g
⊢ False

Tactic:
apply_fun fun e => (e y).down.1 at H

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : ↑((ConcreteCategory.hom h) y).down = ↑((ConcreteCategory.hom g) y).down
⊢ False
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)

Tactic:
rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

Tactic:
refine ⟨1 / δ, fun g hg ↦ ?_⟩

Goal state after:
case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ 1 / δ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁⁻¹ ⊤ + proximity f₂⁻¹ ⊤

Tactic:
by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
⊢ 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ

Tactic:
positivity

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
by_cases hR : R = 0
  · simp [hR, ValueDistribution.logCounting_eval_zero]
  convert circleIntegrable_circleAverage_log_norm_sub h |>.add
    (circleIntegrable_const (logCounting f ⊤ R) 0 1) |>.sub
    circleIntegrable_log_meromorphicTrailingCoeffAt
  simpa using eq_sub_of_add_eq
    (logCounting_add_log_trailingCoeff_eq_circleAverage_add_logCounting_top h hR _)

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2) (volume.restrict (uIoc 0 (2 * π) ×ˢ uIoc 0 (2 * π)))

Tactic:
Measure.volume_eq_prod,

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (uIoc 0 (2 * π) ×ˢ uIoc 0 (2 * π)))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) (volume.restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume

Tactic:
Measure.volume_eq_prod,

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) (volume.restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
Measure.volume_eq_prod,

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int : Integrable (fun p ↦ cartanKernel f R p.1 p.2) ((volume.prod volume).restrict (Ioc 0 (2 * π) ×ˢ Ioc 0 (2 * π)))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
have (d : E) : ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d := by
    simp_rw [this d]
    rcases eq_open_union_countable (fun f : 𝓕 ↦ U f d) (fun f ↦ U_open f.2 d) with ⟨t, t_count, ht⟩
    use (↑) '' t, image_val_subset, t_count.image _
    rw [← ht, biUnion_image]

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this✝ : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
this : ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
⊢ StrictMonoOn (logCounting (single e 1)) (Ioi ‖e‖)

Tactic:
intro a ha b hb hab
    rw [mem_Ioi] at ha hb
    rw [logCounting_single_eq_log_sub_const ha.le, logCounting_single_eq_log_sub_const hb.le]
    gcongr
    exact (norm_nonneg e).trans_lt ha

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
h : e = ⊤
⊢ 0 ≤ (divisor f univ)⁻

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
h : ¬e = ⊤
⊢ 0 ≤ (divisor (fun x ↦ f x - e.untop₀) univ)⁺

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise p' (map f l)
⊢ Triplewise p l

Tactic:
triplewise_map

Goal state after:
α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l
⊢ Triplewise p l
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons.refine_3
α : 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 k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ p tail[i] tail[j] tail[k]

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

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
cb : c ≤ b
⊢ (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}).Subsingleton

Tactic:
exact fun x hx y hy => hx.2.trans hy.2.symm

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha :
  (image (fun z ↦ ↑z) s').Nonempty →
    image (fun z ↦ ↑z) s' ≠ univ → #(image (fun z ↦ ↑z) s') < #((image (fun z ↦ ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)

Tactic:
image_nonempty,

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #(image (fun z ↦ ↑z) s') < #((image (fun z ↦ ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_1.cons.inl
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
head : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
    ∀ (a : P), head :: head :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head :: tail)
ha : ∀ (a : P), head :: head :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a]
ha' : head ∈ head :: tail
⊢ False

Tactic:
cases tail with

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

Goal state before:

Tactic:
0 < 1 := Nat.one_pos
      _ ≤ #(.biUnion {x} t) := ht {x}
      _ = (t x).card := by rw [Finset.singleton_biUnion]

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

Goal state before:
pp: case cons.refine_2.refine_1
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
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
ha' : head ∈ tail
⊢ False

Tactic:
cases tail with

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

Goal state before:
pp: case neg.refine_1
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ ∀ a ∈ 0 :: map (fun x ↦ r + (1 - r) * x) l'', 0 ≤ a

Tactic:
simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]

Goal state after:
case neg.refine_1
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ ∀ a ∈ l'', 0 ≤ r + (1 - r) * a
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
by
  refine ⟨fun h => ?_, fun h => h.map _⟩
  rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h

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

Goal state before:
pp: case neg
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
head : P
tail : List P
hl : head :: tail ≠ []
h : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
hl'' : map (⇑(lineMap (tail.head ht) (tail.getLast ht))) l'' = tail
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht))) l' = head :: tail

Tactic:
cases tail with

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
l : List P
h : List.Wbtw R l
hl : l = []
⊢ ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
exact ⟨AddTorsor.nonempty.some, AddTorsor.nonempty.some, [], by
        simp [hl, sortedLE_iff_pairwise]⟩

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

Goal state before:
pp: case inr.inl
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
x z : P
ht : 1 ∈ Set.Icc 0 1
hyx : (lineMap x z) 1 ≠ x
hyz : (lineMap x z) 1 ≠ z
⊢ False

Tactic:
exact hyz (lineMap_apply_one _ _)

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

Goal state before:
pp: case refine_2.refine_2.cons
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
l' : List R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail
⊢ tail = [] ∨ head ≠ (head :: tail).getLast hl

Tactic:
cases tail with

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

Goal state before:
pp: case refine_2.refine_2.cons
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
l' : List R
hl's : l'.SortedLE
head : P
tail : List P
hl : head :: tail ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hl'l : map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail
⊢ tail = [] ∨ head ≠ (head :: tail).getLast hl

Tactic:
cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp

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

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R x z y ↔ y = z

Tactic:
by
  rw [← wbtw_swap_right_iff R x, and_iff_right h]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a : α
h : (f a).isSome = true
⊢ f a = some ((f a).get h)

Tactic:
some_get

Goal state after:
α : Type u
β : Type v
f : α ≃. β
a : α
h : (f a).isSome = true
⊢ f a = f a
Module: Mathlib.Data.PEquiv

Goal state before:
pp: β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
⊢ f.trans (single b c) = ⊥

Tactic:
ext
  simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h
  dsimp [PEquiv.trans, single]
  simp only [bind_eq_some_iff, iff_false, not_exists, not_and, reduceCtorEq]
  intros
  split_ifs <;> simp_all

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

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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ p ∈ (s.face ⋯).interior ↔ Sbtw R (s.points i) p (s.points j)

Tactic:
rw [h', mem_interior_iff_sbtw, face_points, face_points]

Goal state after:
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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ Sbtw R (s.points (({i, j}.orderEmbOfFin ⋯) 0)) p (s.points (({i, j}.orderEmbOfFin ⋯) 1)) ↔
    Sbtw R (s.points (min i j)) p (s.points (max i j))
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = 1) ∧ ∀ (j : n), ∑ i, M i j = 1

Tactic:
simp [funext_iff, doublyStochastic, mulVec, vecMul, dotProduct]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
⊢ f i₀ / g i₀ * g e ≤ f e

pp: case neg
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∉ s
⊢ f i₀ / g i₀ * g e ≤ f e

Tactic:
· have hge : 0 < g e := by
        rw [mem_filter] at hes
        exact hes.2
      rw [← le_div_iff₀ hge]
      exact w _ hes

Goal state after:
case neg
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∉ s
⊢ f i₀ / g i₀ * g e ≤ f e
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ↑K
n : ℕ
⊢ 0 ≤ ↑(u n)

Tactic:
positivity

Goal state after: