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

Goal state before:
pp: case refine_1
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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (range e) (⇑g ⁻¹' {a})

pp: case refine_2
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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (Ici c) {a}

Tactic:
· rw [Set.disjoint_left]
        rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)
        exact ha' ⟨x, (congr_fun hgf x).symm⟩

Goal state after:
case refine_2
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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (Ici c) {a}
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ Disjoint (Ici c) {a}

Tactic:
· exact Set.disjoint_singleton_right.2 hac.not_ge

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
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f

Tactic:
rcases exists_bounded_mem_Icc_of_closed_of_le
        (he.isClosed_range.union <| isClosed_Ici.preimage g.continuous)
        (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hac.le) with
      ⟨dg, dg0, dga, dgmem⟩

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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (((evalRingHom 0).mapMatrix.comp ((↑(compRingEquiv m n R[X])).comp f.polyToMatrix.mapMatrix)) (cornerAddX M k)).det =
    (((↑(compRingEquiv m n R)).comp f.mapMatrix) M).det

Tactic:
← RingHom.comp_assoc,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((((evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X])).comp f.polyToMatrix.mapMatrix) (cornerAddX M k)).det =
    (((↑(compRingEquiv m n R)).comp f.mapMatrix) M).det
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
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
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
⊢ Disjoint (range e) (⇑g ⁻¹' {b})

Tactic:
rw [Set.disjoint_left]
      rintro _ ⟨x, rfl⟩ (rfl : g (e x) = b)
      exact hb' ⟨x, (congr_fun hgf x).symm⟩

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

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist x c * (R * R / (dist x c * dist x c) * dist x c) = R * R

Tactic:
field

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
⊢ z.im - w.im * ((z.im / w.im + w.im / z.im) / 2) = w.im * ((z.im / w.im - w.im / z.im) / 2)

Tactic:
field

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

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

Tactic:
rw [← div_le_iff₀' w.im_pos, ← exp_log z.im_pos, ← exp_log w.im_pos, ← Real.exp_sub, exp_le_exp]
  exact (le_abs_self _).trans (dist_log_im_le z w)

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

Goal state before:
pp: case refine_2
z✝ w✝ : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
⊢ z.im * (rexp (dist w z) - 1) < R

Tactic:
rwa [← lt_div_iff₀' z.im_pos, sub_lt_iff_lt_add, ← Real.lt_log_iff_exp_lt h₀]

Goal state after:
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)
⊢ IsIso f

Tactic:
let E := Equiv.ofBijective _ bij

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
⊢ IsIso f
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A : CompHausLike P
⊢ ∀ {B : CompHausLike P} (f : A ⟶ B) [IsIso ((forget (CompHausLike P)).map f)], IsIso f

Tactic:
B

Goal state after:
P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
⊢ ∀ (f : A ⟶ B) [IsIso ((forget (CompHausLike P)).map f)], IsIso f
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
x✝¹ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x✝ : X × X
x₁ x₂ : X
hxx : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰) (𝓝 g)
⊢ ((g, x₂).1 • (g, x₂).2, (g, x₂).2) = (x₁, x₂)

Tactic:
simp_rw [hg1]

Goal state after:
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✝ : ProperSMul G X
⊢ T2Space (Quotient (MulAction.orbitRel G X))

Tactic:
by
  rw [t2_iff_isClosed_diagonal]
  set R := MulAction.orbitRel G X
  let π : X → Quotient R := Quotient.mk'
  have : IsOpenQuotientMap (Prod.map π π) :=
    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
  rw [← this.isQuotientMap.isClosed_preimage]
  convert! ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range
  · ext ⟨x₁, x₂⟩
    simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,
      exists_eq_right]
    rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]
  all_goals infer_instance

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

Goal state before:
pp: X : Type w
Y : Type x
inst✝ : TopologicalSpace X
t : TopologicalSpace Y
f : X → Y
h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous[_, t] (f ∘ ⇑g)
⊢ Continuous[compactlyGenerated X, t] f

Tactic:
by
  rw [continuous_coinduced_dom]
  continuity

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

Goal state before:
pp: ⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
simp only [continuous_induced_rng, Function.comp_def, coe_smul, continuous_iff_continuousAt,
    Prod.forall]

Goal state after:
⊢ ∀ (a : GL (Fin 2) ℝ) (b : ℍ), ContinuousAt (fun x ↦ (σ x.1) (num x.1 ↑x.2 / denom x.1 ↑x.2)) (a, b)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioc 0 (2 * π)
⊢ (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, Cartan.cartanKernel f R x✝¹ β =
    circleAverage (fun x ↦ log ‖f x - circleMap 0 1 x✝¹‖) 0 R

Tactic:
by simp [circleAverage, Cartan.cartanKernel]

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
⊢ eVariationOn f (s ∩ Icc z y) = ENNReal.ofReal (↑l * (y - z))

Tactic:
hfs zs ys zy

Goal state after:
case inl.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
⊢ ENNReal.ofReal (↑l * (y - z)) = ENNReal.ofReal (↑l * (y - z))
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
a : WithTop E
⊢ logCounting f a 0 = 0

Tactic:
by
  by_cases h : a = ⊤ <;> simp [logCounting, h]

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
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs : (∀ a ∈ s, Meromorphic (f a)) → logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting (f a) ⊤ r ≤ logCounting (f a) ⊤ r

Tactic:
trivial

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A : FiniteDiagram J
⊢ ∀ (y : FiniteDiagram J),
    ∃ z,
      (fun G ↦ partialSections F G.snd) A ⊇ (fun G ↦ partialSections F G.snd) z ∧
        (fun G ↦ partialSections F G.snd) y ⊇ (fun G ↦ partialSections F G.snd) z

Tactic:
B

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
⊢ ∃ z,
    (fun G ↦ partialSections F G.snd) A ⊇ (fun G ↦ partialSections F G.snd) z ∧
      (fun G ↦ partialSections F G.snd) B ⊇ (fun G ↦ partialSections F G.snd) z
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
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : (s.weightedVSub p) (w₁ - w₂) = 0
⊢ ∑ i ∈ s, (w₁ - w₂) i = 0

Tactic:
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
⊢ (∀ (A : Finset α), #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
have := Classical.decEq β
  let r' a : Finset β := {b | r a b}
  have h : ∀ A : Finset α, ({b | ∃ a ∈ A, r a b} : Finset _) = A.biUnion r' := by
    intro A
    ext b
    simp [r']
  have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']
  simp_rw [h, h']
  apply Finset.all_card_le_biUnion_card_iff_exists_injective

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

Goal state before:
pp: case h.none.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
hf : f i = none
gi : n
hg : g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0

Tactic:
· use gi
      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✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (z -ᵥ x) (z -ᵥ y)

Tactic:
rcases h with ⟨t, ⟨_, ht1⟩, rfl⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
left✝ : 0 ≤ t
ht1 : t ≤ 1
⊢ SameRay R (z -ᵥ x) (z -ᵥ (lineMap x z) t)
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₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h₂₃ : i₂ ≠ i₃ := by
    rintro rfl
    simp at h₁

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₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁
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
hM : M ∈ rowStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ M j k * x k

Tactic:
refine Left.mul_nonneg ?_ (hx k)

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
hM : M ∈ rowStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ M j k
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
hM : M ∈ colStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ M j k * x k

Tactic:
refine Left.mul_nonneg ?_ (hx k)

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
hM : M ∈ colStochastic R n
hx : ∀ (i : n), 0 ≤ x i
j k : n
a✝ : k ∈ univ
⊢ 0 ≤ M j k
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case refine_2
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
⊢ x ∈ ⋂ n, (1 + ↑(u n)) • ↑K

Tactic:
refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)

Goal state after:
case refine_2
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 : ℕ
⊢ 1 ≤ 1 + ↑(u n)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
let r := (y - x) / (z - x)

Goal state after:
case inr
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z
Module: Mathlib.Analysis.Convex.Between

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

Tactic:
exact wbtw_self_left _ _ _

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
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
⊢ (1 - t₁) • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)

Tactic:
sub_smul,

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
⊢ 1 • (x -ᵥ w) - t₁ • (x -ᵥ w) + (t₁ * t₂) • (x -ᵥ w) = (t₁ * t₂) • (z -ᵥ w)
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₂) • (z -ᵥ x + (x -ᵥ w)) = (t₁ • t₂) • (z -ᵥ w)

Tactic:
vsub_add_vsub_cancel

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
⊢ (t₁ • t₂) • (z -ᵥ w) = (t₁ • t₂) • (z -ᵥ w)
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
w x y z : P
h₁ : Wbtw R w x y
h₂ : Wbtw R x y z
h_ne : x ≠ y
⊢ Wbtw R w x z

Tactic:
by
  rcases h₁ with ⟨t₁, ht₁, hx⟩
  rcases h₂ with ⟨t₂, ht₂, hy⟩
  refine ⟨t₁ * t₂ / (1 - t₁ + t₁ * t₂), ?_, ?_⟩
  · constructor
    · apply div_nonneg (mul_nonneg ht₁.1 ht₂.1)
      nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
    · apply div_le_one_of_le₀
      · grind
      · nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
  have h_denom : 1 - t₁ + t₁ * t₂ ≠ 0 := by
    contrapose h_ne
    have h1 : t₁ = 1 := by nlinarith [ht₁.1, ht₁.2, ht₂.1, ht₂.2]
    rw [← hx, h1, lineMap_apply_one]
  rw [← hy, lineMap_apply, lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq] at hx
  rw [lineMap_apply, eq_comm, eq_vadd_iff_vsub_eq, div_eq_mul_inv, mul_comm, mul_smul,
    eq_inv_smul_iff₀ h_denom, add_smul, sub_smul, one_smul]
  nth_rw 1 [hx]
  rw [← smul_sub, mul_smul, mul_smul, vsub_sub_vsub_cancel_right, vadd_vsub, ← smul_assoc,
    ← smul_assoc, ← smul_assoc, ← smul_add, vsub_add_vsub_cancel]

Goal state after: