awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
hb : d = ur.b
ha' : (↑a' : ℕ) = (↑w : ℕ) + x
hb' : (↑b' : ℕ) = y + (↑z : ℕ)
hdet : w * z = (x * y).succPNat
hdet' : (↑w : ℕ) * (↑z : ℕ) = x * y + 1
hv : ((↑a' : ℕ) * (↑d : ℕ), (↑b' : ℕ) * (↑d : ℕ)) = ((↑a : ℕ), (↑b : ℕ))
ha'' : (↑a : ℕ) = (↑a' : ℕ) * (↑d : ℕ)
hb'' : (↑b : ℕ) = (↑b' : ℕ) * (↑d : ℕ)
hza' : (↑z : ℕ) * (↑a' : ℕ) = x * (↑b' : ℕ) + 1
hwb' : (↑w : ℕ) * (↑b' : ℕ) = y * (↑a' : ℕ) + 1
⊢ (↑z : ℕ) * (↑a : ℕ) = x * (↑b : ℕ) + (↑d : ℕ) ∧ (↑w : ℕ) * (↑b : ℕ) = y * (↑a : ℕ) + (↑d : ℕ)

Tactic:
grind
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
⊢ a = a.gcdA' b * a.gcdD b

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
⊢ b = a.gcdB' b * a.gcdD b

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
⊢ a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
⊢ a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left₂ : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
⊢ (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left₁ : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left₂ : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)

Tactic:
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩

Premises used: PNat.gcd_props
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
a₁ : a.gcdD b ∣ a.gcd b
a₂ : a.gcd b ∣ a.gcdD b
⊢ a.gcdD b = a.gcd b

Tactic:
apply dvd_antisymm

Premises used: PNat.dvd_antisymm
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
a₁ : a.gcdD b ∣ a
a₂ : a.gcdD b ∣ b
⊢ a.gcdD b ∣ a.gcd b

Tactic:
apply dvd_gcd

Premises used: PNat.dvd_gcd
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b ∣ a

Tactic:
Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm

Premises used: Dvd.intro, PNat.gcdA', mul_comm, Eq.symm, Eq.trans
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b ∣ a

Tactic:
exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm

Premises used: Dvd.intro, PNat.gcdA', mul_comm, Eq.symm, Eq.trans
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b ∣ b

Tactic:
Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm

Premises used: Dvd.intro, mul_comm, Eq.symm, Eq.trans, PNat.gcdB'
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ a.gcdD b ∣ b

Tactic:
exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm

Premises used: Dvd.intro, mul_comm, Eq.symm, Eq.trans, PNat.gcdB'
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdZ b) : ℕ) * (↑a : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
⊢ (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)

Tactic:
rw [h₅] at h₇
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdZ b) : ℕ) * (↑a : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
h₉ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
⊢ (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)

Tactic:
rw [h₅] at h₇
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
a₁ : (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdD b) : ℕ)
⊢ a.gcd b ∣ a.gcdD b

Tactic:
rw [dvd_iff]

Premises used: PNat.dvd_iff
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
⊢ (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdD b) : ℕ)

Tactic:
(Nat.dvd_add_iff_right h₈).mpr h₇

Premises used: Iff.mpr, Nat.dvd_add_iff_right
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
left : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left_1 : a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat
left_2 : a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat
h₅ : (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
right : (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcdD b) : ℕ)
h₇ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ) + (↑(a.gcdD b) : ℕ)
h₈ : (↑(a.gcd b) : ℕ) ∣ a.gcdX b * (↑b : ℕ)
⊢ (↑(a.gcd b) : ℕ) ∣ (↑(a.gcdD b) : ℕ)

Tactic:
exact (Nat.dvd_add_iff_right h₈).mpr h₇

Premises used: Iff.mpr, Nat.dvd_add_iff_right
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat

Tactic:
(gcd_props a b).1

Premises used: PNat.gcd_props, And.left
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ a = a.gcdA' b * a.gcd b

Tactic:
gcd_eq a b ▸ (gcd_props a b).2.1

Premises used: PNat.gcd_props, Eq.rec, And.right, And.left, PNat.gcd_eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ b = a.gcdB' b * a.gcd b

Tactic:
gcd_eq a b ▸ (gcd_props a b).2.2.1

Premises used: PNat.gcd_props, Eq.rec, And.right, And.left, PNat.gcd_eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ a.gcdZ b * a.gcdA' b = (a.gcdX b * (↑(a.gcdB' b) : ℕ)).succPNat

Tactic:
(gcd_props a b).2.2.2.1

Premises used: PNat.gcd_props, And.right, And.left
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ a.gcdW b * a.gcdB' b = (a.gcdY b * (↑(a.gcdA' b) : ℕ)).succPNat

Tactic:
(gcd_props a b).2.2.2.2.1

Premises used: PNat.gcd_props, And.right, And.left
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ (↑(a.gcdZ b) : ℕ) * (↑a : ℕ) = a.gcdX b * (↑b : ℕ) + (↑(a.gcd b) : ℕ)

Tactic:
gcd_eq a b ▸ (gcd_props a b).2.2.2.2.2.1

Premises used: PNat.gcd_props, Eq.rec, And.right, And.left, PNat.gcd_eq
-- Module: Mathlib.Data.PNat.Xgcd
Goal:
a b : ℕ+
⊢ (↑(a.gcdW b) : ℕ) * (↑b : ℕ) = a.gcdY b * (↑a : ℕ) + (↑(a.gcd b) : ℕ)

Tactic:
gcd_eq a b ▸ (gcd_props a b).2.2.2.2.2.2

Premises used: PNat.gcd_props, Eq.rec, And.right, PNat.gcd_eq
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
left : a₁ < a₃
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₃ b₃

Tactic:
left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
left : a₁ < a₂
left₁ : a₂ < a₃
left₂ : ι
⊢ a₁ < a₃

Tactic:
apply lt_trans

Premises used: lt_trans
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
⊢ a₁ < a₂

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
⊢ a₂ < a₃

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
h : a₁ < a₂
h_1 : a₂ < a₃
⊢ ι

Tactic:
repeat' assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
h : a₁ < a₂
b₂_1 : α a₂
h_1 : b₂ ≤ b₂_1
left : a₁ < a₂
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₂ b₂_1

Tactic:
left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
h : a₁ < a₂
b₂_1 : α a₂
h_1 : b₂ ≤ b₂_1
⊢ a₁ < a₂

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂ : α a₁
h : b₁ ≤ b₂
h_1 right : a₁ < a₃
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₃ b₃

Tactic:
left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂ : α a₁
h : b₁ ≤ b₂
h_1 : a₁ < a₃
⊢ a₁ < a₃

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
right : b₁ ≤ b₂_1
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ ≤ mk (β := fun (i : ι) ↦ α i) a₁ b₂_1

Tactic:
right
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
right : b₁ ≤ b₂
right₁ : b₂ ≤ b₂_1
right₂ : α a₁
⊢ b₁ ≤ b₂_1

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
⊢ b₁ ≤ b₂

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
⊢ b₂ ≤ b₂_1

Tactic:
assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂ : α a₁
h : b₁ ≤ b₂
b₂_1 : α a₁
h_1 : b₂ ≤ b₂_1
⊢ α a₁

Tactic:
repeat' assumption
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩

Premises used: le_of_lt, PSigma.Lex.mono_right, And.intro, Iff.intro
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
refine_1 : ∀ (a b : Σₗ' (i : ι), α i) (hab : a < b), ¬b ≤ a
refine_2 : ∀ (a b : Σₗ' (i : ι), α i), a ≤ b ∧ ¬b ≤ a → a < b
⊢ ∀ (a b : Σₗ' (i : ι), α i), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine fun a b => ⟨fun hab => ⟨hab.mono_right fun i a b => le_of_lt, ?_⟩, ?_⟩
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i : α a₁
a₂ : ι
a : α a₂
hji : a₁ < a₂
hab : mk (β := fun (i : ι) ↦ α i) a₂ a < mk (β := fun (i : ι) ↦ α i) a₁ i
refine_1 : ∀ (hij : a₂ < a₁), False
refine_1₁ : ∀ (a : α a₁) (hji : a₁ < a₁) (hab : a < i), False
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hab : mk (β := fun (i : ι) ↦ α i) i b₂ < mk (β := fun (i : ι) ↦ α i) i b₁
refine_1 : ∀ (hij : i < i), False
refine_1₁ : ∀ (hab : b₂ < b₁), False
⊢ False

Tactic:
obtain ⟨_, _, hij⟩ | ⟨_, hab⟩ := hab
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i : α a₁
a₂ : ι
a : α a₂
hji : a₁ < a₂
hij : a₂ < a₁
⊢ False

Tactic:
hij.not_gt hji

Premises used: LT.lt.not_gt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i : α a₁
a₂ : ι
a : α a₂
hji : a₁ < a₂
hij : a₂ < a₁
⊢ False

Tactic:
exact hij.not_gt hji

Premises used: LT.lt.not_gt
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i a : α a₁
hji : a₁ < a₁
hab : a < i
⊢ False

Tactic:
lt_irrefl _ hji

Premises used: lt_irrefl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
i a : α a₁
hji : a₁ < a₁
hab : a < i
⊢ False

Tactic:
exact lt_irrefl _ hji

Premises used: lt_irrefl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hij : i < i
⊢ False

Tactic:
lt_irrefl _ hij

Premises used: lt_irrefl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hij : i < i
⊢ False

Tactic:
exact lt_irrefl _ hij

Premises used: lt_irrefl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hab : b₂ < b₁
⊢ False

Tactic:
hab.not_ge hba

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hba : b₁ ≤ b₂
hab : b₂ < b₁
⊢ False

Tactic:
exact hab.not_ge hba

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
j : α a₁
a₂ : ι
b : α a₂
hij : a₁ < a₂
hba : ¬mk (β := fun (i : ι) ↦ α i) a₂ b ≤ mk (β := fun (i : ι) ↦ α i) a₁ j
⊢ mk (β := fun (i : ι) ↦ α i) a₁ j < mk (β := fun (i : ι) ↦ α i) a₂ b

Tactic:
Lex.left _ _ hij

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
a₁ : ι
j : α a₁
a₂ : ι
b : α a₂
hij : a₁ < a₂
hba : ¬mk (β := fun (i : ι) ↦ α i) a₂ b ≤ mk (β := fun (i : ι) ↦ α i) a₁ j
⊢ mk (β := fun (i : ι) ↦ α i) a₁ j < mk (β := fun (i : ι) ↦ α i) a₂ b

Tactic:
exact Lex.left _ _ hij

Premises used: PSigma.Lex.left
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hab : b₁ ≤ b₂
hba : ¬mk (β := fun (i : ι) ↦ α i) i b₂ ≤ mk (β := fun (i : ι) ↦ α i) i b₁
⊢ mk (β := fun (i : ι) ↦ α i) i b₁ < mk (β := fun (i : ι) ↦ α i) i b₂

Tactic:
Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

Premises used: LE.le.lt_of_not_ge, PSigma.Lex.right
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
i : ι
b₁ b₂ : α i
hab : b₁ ≤ b₂
hba : ¬mk (β := fun (i : ι) ↦ α i) i b₂ ≤ mk (β := fun (i : ι) ↦ α i) i b₁
⊢ mk (β := fun (i : ι) ↦ α i) i b₁ < mk (β := fun (i : ι) ↦ α i) i b₂

Tactic:
exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

Premises used: PSigma.Lex.right
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₂ b₂

Tactic:
(lt_irrefl a₁ <| hlt₁.trans hlt₂).elim

Premises used: lt_irrefl, False.elim, LT.lt.trans
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₂ b₂

Tactic:
exact (lt_irrefl a₁ <| hlt₁.trans hlt₂).elim

Premises used: lt_irrefl, False.elim, LT.lt.trans
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂

Tactic:
(lt_irrefl a₁ hlt₁).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂

Tactic:
exact (lt_irrefl a₁ hlt₁).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : b₁ ≤ b₂
hlt₂ : a₁ < a₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂

Tactic:
(lt_irrefl a₁ hlt₂).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : b₁ ≤ b₂
hlt₂ : a₁ < a₁
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂

Tactic:
exact (lt_irrefl a₁ hlt₂).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : b₁ ≤ b₂
hlt₂ : b₂ ≤ b₁
right right₁ : mk (β := fun (i : ι) ↦ α i) a₁ b₂ = mk (β := fun (i : ι) ↦ α i) a₁ b₂
⊢ mk (β := fun (i : ι) ↦ α i) a₁ b₁ = mk (β := fun (i : ι) ↦ α i) a₁ b₂

Tactic:
rw [hlt₁.antisymm hlt₂]

Premises used: LE.le.antisymm
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (hij : i < j),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
      mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
inr :
  ∀ (b : α i),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b ∨
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
inr₁ :
  ∀ (hji : j < i),
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
      mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain hij | rfl | hji := lt_trichotomy i j

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hij : i < j
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
Or.inl (Lex.left _ _ hij)

Premises used: PSigma.Lex.left, Or.inl
-- Module: Mathlib.Data.PSigma.Order
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → LinearOrder (α i)
i : ι
a : α i
j : ι
b : α j
hij : i < j
⊢ mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b ∨
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
exact Or.inl (Lex.left _ _ hij)

Premises used: PSigma.Lex.left, Or.inl