mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : 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
x : ↑s
hx : s.domRestrict φ x ≠ 0 x
this : sSup 𝓕' x = s.domRestrict φ x
⊢ s = ∅

Tactic:
simp_all

Goal state after:
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
⊢ sSup ((fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) '' 𝓕) x = (sSup 𝓕 ∘ ⇑(Equiv.Set.univ E).symm) x

Tactic:
sSup_image',

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 = (sSup 𝓕 ∘ ⇑(Equiv.Set.univ E).symm) x
Module: Mathlib.Combinatorics.Hall.Basic

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

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

Tactic:
· 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

Goal state after:
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.Combinatorics.Hall.Basic

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

Tactic:
rintro ⟨f, hf₁, hf₂⟩ s
    rw [← Finset.card_image_of_injective s hf₁]
    apply Finset.card_le_card
    grind

Goal state after:
Module: Mathlib.Data.PEquiv

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
h✝ : x✝ = a
⊢ ((some b).bind fun a ↦ f a) = some a✝ ↔ some c = some a✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
h✝ : ¬x✝ = a
⊢ (none.bind fun a ↦ f a) = some a✝ ↔ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
h✝ : x✝ = b
⊢ ¬some c = some a✝¹

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x✝¹ : δ
a✝¹ : γ
h : ∀ (a : δ), ¬f a = some b
x✝ : β
a✝ : f x✝¹ = some x✝
h✝ : ¬x✝ = b
⊢ ¬False

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 1 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 1 - 1 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 1 = 1 - 0 - 1 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 1 - 0 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 1 - 0 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 1 = 0 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 0 - 1 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∈ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 1 = 0 - 0 - 1 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 1 = 0 - 0 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∈ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 1 = 0 - 0 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 1 - 1 - 0 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 1 - 1 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 0 = 1 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 1 - 0 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 1 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ some i
h✝ : i✝ = j
⊢ 0 = 0 - 1 - 0 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∈ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 0 - 1 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : i✝ = i
h✝³ : j✝ ∉ some j
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ some i
h✝ : i✝ = j
⊢ 0 = 0 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∈ none
⊢ 0 = 0 - 0 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : i✝ = i
h✝⁴ : j✝ ∉ some j
h✝³ : ¬i✝ = j✝
h✝² : j✝ ∉ some i
h✝¹ : ¬i✝ = j
h✝ : j✝ ∉ none
⊢ 0 = 0 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 1 = 1 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 1 = 1 - 1 - 0 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 1 = 1 - 0 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 1 = 1 - 0 - 0 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 1 = 0 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 1 = 0 - 1 - 0 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 1 = 0 - 0 - 1 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∈ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 1 = 0 - 0 - 0 + 0 + 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 0 = 1 - 1 - 1 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 0 = 1 - 1 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 0 = 1 - 0 - 1 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 0 = 1 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∈ some j
⊢ 0 = 0 - 1 - 1 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∈ none
h✝ : j✝ ∉ some j
⊢ 0 = 0 - 1 - 0 + 1 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∈ some j
⊢ 0 = 0 - 0 - 1 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁵ : ¬i✝ = i
h✝⁴ : i✝ = j
h✝³ : j✝ ∉ some i
h✝² : ¬i✝ = j✝
h✝¹ : j✝ ∉ none
h✝ : j✝ ∉ some j
⊢ 0 = 0 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∈ none
⊢ 1 = 1 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∉ none
⊢ 1 = 1 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∈ none
⊢ 1 = 0 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∈ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∉ none
⊢ 1 = 0 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∈ none
⊢ 0 = 1 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : i✝ = j✝
h✝ : j✝ ∉ none
⊢ 0 = 1 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case pos
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∈ none
⊢ 0 = 0 - 1 - 1 + 1 + 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
n : Type u_4
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j i✝ j✝ : n
h✝⁴ : ¬i✝ = i
h✝³ : ¬i✝ = j
h✝² : j✝ ∉ some i✝
h✝¹ : ¬i✝ = j✝
h✝ : j✝ ∉ none
⊢ 0 = 0 - 0 - 0 + 0 + 0

Tactic:
simp_all

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz✝ : x ≤ z
hxz : x = z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
subst hxz

Goal state after:
case inl
R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ Set.extremePoints R ↑(doublyStochastic R n)

Tactic:
rintro _ ⟨σ, rfl⟩

Goal state after:
case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R ↑(doublyStochastic R n)
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ hx₂ : x₁ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁
this : ∀ (i j : n), x₁ i j = x₁ i j
⊢ x₁ = Equiv.Perm.permMatrix R σ

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
ext; simp [forall_comm (α := M)]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
ext; simp [forall_comm (α := M)]

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

Goal state before:
pp: case 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 y z : P
h : y -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
simp_all

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

Goal state before:
pp: case inr.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 y z : P
h : z -ᵥ x = 0
⊢ Wbtw R x y z ∨ Wbtw R x z y

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
ext; simp [forall_comm (α := M)]

Goal state after: