mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
i : Fin n
⊢ insertNth 0 x f i.succ.castSucc ≤ insertNth 0 x f i.succ.succ

Tactic:
simpa using

Goal state after:
case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : x ≤ f 0
i : Fin n
⊢ f i.castSucc ≤ f i.succ
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : x < f 0
i : Fin n
⊢ insertNth 0 x f i.succ.castSucc < insertNth 0 x f i.succ.succ

Tactic:
simpa using

Goal state after:
case inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : x < f 0
i : Fin n
⊢ f i.castSucc < f i.succ
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty { t // t ⊆ s ∧ IsChain r t }
⊢ ⨆ i, ?m.28 i < ⊤

Tactic:
by rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top]

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
x : α
⊢ x ∈ s ↔ x ∈ ∅

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ a ⊆ s, IsChain r a → a = ∅
x : α
⊢ x ∉ s
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain (flip r) a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ r x y ∨ r y x) x✝¹ x✝

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight (flip r)
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain (flip r) a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ r x✝¹ x✝ ∨ r x✝ x✝¹
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ (fun x y ↦ flip r x y ∨ flip r y x) x✝¹ x✝

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
x✝¹ : α
hx : x✝¹ ∈ a
x✝ : α
hy : x✝ ∈ a
hne : x✝¹ ≠ x✝
⊢ r x✝¹ x✝ ∨ r x✝ x✝¹
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
i : Fin n
⊢ (last (n + 1)).insertNth x f i.castSucc.castSucc ≤ (last (n + 1)).insertNth x f i.castSucc.succ

Tactic:
simpa using

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
i : Fin n
⊢ f i.castSucc ≤ f i.succ
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
hs : (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) = fun x y ↦ r ↑x ↑y
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
hc :
  ((⇑(Subtype.relEmbedding (fun x1 x2 ↦ r x1 x2) fun x ↦ x ∈ s) '' univ).chainHeight fun x1 x2 ↦ r x1 x2) =
    univ.chainHeight (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2)
hs : (Subtype.val ⁻¹'o fun x1 x2 ↦ r x1 x2) = fun x y ↦ r ↑x ↑y
⊢ (univ.chainHeight fun x1 x2 ↦ r ↑x1 ↑x2) = s.chainHeight r
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 ≤ x2) = s.chainHeight fun x1 x2 ↦ x1 ≤ x2

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
inst✝ : LE α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 ≤ x2) = s.chainHeight fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LT α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 < x2) = s.chainHeight fun x1 x2 ↦ x1 < x2

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
inst✝ : LT α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 < x2) = s.chainHeight fun x1 x2 ↦ x1 < x2
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x

Tactic:
simpa using

Goal state after:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ 1 < c
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : f (last n) < x
i : Fin n
⊢ (last (n + 1)).insertNth x f i.castSucc.castSucc < (last (n + 1)).insertNth x f i.castSucc.succ

Tactic:
simpa using

Goal state after:
case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
x : α
hx : f (last n) < x
i : Fin n
⊢ f i.castSucc < f i.succ
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Icc a b).ncard = b + 1 - a

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ (Icc a b).ncard = b + 1 - a
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ico a b).ncard = b - a

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ (Ico a b).ncard = b - a
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioc a b).ncard = b - a

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ (Ioc a b).ncard = b - a
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (Ioo a b).ncard = b - a - 1

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ (Ioo a b).ncard = b - a - 1
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: a b : ℕ
⊢ (uIcc a b).ncard = (↑b - ↑a).natAbs + 1

Tactic:
simpa using

Goal state after:
a b : ℕ
⊢ (uIcc a b).ncard = (↑b - ↑a).natAbs + 1
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: b : ℕ
⊢ (Iic b).ncard = b + 1

Tactic:
simpa using

Goal state after:
b : ℕ
⊢ (Iic b).ncard = b + 1
Module: Mathlib.Order.Interval.Set.Nat

Goal state before:
pp: b : ℕ
⊢ (Iio b).ncard = b

Tactic:
simpa using

Goal state after:
b : ℕ
⊢ (Iio b).ncard = b
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ↑j - ↑i ≤ n

Tactic:
simpa using

Goal state after:
case refine_1
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : ↑(Icc 0 n)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ↑j ≤ n + ↑i
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a ↦ exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t ↦ Nat.rec ⟨b, hb⟩ (fun x a ↦ ⟨⋯.choose, ⋯⟩) t
i : ℕ
⊢ (fun i ↦ ↑(ks i)) i ⋖ (fun i ↦ ↑(ks i)) (i + 1)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
h : ∀ (a : { a // (Ici a).Infinite }), ∃ b, ↑a ⋖ b ∧ (Ici b).Infinite :=
  fun a ↦ exists_covby_infinite_Ici_of_infinite_Ici a.property (hfin ↑a)
ks : ℕ → { a // (Ici a).Infinite } := fun t ↦ Nat.rec ⟨b, hb⟩ (fun x a ↦ ⟨⋯.choose, ⋯⟩) t
i : ℕ
⊢ ↑(ks i) ⋖ ↑(ks (i + 1))
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : IsStronglyAtomic α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ (Ici ⊥).Infinite

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : IsStronglyAtomic α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
⊢ univ.Infinite
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : grade ℕ (f i) = i
⊢ grade ℕ (f (i + 1)) = i + 1

Tactic:
simpa using

Goal state after:
case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : grade ℕ (f i) = i
⊢ i + 1 = grade ℕ (f (i + 1))
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
h'' : ∀ (j : ↑(Icc 0 n)), (B j).Nonempty
⊢ n = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : ⋃ j, B j = univ
hδ : 0 ≤ δ / 2
h'' : ∀ (j : ↑(Icc 0 n)), (B j).Nonempty
⊢ n = 0
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ≈ ?m.17 h

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ≈ ?m.17 h
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ⊓ y ≈ y

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ⊓ y ≈ y
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ x ⊓ y ≈ ?m.27 h

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ x ⊓ y ≈ ?m.27 h
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ y ≈ x ⊔ y

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid x y
⊢ y ≈ x ⊔ y
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
this : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
⊢ r b c

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
this : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
⊢ r (b ⊓ c ⊓ (b ⊔ c)) (b ⊓ c ⊔ (b ⊔ c))
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r (b ⊓ c) d

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r (b ⊓ c) d
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊔ z

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ (y ⊓ z) ≤ y ⊔ z
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ y ⊓ z

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ (y ⊓ z) ≤ y ∧ x ⊓ (y ⊓ z) ≤ z
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (y ⊓ (x ⊓ z)) (y ⊓ z)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
this : r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
⊢ r (y ⊓ (z ⊓ x)) (y ⊓ z)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (y ⊔ z) (x ⊔ y ⊔ z)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (y ⊔ z) (x ⊔ (y ⊔ z))
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x✝ y✝ : α
h : r x✝ y✝
⊢ r y✝ x✝

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x✝ y✝ : α
h : r x✝ y✝
⊢ r (x✝ ⊓ y✝ ⊓ (x✝ ⊔ y✝)) (x✝ ⊓ y✝ ⊔ (x✝ ⊔ y✝))
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_inf : ∀ {x y t : α}, r x y → r (x ⊓ t) (y ⊓ t)
⊢ r (w ⊓ y✝) (w ⊓ z✝)

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_inf : ∀ {x y t : α}, r x y → r (x ⊓ t) (y ⊓ t)
⊢ r (y✝ ⊓ w) (z✝ ⊓ w)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_sup : ∀ {x y t : α}, r x y → r (x ⊔ t) (y ⊔ t)
⊢ r (w ⊔ y✝) (w ⊔ z✝)

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
h1 : r w x✝
h2 : r y✝ z✝
compatible_left_sup : ∀ {x y t : α}, r x y → r (x ⊔ t) (y ⊔ t)
⊢ r (y✝ ⊔ w) (z✝ ⊔ w)
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
hle : i + 1 ≤ j
⊢ π ⋯ ⟨i + 1, π hle b⟩.snd = ⟨i, a⟩.snd

Tactic:
by rw [π_trans, ← h2]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ m ((x ⊔ k) ⊓ (y ⊔ k))

Tactic:
← sup_inf_right,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l = l ⊓ m (x ⊓ y ⊔ k)
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ n ((x ⊔ k) ⊓ (y ⊔ k)) = n k

Tactic:
← sup_inf_right,

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ n (x ⊓ y ⊔ k) = n k
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x y : X
m n : Nucleus X
⊢ ∀ (x : X), x ≤ ⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x y : X
m n : Nucleus X
⊢ ∀ (x i : X), x ≤ i → x ⊓ m i ≤ n i
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
x✝¹ n x✝ : Nucleus X
⊢ x✝¹ ≤ n ⇨ x✝ ↔ x✝¹ ⊓ n ≤ x✝

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
x✝¹ n x✝ : Nucleus X
⊢ (∀ (i i_1 : X), i ≤ i_1 → x✝¹ i ⊓ n i_1 ≤ x✝ i_1) ↔ ∀ (i : X), x✝¹ i ⊓ n i ≤ x✝ i
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
parts✝¹ : Set α
sSupIndep'✝¹ : sSupIndep parts✝¹
bot_notMem'✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h :
  { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ }.parts =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts
⊢ { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }

Tactic:
simpa using

Goal state after:
case mk.mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
parts✝¹ : Set α
sSupIndep'✝¹ : sSupIndep parts✝¹
bot_notMem'✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h :
  { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ }.parts =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts
⊢ parts✝¹ = parts✝
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_3
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b

Tactic:
· apply le_antisymm
    · apply iInf₂_le a ha
    · apply le_trans (le_iSup₂ b hb) h

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
h : x ∈ u
⊢ (P.partOf x).Nonempty

Tactic:
simpa using

Goal state after:
α : Type u_1
x : α
u : Set α
P : Partition u
h : x ∈ u
⊢ ¬P.partOf x = ∅
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ = 0
⊢ r = ⊥

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ = 0
⊢ r = ⊥
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥

Tactic:
simpa using

Goal state after:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ ⊤ ∈ S

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
S : Sublocale X
⊢ ⊤ ∈ S