mathlib-initiative/mathlib-tactics huggingface dataset:
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 : i ⟶ j
⊢ (∀ (i_1 : J) (j_1 : i_1 ⟶ j), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map j_1))) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ 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 : i ⟶ j
⊢ (∀ (i_1 : J) (j_1 : i_1 ⟶ j), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map j_1))) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
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 : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range (⇑(ConcreteCategory.hom (F.map f')) ∘ ⇑(ConcreteCategory.hom (F.map g'))) ⊆
    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 : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range (⇑(ConcreteCategory.hom (F.map f')) ∘ ⇑(ConcreteCategory.hom (F.map g'))) ⊆
    range ⇑(ConcreteCategory.hom (F.map f'))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case e'_4
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ι' : Finset ι
s' : Finset ↥ι'
⊢ #(s'.biUnion fun i ↦ t ↑i) = #(s'.biUnion fun a ↦ t ↑a)

Tactic:
]

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}

Tactic:
]

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑{f | Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : ↥ι'
⊢ ∃ a ∈ ι', ↑f i ∈ t a

Tactic:
]

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : ↥ι'
⊢ ∃ a ∈ ι', ↑f i ∈ t a
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : ∀ (x : ↥ι'), g f x = g f' x
a : ↥ι'
⊢ ↑f a = ↑f' a

Tactic:
]

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : ∀ (x : ↥ι'), g f x = g f' x
a : ↥ι'
⊢ ↑f a = ↑f' a
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
hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0
ha' : w₁ i = w₂ i
⊢ w₁ i = w₂ i

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
hz : (s.weightedVSub p) (w₁ - w₂) = 0
hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0
ha' : w₁ i = w₂ i
⊢ w₁ i = w₂ i
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
⊢ (ConcreteCategory.hom (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
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
⊢ (ConcreteCategory.hom (F.map f₂)) x ∈ range ⇑(ConcreteCategory.hom (F.map f₂))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ({ obj := fun ι' ↦ ↑(hallMatchingsOn t (Opposite.unop ι')), map := fun {x x_1} g ↦ ↾hallMatchingsOn.restrict t ⋯,
          map_id := ⋯, map_comp := ⋯ }.obj
      ι')

Tactic:
]

Goal state after:
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
ι' : (Finset ι)ᵒᵖ
⊢ Finite
    ({ obj := fun ι' ↦ ↑(hallMatchingsOn t (Opposite.unop ι')), map := fun {x x_1} g ↦ ↾hallMatchingsOn.restrict t ⋯,
          map_id := ⋯, map_comp := ⋯ }.obj
      ι')
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
w : Fin (1 + 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)

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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : w 0 + w 1 = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ (lineMap (s.points 0) (s.points 1)) (w 1) ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
]

Goal state after:
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ (lineMap (s.points 0) (s.points 1)) (w 1) ∈ affineSegment R (s.points 0) (s.points 1)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ ∀ (i : Fin (1 + 1)), Finset.affineCombinationLineMapWeights 0 1 r i ∈ Set.Icc 0 1

Tactic:
]

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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 ≤ r
h1 : r ≤ 1
⊢ ∀ (i : Fin (1 + 1)), Finset.affineCombinationLineMapWeights 0 1 r i ∈ Set.Icc 0 1
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map f₄)) y ∈ ⇑(ConcreteCategory.hom (F.map g₂)) ⁻¹' s

Tactic:
]

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map f₄)) y ∈ ⇑(ConcreteCategory.hom (F.map g₂)) ⁻¹' s
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ (⨆ a, ↑a ∘ ⇑(Equiv.Set.univ E).symm) x = ((⨆ a, ↑a) ∘ ⇑(Equiv.Set.univ E).symm) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : 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
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
x : E
⊢ (⨆ a, ↑a ∘ ⇑(Equiv.Set.univ E).symm) x = ((⨆ a, ↑a) ∘ ⇑(Equiv.Set.univ E).symm) x
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 ∈ affineSegment R (s.points 0) (s.points 1) ↔ p ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
]

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

Goal state before:
pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi).op)) (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi').op)) (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'

Tactic:
]

Goal state after:
case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
i i' : ι
subi : {i} ⊆ {i, i'}
subi' : {i'} ⊆ {i, i'}
⊢ ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi).op)) (u (Opposite.op {i, i'}))) ⟨i, ⋯⟩ =
      ↑((ConcreteCategory.hom ((hallMatchingsFunctor t).map (homOfLE subi').op)) (u (Opposite.op {i, i'}))) ⟨i', ⋯⟩ →
    i = i'
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr
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
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))

Tactic:
]

Goal state after:
case inr
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
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
hji : j < i
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (max i j)) (s.points (min i j))
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 ι
⊢ #(image f s) ≤ #(s.biUnion t)

Tactic:
]

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.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) ↔ ∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
by
  constructor
  · intro h
    -- Set up the functor
    have : ∀ ι' : (Finset ι)ᵒᵖ, Nonempty ((hallMatchingsFunctor t).obj ι') := fun ι' =>
      hallMatchingsOn.nonempty t h ι'.unop
    classical
      have : ∀ ι' : (Finset ι)ᵒᵖ, Finite ((hallMatchingsFunctor t).obj ι') := by
        intro ι'
        rw [hallMatchingsFunctor]
        infer_instance
      -- Apply the compactness argument
      obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (hallMatchingsFunctor t)
      -- Interpret the resulting section of the inverse limit
      refine ⟨?_, ?_, ?_⟩
      · -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩
      · -- Show that it is injective
        intro i i'
        have subi : ({i} : Finset ι) ⊆ {i, i'} := by simp
        have subi' : ({i'} : Finset ι) ⊆ {i, i'} := by simp
        simp only
        rw [← hu (CategoryTheory.homOfLE subi).op, ← hu (CategoryTheory.homOfLE subi').op]
        let uii' := u (Opposite.op ({i, i'} : Finset ι))
        exact fun h => Subtype.mk_eq_mk.mp (uii'.property.1 h)
      · -- Show that it maps each index to the corresponding finite set
        intro i
        apply (u (Opposite.op ({i} : Finset ι))).property.2
  · -- The reverse direction is a straightforward cardinality argument
    rintro ⟨f, hf₁, hf₂⟩ s
    rw [← Finset.card_image_of_injective s hf₁]
    apply Finset.card_le_card
    grind

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
h : R.image ↑A = ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)
⊢ Fintype ↑↑(A.biUnion fun a ↦ (R.image {a}).toFinset)

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
h : R.image ↑A = ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)
⊢ Fintype ↑↑(A.biUnion fun a ↦ (R.image {a}).toFinset)
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : 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
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous (⇑re ∘ ⇑l + const E c)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : 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
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
f : E → ℝ
hf : f ∈ 𝓕
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ Continuous (⇑re ∘ ⇑l + const E c)
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map (f₂ ≫ g₁))) x ∈ s

Tactic:
]

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map (f₂ ≫ g₁))) x ∈ s
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
r' : α → Finset β := fun a ↦ (R.image {a}).toFinset
A : Finset α
⊢ #(R.image ↑A).toFinset = #(A.biUnion r')

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
r' : α → Finset β := fun a ↦ (R.image {a}).toFinset
A : Finset α
⊢ #(R.image ↑A).toFinset = #(A.biUnion r')
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
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ affineSegment R (s.points (({i, j}.orderEmbOfFin ⋯) 0)) (s.points (({i, j}.orderEmbOfFin ⋯) 1)) =
    affineSegment R (s.points (min i j)) (s.points (max i j))

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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ affineSegment R (s.points (({i, j}.orderEmbOfFin ⋯) 0)) (s.points (({i, j}.orderEmbOfFin ⋯) 1)) =
    affineSegment R (s.points (min i j)) (s.points (max i j))
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x : β
y : α
⊢ some x = f y ↔ some x = f y

Tactic:
]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x : β
y : α
⊢ f.symm x = some y ↔ f.symm x = some y

Tactic:
]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : a₁ ∈ f.symm b
h₂ : a₂ ∈ f.symm b
⊢ a₁ = a₂
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case refine_2
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map f₁)) ((ConcreteCategory.hom (F.map f₂)) x) =
    (ConcreteCategory.hom (F.map f₁)) ((ConcreteCategory.hom (F.map f₂)) x)

Tactic:
]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x

Tactic:
]

Goal state after:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
⊢ ∀ (x : α), x ∈ s

Tactic:
]

Goal state after:
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
⊢ ∀ (x : α), x ∈ s
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ (PEquiv.refl α) x✝

Tactic:
]

Goal state after:
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ (PEquiv.refl α) x✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true
Module: Mathlib.Data.PEquiv

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

Tactic:
]

Goal state after: