mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : β
⊢ x✝¹ ≤ x✝ → (inr α β) x✝¹ ≤ (inr α β) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : β
⊢ x✝¹ < x✝ → (inr α β) x✝¹ < (inr α β) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : α × β
⊢ x✝¹ ≤ x✝ → (fst α β) x✝¹ ≤ (fst α β) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : Monoid β
inst✝ : Preorder β
x✝¹ x✝ : α × β
⊢ x✝¹ ≤ x✝ → (snd α β) x✝¹ ≤ (snd α β) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : α),
    (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun (x * y) =
      (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun x * (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : β),
    (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun (x * y) =
      (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun x * (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : Lex (α × β)), (ofLex (x * y)).1 = (ofLex x).1 * (ofLex y).1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
m : α
n : β
⊢ (inl α β) m * (inr α β) n = (m, n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
m : α
n : β
⊢ (inlₗ α β) m * (inrₗ α β) n = toLex (m, n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(inl M₀ N₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Lattice

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
⊢ ⨆ i, v (x i) = ⨆ i, v (x ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Units

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Monoid α
inst✝¹ : Preorder β
inst✝ : Monoid β
e : α ≃*o β
x y : αˣ
⊢ (Units.mapEquiv e.toMulEquiv).toFun x ≤ (Units.mapEquiv e.toMulEquiv).toFun y ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(inr M₀ N₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero M₀
inst✝¹ : GroupWithZero N₀
inst✝ : Preorder N₀
⊢ Monotone ⇑(fst M₀ N₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝² : GroupWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : LinearOrderedCommGroupWithZero N₀
⊢ Monotone ⇑(snd M₀ N₀)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((WithZero.map' (toLexMulEquiv (αˣ × βˣ)).toMonoidHom).comp (MonoidWithZeroHom.inl α β))).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((WithZero.map' (toLexMulEquiv (αˣ × βˣ)).toMonoidHom).comp (MonoidWithZeroHom.inr α β))).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ (fst α β).comp (inl α β) = OrderMonoidWithZeroHom.id α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : α
hm : m ≠ 0
⊢ (inl α β) m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 m hm))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
n : β
hn : n ≠ 0
⊢ (inr α β) n = ↑((OrderMonoidHom.inrₗ αˣ βˣ) (Units.mk0 n hn))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
⊢ (inl α β) m * (inr α β) n = ↑(toLex (Units.mk0 m hm, Units.mk0 n hn))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
by
  classical rw [Icc, Icc, ← Finset.image_add_left_Icc, Finset.image_val,
      ((Finset.nodup _).map <| add_right_injective c).dedup]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊓ y = ⅟2 • (x + y - |y - x|)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
⊢ |a • b| = |a| • |b|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ 0 ≤ |a|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ n • |a| = (n • 1) • |a|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
⊢ Ico (a + 1) b = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this✝ : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
this : n • |a| = (n • 1) • |a|
⊢ 0 ≤ |a|

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
⊢ mk (k • a) = mk a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
⊢ mk a ≤ mk (k • a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
s : UpperSet (FiniteArchimedeanClass M)
k : K
a : M
ha : a ∈ (addSubgroup s).carrier
ne : ArchimedeanClass.mk (k • a) ≠ ⊤
eq : ArchimedeanClass.mk a = ⊤
⊢ ArchimedeanClass.mk (k • a) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b + 1
⊢ insert (b + 1) (Icc a b) = Icc a (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert a (Ico (a + 1) b) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 * (↑x).2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑y).2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
⊢ False

Tactic:
obtain ⟨g, hg⟩ :=
    h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2

Goal state after:
α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))
⊢ False
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
⊢ (s.mulAntidiagonal t a).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a < b
⊢ insert (a + 1) (Ioc (a + 1) b) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico a (b + 1) = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
⊢ Ioc a (b - 1) = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : NonemptyInterval α
h : s.toProd = t.toProd
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
s : NonemptyInterval α
x : α × α
a : α
inst✝ : Nonempty α
⊢ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ b ∈ pure a ↔ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
s : Interval α
⊢ dual (map f s) = map (OrderHom.dual f) (dual s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Interval α
⊢ ↑(dual s) = ⇑ofDual ⁻¹' ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α →o β
⊢ ⇑f '' ↑⊥ ⊆ ↑(map f ⊥)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
by

Goal state after: