mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y z : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x

Tactic:
constructor

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✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ z ∈ affineSegment R x y → z ∈ affineSegment R y x

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
x y z : P
⊢ z ∈ affineSegment R y x → z ∈ affineSegment R x y
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝¹¹ : Ring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddTorsor V P
inst✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 ≤ a • 1

Tactic:
rw [← zero_smul R' (1 : R)]

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝¹¹ : Ring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddTorsor V P
inst✝⁶ : ZeroLEOneClass R
R' : Type u_6
inst✝⁵ : Ring R'
inst✝⁴ : PartialOrder R'
inst✝³ : Module R' V
inst✝² : Module R' R
inst✝¹ : IsScalarTower R' R V
inst✝ : SMulPosMono R' R
x y : P
a : R'
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ 0 • 1 ≤ a • 1
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2.refine_2.cons.cons
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 R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl))) l' = head :: head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl

Tactic:
pairwise_cons

Goal state after:
case refine_2.refine_2.cons.cons
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 R
hl's : l'.SortedLE
head head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
hp : (∀ a' ∈ head2 :: tail, head ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail)
hl'l :
  map (⇑(lineMap ((head :: head2 :: tail).head hl) ((head :: head2 :: tail).getLast hl))) l' = head :: head2 :: tail
⊢ head ≠ (head :: head2 :: tail).getLast hl
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 x y z ∧ Wbtw R y x z ↔ x = y

Tactic:
constructor

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✝³ : 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

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

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

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

case mpr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite ι
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos.refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
⊢ ⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i) = s.domRestrict φ

Tactic:
ext

Goal state after:
case pos.refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
𝓕' : Set (↑s → ℝ)
h𝓕' :
  𝓕'.Countable ∧
    sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
he : 𝓕' = ∅
hsφ : s.domRestrict φ = 0
this : ∀ (a : ↑s), s.domRestrict φ a = 0 a
x✝ : ↑s
⊢ (⨆ i, s.domRestrict (⇑re ∘ ⇑((fun x ↦ 0) i)) + const (↑s) ((fun x ↦ 0) i)) x✝ = s.domRestrict φ x✝
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 : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
⊢ (ConcreteCategory.hom (F.map g)) x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s

Tactic:
by
    rw [mem_iInter] at h ⊢
    intro f
    rw [← mem_preimage, preimage_preimage, mem_preimage]
    convert! h (g ≫ f); rw [F.map_comp]; rfl

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

Goal state before:
pp: case refine_2
𝕜 : 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
f : E → ℝ
x✝ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
⊢ (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) (f ∘ Subtype.val) = f

Tactic:
ext

Goal state after:
case refine_2
𝕜 : 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
f : E → ℝ
x✝¹ : f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
hp : f ≤ φ
l : E →L[𝕜] 𝕜
c : ℝ
hlc : f = ⇑re ∘ ⇑l + const E c
x✝ : E
⊢ (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) (f ∘ Subtype.val) x✝ = f x✝
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:
constructor

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

case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
⊢ (∃ f, Injective f ∧ ∀ (x : ι), f x ∈ t x) → ∀ (s : Finset ι), #s ≤ #(s.biUnion 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✝⁴ : 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 ↔ p ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
constructor

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

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
p : P
⊢ p ∈ affineSegment R (s.points 0) (s.points 1) → p ∈ s.closedInterior
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
⊢ φ ∘ Subtype.val ∘ ⇑(Equiv.Set.univ E).symm = φ

Tactic:
ext

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
⊢ (φ ∘ Subtype.val ∘ ⇑(Equiv.Set.univ E).symm) x✝ = φ x✝
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inl
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
hij : i < j
⊢ affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))

Tactic:
simp [min_eq_left hij.le, max_eq_right hij.le]

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 α
⊢ R.image ↑A = ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)

Tactic:
ext

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
A : Finset α
x✝ : β
⊢ x✝ ∈ R.image ↑A ↔ x✝ ∈ ↑(A.biUnion fun a ↦ (R.image {a}).toFinset)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (PEquiv.refl α).trans f = f

Tactic:
ext

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ ((PEquiv.refl α).trans f) x✝ = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans (PEquiv.refl β) = f

Tactic:
ext

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ (f.trans (PEquiv.refl β)) x✝ = some a✝ ↔ f x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = ofSet {a | (f a).isSome = true}

Tactic:
ext

Goal state after:
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (f.trans f.symm) x✝ = some a✝ ↔ (ofSet {a | (f a).isSome = true}) x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ (∃ a, f x✝ = some a ∧ f a✝ = some a) → a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}

case mpr
α : Type u
β : Type v
f : α ≃. β
x✝ a✝ : α
⊢ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1} → ∃ a, f x✝ = some a ∧ f a✝ = some a
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
j i✝ : J
hi : i✝ ⟶ j
hf : (range ⇑(ConcreteCategory.hom (F.map hi))).Finite
m : Finset (F.obj j)
hmin : ∀ x ∈ {s | ∃ i f, ↑s = range ⇑(ConcreteCategory.hom (F.map f))}, ¬x ⊂ m
i : J
f : i ⟶ j
hm : ↑m = range ⇑(ConcreteCategory.hom (F.map f))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊆
    (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
⊢ ¬(fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊂
      (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩

Tactic:
have := hmin _ ⟨k', g', (m.finite_toSet.subset <| hm.substr hl).coe_toFinset⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
j i✝ : J
hi : i✝ ⟶ j
hf : (range ⇑(ConcreteCategory.hom (F.map hi))).Finite
m : Finset (F.obj j)
hmin : ∀ x ∈ {s | ∃ i f, ↑s = range ⇑(ConcreteCategory.hom (F.map f))}, ¬x ⊂ m
i : J
f : i ⟶ j
hm : ↑m = range ⇑(ConcreteCategory.hom (F.map f))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊆
    (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
this : ¬⋯.toFinset ⊂ m
⊢ ¬(fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨k', g'⟩ ⊂
      (fun f ↦ range ⇑(ConcreteCategory.hom (F.map f.snd))) ⟨i, f⟩
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
⊢ f.trans ⊥ = ⊥

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x✝ : α
a✝ : γ
⊢ (f.trans ⊥) x✝ = some a✝ ↔ ⊥ x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β ≃. γ
⊢ ⊥.trans f = ⊥

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x✝ : α
a✝ : γ
⊢ (⊥.trans f) x✝ = some a✝ ↔ ⊥ x✝ = some a✝
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
⊢ (single a b).trans f = single a c

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ ((single a b).trans f) x✝ = some a✝ ↔ (single a c) x✝ = some 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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ s.interior ↔ p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1

Tactic:
constructor

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
p : P
⊢ p ∈ s.interior → p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1

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
p : P
⊢ p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 → p ∈ s.interior
Module: Mathlib.Data.PEquiv

Goal state before:
pp: β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
⊢ f.trans (single b c) = ⊥

Tactic:
ext

Goal state after:
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
x✝ : δ
a✝ : γ
⊢ (f.trans (single b c)) x✝ = some a✝ ↔ ⊥ x✝ = some a✝
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ f.symm.toMatrix = f.toMatrixᵀ

Tactic:
ext

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
j✝ : m
⊢ f.symm.toMatrix i✝ j✝ = f.toMatrixᵀ i✝ j✝
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ (PEquiv.refl n).toMatrix = 1

Tactic:
ext

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : n
⊢ (PEquiv.refl n).toMatrix i✝ j✝ = 1 i✝ j✝
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
⊢ f.toPEquiv.toMatrix i = Pi.single (f i) 1

Tactic:
ext

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
x✝ : n
⊢ f.toPEquiv.toMatrix i x✝ = Pi.single (f i) 1 x✝
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
⊢ f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) 1

Tactic:
ext

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
x✝ : m
⊢ f.toPEquiv.toMatrixᵀ j x✝ = Pi.single (f.symm j) 1 x✝
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
⊢ (f.toPEquiv.toMatrix * M) i j = M.submatrix (⇑f) id i j

Tactic:
toMatrix_mul_apply,

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
⊢ (Option.casesOn (f.toPEquiv i) 0 fun fi ↦ M fi j) = M.submatrix (⇑f) id i j
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inl
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
hij : i < j
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
simp [min_eq_left hij.le, max_eq_right hij.le]

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix =
    1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix

Tactic:
ext

Goal state after:
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i✝ j✝ =
    (1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix) i✝ j✝
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

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

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s

case mpr
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : 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
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ t₁ * t₂ / (1 - t₁ + t₁ * t₂) ∈ Set.Icc 0 1

Tactic:
constructor

Goal state after:
case refine_1.left
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
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 0 ≤ t₁ * t₂ / (1 - t₁ + t₁ * t₂)

case refine_1.right
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
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ t₁ * t₂ / (1 - t₁ + t₁ * t₂) ≤ 1
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ innerDual ∅ = ⊤

Tactic:
ext

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
⊢ x✝ ∈ innerDual ∅ ↔ x✝ ∈ ⊤
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ innerDual 0 = ⊤

Tactic:
ext

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x✝ : E
⊢ x✝ ∈ innerDual 0 ↔ x✝ ∈ ⊤
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x : E
⊢ innerDual {x} = comap ((innerSL ℝ) x) (positive ℝ ℝ)

Tactic:
ext

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x✝ : E
⊢ x✝ ∈ innerDual {x} ↔ x✝ ∈ comap ((innerSL ℝ) x) (positive ℝ ℝ)
Module: Mathlib.Analysis.Convex.Cone.InnerDual

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
ι : Sort u_4
f : ι → Set E
⊢ innerDual (⋃ i, f i) = ⨅ i, innerDual (f i)

Tactic:
ext

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
ι : Sort u_4
f : ι → Set E
x✝ : E
⊢ x✝ ∈ innerDual (⋃ i, f i) ↔ x✝ ∈ ⨅ i, innerDual (f i)