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

Goal state before:
pp: z w : ℍ
⊢ tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_half_dist, cosh_half_dist, div_div_div_comm, div_self, div_one]

Goal state after:
z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Tactic:
simp only [add_div _ _ (2 : ℝ), sinh_add, sinh_half_dist, cosh_half_dist, div_mul_div_comm]

Goal state after:
a b c : ℍ
⊢ dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) +
      dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
by simpa only [sinh_zero] using @sinh_le_sinh x 0

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

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.center |log (z.im / w.im)|).im = w.im * |(z.im / w.im - (z.im / w.im)⁻¹) / 2|

pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re

Tactic:
center_im,

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * Real.cosh |log (z.im / w.im)|) = w.im * |(z.im / w.im - (z.im / w.im)⁻¹) / 2|

z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
intro hf x₁ x₂ h

Goal state after:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
⊢ x₁ = x₂
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ Continuous ⇑E.symm

Tactic:
continuous_iff_isClosed

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ ∀ (s : Set ((fun X ↦ ↑X.toTop) X)), IsClosed s → IsClosed (⇑E.symm ⁻¹' s)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u

Tactic:
eq_comm,

Goal state after:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ joinM u = x
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x✝ : TopologicalSpace α := ⊥
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)

Tactic:
exact isDenseInducing_pure.continuous_extend h

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange stoneCechUnit

Tactic:
unfold stoneCechUnit T2Quotient.mk
  have : Function.Surjective (T2Quotient.mk : PreStoneCech α → StoneCech α) := by
    exact Quot.mk_surjective
  exact this.denseRange.comp denseRange_preStoneCechUnit continuous_coinduced_rng

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

Goal state before:
pp: X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ y, ↑y = x

Tactic:
induction x using OnePoint.rec <;> simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
⊢ (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen[inst✝] (some ⁻¹' (s ∩ t))

Tactic:
refine ⟨?_, hs.inter ht⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
⊢ ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : IsTopologicalGroup G
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
let Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
    { toFun := fun gh ↦ (gh.2 * (unop gh.1), gh.2)
      invFun := fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2)
      left_inv := fun _ ↦ by simp
      right_inv := fun _ ↦ by simp }
    exact Φ.isProperMap

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense (range some)

Tactic:
← compl_infty

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | 0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : 0 < ↑(Matrix.GeneralLinearGroup.det h)
⊢ σ h = σ g

Tactic:
simp only [σ, hh, ↓reduceIte, hg]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
this : {h | ¬0 < ↑(Matrix.GeneralLinearGroup.det h)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : ¬0 < ↑(Matrix.GeneralLinearGroup.det h)
⊢ σ h = σ g

Tactic:
simp only [σ, hh, ↓reduceIte, hg]

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

Goal state before:
pp: f : ℂ → ℂ
n : ℕ
⊢ proximity (f ^ n) 0 = n • proximity f 0

Tactic:
rw [← proximity_inv, ← proximity_inv, ← inv_pow, proximity_pow_top]

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

Goal state before:
pp: 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 D) (Ioi ‖e‖)

Tactic:
(by aesop : logCounting D = logCounting (single e 1) + logCounting (D - single e 1))

Goal state after:
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) + logCounting (D - single e 1)) (Ioi ‖e‖)
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'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
by
  simp_rw [Sbtw, hf.wbtw_map_iff hx hy hz, hf.ne_iff hy hx, hf.ne_iff hy hz]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
⊢ sSup {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c} = s.domRestrict φ

Tactic:
by
  let A := { p : E × 𝕜 | p.1 ∈ s ∧ φ p.1 ≤ re p.2 }
  ext x
  rw [sSup_apply]
  refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ (fun r ⟨f, hf⟩ => ?_) (fun r hr => ?_)
  · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 (show φ x - 1 < φ x by grind)
      hsc hφc hφcv
    exact ⟨φ x - 1, hlc.2 ▸ ⟨⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩⟩
  · exact hf ▸ f.2.1 x
  · obtain ⟨z, hz⟩ := exists_between hr
    obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) x.2 hz.2 hsc hφc hφcv
    exact ⟨z, hlc.2 ▸ ⟨⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩, rfl⟩, hz.1⟩

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

Goal state before:
pp: case 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✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 • 1 ≤ a • 1

Tactic:
exact smul_le_smul_of_nonneg_right ha₀ zero_le_one

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

Goal state before:
pp: case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)

Tactic:
← Finset.card_image_of_injective s hf₁

Goal state after:
case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #(image f s) ≤ #(s.biUnion t)
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

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
x : n → R
hA : M ∈ colStochastic R n
⊢ ∑ i, ∑ x_1, M i x_1 * x x_1 = ∑ i, x i

Tactic:
Finset.sum_comm

Goal state after:
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
x : n → R
hA : M ∈ colStochastic R n
⊢ ∑ y, ∑ x_1, M x_1 y * x y = ∑ i, x i
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

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 : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
hM : M ∈ rowStochastic R n
⊢ (reindex e₁ e₂) M *ᵥ 1 = 1

Tactic:
by simp [submatrix_mulVec_equiv, hM.2]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j, M i j = s
hM₃ : ∀ (j : n), ∑ i, M i j = s
⊢ s⁻¹ • M ∈ doublyStochastic R n ∧ M = s • s⁻¹ • M

Tactic:
simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Injective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
Finite.injective_iff_bijective

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : |↑(u n)| * C < ε
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ |↑(u n)| * ‖y‖ < ε

Tactic:
refine lt_of_le_of_lt ?_ hn

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : |↑(u n)| * C < ε
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ |↑(u n)| * ‖y‖ ≤ |↑(u n)| * C
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := ⋯
hk : #(minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ (convexHull 𝕜) ↑((minCardFinsetOfMemConvexHull hx).erase ↑p)
contra : ¬#((minCardFinsetOfMemConvexHull hx).erase ↑p) < #(minCardFinsetOfMemConvexHull hx)
⊢ #((minCardFinsetOfMemConvexHull hx).erase ↑p) < #(minCardFinsetOfMemConvexHull hx)

Tactic:
card_erase_of_mem p.2,

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
k : ℕ := #(minCardFinsetOfMemConvexHull hx) - 1
hk : #(minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ (convexHull 𝕜) ↑((minCardFinsetOfMemConvexHull hx).erase ↑p)
contra : ¬#((minCardFinsetOfMemConvexHull hx).erase ↑p) < #(minCardFinsetOfMemConvexHull hx)
⊢ #(minCardFinsetOfMemConvexHull hx) - 1 < #(minCardFinsetOfMemConvexHull hx)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
h : x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1
⊢ Wbtw R x y z

Tactic:
rcases h with (rfl | ⟨r, ⟨hr, rfl⟩⟩)

Goal state after:
case refine_2.inl
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 z : P
⊢ Wbtw R x x z

case refine_2.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 : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) +ᵥ w = x
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x

Tactic:
eq_comm,

Goal state after:
case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w) +ᵥ w
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (lineMap w z) (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) = x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) • (z -ᵥ w) +ᵥ w = x

Tactic:
eq_comm,

Goal state after:
case refine_2
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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
hx : x -ᵥ w = t₁ • ((t₂ • (z -ᵥ x) +ᵥ x) -ᵥ w)
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_denom : 1 - t₁ + t₁ * t₂ ≠ 0
⊢ x = (t₁ * t₂ / (1 - t₁ + t₁ * t₂)) • (z -ᵥ w) +ᵥ w
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: case g2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
case g2 =>
    obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM
    exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3

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✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
h : ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at h

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
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
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
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ b ∈ map f C → ∀ (y : F), (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C → 0 ≤ ⟪b, y⟫_ℝ

Tactic:
simp only [map, ClosedSubmodule.map, Submodule.closure, Submodule.topologicalClosure,
      AddSubmonoid.topologicalClosure, Submodule.coe_toAddSubmonoid, Submodule.map_coe,
      ContinuousLinearMap.coe_coe,
      ContinuousLinearMap.coe_restrictScalars', ClosedSubmodule.coe_toSubmodule,
      ClosedSubmodule.mem_mk, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk,
      mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, Classical.skolem, forall_and,
      mem_innerDual, ContinuousLinearMap.adjoint_inner_right, forall_exists_index, and_imp]

Goal state after:
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
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ ∀ (x : ℕ → F) (x_1 : ℕ → E),
    (∀ (x : ℕ), x_1 x ∈ C) →
      (∀ (x_2 : ℕ), f (x_1 x_2) = x x_2) →
        Filter.Tendsto x Filter.atTop (nhds b) → ∀ (y : F), (∀ ⦃x : E⦄, x ∈ C → 0 ≤ ⟪f x, y⟫_ℝ) → 0 ≤ ⟪b, y⟫_ℝ
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case inl
𝕜 : 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✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∅ = {x | x ∈ A ∧ 1 ≤ 0 x}

Tactic:
eq_comm,

Goal state after:
case inl
𝕜 : 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✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ {x | x ∈ A ∧ 1 ≤ 0 x} = ∅
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl : {x} = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
eq_comm,

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x}
⊢ x ∈ exposedPoints 𝕜 A
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:

Tactic:
-|2 * f x₀| ≤ 2 * f x₀ := neg_abs_le _
    _ ≤ f y + f (2 • x₀ - y) := by
      have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
      simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
      cancel_denoms at this
      rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
    _ ≤ f y + |r| := by gcongr; exact hfr'.trans (le_abs_self _)

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E
hx₀b : x₀ ∈ interior ((convexHull ℝ) (Set.range ⇑b))
hbC : (convexHull ℝ) (Set.range ⇑b) ⊆ C
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
refine ⟨x₀, hx₀, BddAbove.isBoundedUnder (IsOpen.mem_nhds isOpen_interior hx₀b) ?_⟩

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E
hx₀b : x₀ ∈ interior ((convexHull ℝ) (Set.range ⇑b))
hbC : (convexHull ℝ) (Set.range ⇑b) ⊆ C
⊢ BddAbove (f '' interior ((convexHull ℝ) (Set.range ⇑b)))