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

Goal state before:
pp: case inl
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
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
have : ∀ x, f x = a := by simpa using hmem

Goal state after:
case inl
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
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
this : ∀ (x : X), f x = a
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
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
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hb : IsLUB (range ⇑f) (g y)
hmem : ∀ (x : X), f x ∈ Icc a (g y)
hle : a ≤ g y
hlt : a < g y
c : ℝ := (a + g y) / 2
hac : a < c
hcb : c < g y
hsub : c - a = g y - c
hgb : ∀ (y_1 : Y), g y_1 ≤ g y
hb' : ¬∃ x, f x = g y
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {g y})
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (g y - c)) (⇑g ⁻¹' {g y})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (g y - c)
⊢ (g - dg) y < g y

Tactic:
refine (sub_lt_self_iff _).2 ?_
      calc
        0 < g y - c := sub_pos.2 hcb
        _ = dg y := (dgb rfl).symm

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

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

Tactic:
rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
    sq_sqrt, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_mul_left] <;> positivity

Goal state after:
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]
  rw [← add_div, Complex.dist_self_conj, coe_im, abs_of_pos b.im_pos, mul_comm (dist (b : ℂ) _),
    dist_comm (b : ℂ), Complex.dist_conj_comm, mul_mul_mul_comm, mul_mul_mul_comm _ _ _ b.im]
  congr 2
  rw [sqrt_mul, sqrt_mul, sqrt_mul, mul_comm (√a.im), mul_mul_mul_comm, mul_self_sqrt,
      mul_comm] <;> exact (im_pos _).le

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d + 0

Tactic:
add_zero,

Goal state after:
case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d
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
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := fun x ↦ (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = Function.diag
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))

Tactic:
exact (proper_g.comp proper_f).isClosed_range

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

Goal state before:
pp: case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ ∃ u v,
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ↑val ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
| coe val =>

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ IsClosed[inst✝³] s

Tactic:
rw [CompactlyCoherentSpace.isClosed_iff]

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
⊢ IsCompact ((fun g ↦ g • I) ⁻¹' K)

Tactic:
refine this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop) (fun g hg ↦ ?_)

Goal state after:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
⊢ g ∈ Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
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) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
have : ∫ α, (cartanKernel f R α β)⁺ ∂(volume.restrict (Ioc 0 (2 * π))) ≤
        ∫ _, log⁺ ‖f (circleMap 0 R β)‖ + log 2 ∂(volume.restrict (Ioc 0 (2 * π))) := by
      refine integral_mono_of_nonneg (.of_forall (by simp [posPart])) (integrable_const _)
        (.of_forall ?_)
      intro α
      calc (cartanKernel f R α β)⁺
        _ = log⁺ ‖f (circleMap 0 R β) + (-circleMap 0 1 α)‖ := by
          simp [cartanKernel, posLog_def, posPart, max_comm, sub_eq_add_neg]
        _ ≤ log⁺ ‖f (circleMap 0 R β)‖ + log⁺ ‖-circleMap 0 1 α‖ + log 2 :=
          posLog_norm_add_le (f (circleMap 0 R β)) (-circleMap 0 1 α)
        _ = log⁺ ‖f (circleMap 0 R β)‖ + log 2 := by
          simp [norm_circleMap_zero, add_comm]

Goal state after:
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) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
this :
  ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ ∫ (x : ℝ) in Ioc 0 (2 * π), log⁺ ‖f (circleMap 0 R β)‖ + log 2
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l →
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
rintro h

Goal state after:
case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
⊢ locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f univ)⁻ =O[atTop] 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ

Tactic:
rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl
α : 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
⊢ eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}) = 0

Tactic:
eVariationOn.subsingleton

Goal state after:
case inl
α : 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
⊢ 0 = 0

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
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case 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
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.length = 1 ∨ l.head hl ≠ l.getLast hl
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')

Tactic:
rcases hla with hla | hla

Goal state after:
case refine_1.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
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.length = 1
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')

case refine_1.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
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
hla : l.head hl ≠ l.getLast hl
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (map (⇑(lineMap (l.head hl) (l.getLast hl))) l')
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this : ∀ (i : J'), Nonempty (F'.obj i)
⊢ F.sections.Nonempty

Tactic:
have : ∀ i, Finite (F'.obj i) := fun i => Finite.of_equiv (F.obj (down.obj i)) Equiv.ulift.symm

Goal state after:
J : Type u
inst✝³ : Category.{w, u} J
inst✝² : IsCofilteredOrEmpty J
F : J ⥤ Type v
inst✝¹ : ∀ (j : J), Finite (F.obj j)
inst✝ : ∀ (j : J), Nonempty (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this✝ : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
⊢ F.sections.Nonempty
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
⊢ F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ i f,
        ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))

Tactic:
by
  simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]

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
s : Simplex R P 1
p : P
⊢ p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)

Tactic:
closedInterior_eq_affineSegment,

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
s : Simplex R P 1
p : P
⊢ p ∈ affineSegment R (s.points 0) (s.points 1) ↔ Wbtw R (s.points 0) p (s.points 1)
Module: Mathlib.Data.PEquiv

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

Tactic:
rw [f.eq_some_iff, some_get]

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
⊢ ∃ x, ¬(if x ∈ f i then 1 else 0) = if x ∈ g i then 1 else 0

Tactic:
rcases hf : f i with - | fi

Goal state after:
case h.none
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
hf : f i = none
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ g i then 1 else 0

case h.some
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
fi : n
hf : f i = some fi
⊢ ∃ x, ¬(if x ∈ some fi then 1 else 0) = if x ∈ g i then 1 else 0
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✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
⊢ Sbtw R ((Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1))
    ((Finset.affineCombination R Finset.univ t.points) w)
    ((Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁))

Tactic:
refine
    Sbtw.affineCombination_of_mem_affineSpan_pair t.independent hw (Fintype.sum_pi_single' _ _)
      (Finset.univ.sum_affineCombinationLineMapWeights (Finset.mem_univ _) (Finset.mem_univ _) _)
      h₁' (Finset.mem_univ i₁) ?_

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
⊢ Sbtw R (Pi.single i₁ 1 i₁) (w i₁) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁ i₁)
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✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)
⊢ w i₁ ∈ Set.Ioo 0 1

Tactic:
have hss : SignType.sign (∑ i, w i) = 1 := by simp [hw]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Finset.univ = {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)
hss : SignType.sign (∑ i, w i) = 1
⊢ w i₁ ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case inl
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • ↑K

Tactic:
exact Set.mem_smul_set.mpr ⟨0, h_zero, smul_zero _⟩

Goal state after:
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.Ioi 1
⊢ Sbtw R x y z

Tactic:
· rcases h with ⟨hne, r, hr, rfl⟩
    rw [Set.mem_Ioi] at hr
    refine
      ⟨wbtw_iff_left_eq_or_right_mem_image_Ici.2
          (Or.inr (Set.mem_image_of_mem _ (Set.mem_of_mem_of_subset hr Set.Ioi_subset_Ici_self))),
        hne.symm, ?_⟩
    rw [lineMap_apply, ← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub]
    nth_rw 1 [← one_smul R (y -ᵥ x)]
    rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]
    exact ⟨hr.ne, hne.symm⟩

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsOrderedRing R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
p : M →ₗ[R] N →ₗ[R] R
M' : Type u_4
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
s : Set M'
q : M' →ₗ[R] M
⊢ dual p (⇑q '' s) = dual (p ∘ₗ q) s

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ dual p s = comap p.flip (dual (Module.Dual.eval R M) s)

Tactic:
by
  ext; simp

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

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
fg_min_on : IsMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}

Tactic:
simpa only [hg0, hg1, comp_apply, mem_ofPred_eq] using fg_min_on (right_mem_Icc.2 zero_le_one)

Goal state after: