mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H ?h.mY))) ⋯.some =
    (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hY))) ⋯.some

pp: case h.mY
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ Y ∈ G

pp: case h.mf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ ⟨X, ⟨Y, ⟨hX, ⟨?h.mY, f⟩⟩⟩⟩ ∈ H

Tactic:
]

Goal state after:
case h.mf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp
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
⊢ Wbtw R x y z ∧ Wbtw R y x z → x = y

pp: case mpr
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
⊢ x = y → Wbtw R x y z ∧ Wbtw R y x z

Tactic:
· rintro ⟨hxyz, hyxz⟩
    rcases hxyz with ⟨ty, hty, rfl⟩
    rcases hyxz with ⟨tx, htx, hx⟩
    rw [lineMap_apply, lineMap_apply, ← add_vadd] at hx
    rw [← @vsub_eq_zero_iff_eq V, vadd_vsub, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul, ← sub_smul,
      ← add_smul, smul_eq_zero] at hx
    rcases hx with (h | h)
    · nth_rw 1 [← mul_one tx] at h
      rw [← mul_sub, add_eq_zero_iff_neg_eq] at h
      have h' : ty = 0 := by
        refine le_antisymm ?_ hty.1
        rw [← h, Left.neg_nonpos_iff]
        exact mul_nonneg htx.1 (sub_nonneg.2 hty.2)
      simp [h']
    · rw [vsub_eq_zero_iff_eq] at h
      rw [h, lineMap_same_apply]

Goal state after:
case mpr
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
⊢ x = y → Wbtw R x y z ∧ Wbtw R y x 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
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ z = y

Tactic:
]

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

Tactic:
]

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 y x z ↔ Wbtw R y x z

Tactic:
]

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 ↔ Wbtw R x z y

Tactic:
]

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 z x y ↔ Wbtw R z x y

Tactic:
]

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

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

Tactic:
]

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Function.Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #(image f s) ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Hall.Finite

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

Tactic:
]

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

Goal state before:
pp: case pos
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 : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1

Tactic:
]

Goal state after:
case pos
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 : P
r : R
hxy : x = y
⊢ Wbtw R y y y ↔ y = y ∨ r ∈ Set.Icc 0 1
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ∃ a ∈ A.snd, ιA a = ιA f

Tactic:
]

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow A.fst
hf : f ∈ A.snd
⊢ ∃ a ∈ A.snd, ιA a = ιA f
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case neg
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 : P
r : R
hxy : ¬x = y
⊢ r ∈ Set.Icc 0 1 ↔ r ∈ Set.Icc 0 1

Tactic:
]

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 : P
r : R
⊢ x ≠ y ∧ ?m.59 ↔ x ≠ y ∧ r ∈ Set.Ioo 0 1

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 : P
r : R
⊢ x ≠ y → ((lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ ?m.59)

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 : P
r : R
⊢ Prop

Tactic:
]

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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y : P
r : R
⊢ x ≠ y → ((lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1)
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 : P
r : R
hxy : x ≠ y
⊢ r ∈ Set.Ioo 0 1 ↔ r ∈ Set.Ioo 0 1

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' range ⇑(ConcreteCategory.hom (F.map g))

Tactic:
]

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
⊢ F.eventualRange i ⊆ ⇑(ConcreteCategory.hom (F.map f)) '' range ⇑(ConcreteCategory.hom (F.map g))
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
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
]

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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y 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
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w

Tactic:
]

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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
x : F.obj k
hx : (ConcreteCategory.hom (F.map (g ≫ f))) x ∈ F.eventualRange i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) =
    (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x)

Tactic:
]

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
ι : 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
h : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
]

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✝³ : 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
h : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)
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₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
]

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✝³ : 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₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a ∈ B.snd, ιB a = ιB f

Tactic:
]

Goal state after:
J : Type u
inst✝ : SmallCategory J
F : J ⥤ TopCat
A B : FiniteDiagram J
ιA : FiniteDiagramArrow A.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
ιB : FiniteDiagramArrow B.fst → FiniteDiagramArrow (A.fst ⊔ B.fst) :=
  fun f ↦ ⟨f.fst, ⟨f.snd.fst, ⟨⋯, ⟨⋯, f.snd.snd.snd.snd⟩⟩⟩⟩
u : (j : J) → ↑(F.obj j)
hu : u ∈ (fun G ↦ partialSections F G.snd) ⟨A.fst ⊔ B.fst, Finset.image ιA A.snd ⊔ Finset.image ιB B.snd⟩
f : FiniteDiagramArrow B.fst
hf : f ∈ B.snd
⊢ ∃ a ∈ B.snd, ιB a = ιB f
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range (⇑(ConcreteCategory.hom (F.map g)) ∘ ⇑(ConcreteCategory.hom (F.map f))) ⊆
    range ⇑(ConcreteCategory.hom (F.map g))

Tactic:
]

Goal state after:
case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range (⇑(ConcreteCategory.hom (F.map g)) ∘ ⇑(ConcreteCategory.hom (F.map f))) ⊆
    range ⇑(ConcreteCategory.hom (F.map g))
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
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) (r • (w₂ - w₁) + w₁))
    ((Finset.affineCombination R s p) w₂)

Tactic:
]

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✝³ : 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
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) (r • (w₂ - w₁) + w₁))
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
j k : J
g : k ⟶ j
⊢ univ ⊆ univ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
⊢ ∀ (i_1 : Y✝ ⟶ i), (ConcreteCategory.hom (F.map g)) x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s

Tactic:
]

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
⊢ ∀ (i_1 : Y✝ ⟶ i), (ConcreteCategory.hom (F.map g)) x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst})

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
⊢ IsClosed (⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst})
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s

Tactic:
]

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map g ≫ F.map f)) ⁻¹' s

Tactic:
]

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s ↔
    x ∈ ⇑(ConcreteCategory.hom (F.map g ≫ F.map f)) ⁻¹' s
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), (ConcreteCategory.hom (F.map f)) x ∈ range ⇑(ConcreteCategory.hom (F.map f_1))

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), (ConcreteCategory.hom (F.map f)) x ∈ range ⇑(ConcreteCategory.hom (F.map f_1))
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
⊢ (s.weightedVSub p) (w₁ - w₂) ≠ 0

Tactic:
]

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✝³ : 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
⊢ (s.weightedVSub p) (w₁ - w₂) ≠ 0
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), (ConcreteCategory.hom (F.map g)) x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ (ConcreteCategory.hom (F.map g' ≫ F.map f')) x ∈ range ⇑(ConcreteCategory.hom (F.map f'))

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), (ConcreteCategory.hom (F.map g)) x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ (ConcreteCategory.hom (F.map g' ≫ F.map f')) x ∈ range ⇑(ConcreteCategory.hom (F.map f'))