awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
exact Or.inr (Or.inr <| Lex.left _ _ hji)

Premises used: Prod.Lex.left, Or.inr
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
{ exact Or.inr (Or.inr <| Lex.left _ _ hji) }

Premises used: Prod.Lex.left, Or.inr
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Injective f
hg : Injective g
⊢ Injective (map f g)

Tactic:
fun _ _ h ↦ Prod.ext (hf <| congr_arg Prod.fst h) (hg <| congr_arg Prod.snd h)

Premises used: Prod.fst, congr_arg, Prod.ext, Function.Injective, Prod.snd
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Surjective f
hg : Surjective g
⊢ Surjective (map f g)

Tactic:
fun p ↦
  let ⟨x, hx⟩ := hf p.1
  let ⟨y, hy⟩ := hg p.2
  ⟨(x, y), Prod.ext hx hy⟩

Premises used: Exists, Prod.mk, Prod.map, Prod.fst, Prod.ext, Exists.intro, _private.0.Function.Surjective.prodMap.match_1, _private.0.Function.Surjective.prodMap.match_2, Eq, Prod.snd, Function.Surjective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Bijective f
hg : Bijective g
⊢ Bijective (map f g)

Tactic:
⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2⟩

Premises used: Function.Injective.prodMap, Function.Surjective.prodMap, And.right, And.left, And.intro, Function.Bijective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
hf : LeftInverse f₁ f₂
hg : LeftInverse g₁ g₂
a : β × δ
rw : map (f₁ ∘ f₂) (g₁ ∘ g₂) a = a
rw₁ : map id (g₁ ∘ g₂) a = a
rw₂ : map id id a = a
rw₃ : id a = a
rw₄ rw₅ : a = a
⊢ map f₁ g₁ (map f₂ g₂ a) = a

Tactic:
rw [Prod.map_map, hf.comp_eq_id, hg.comp_eq_id, map_id, id]

Premises used: id, Function.LeftInverse.comp_eq_id, Prod.map_id, Prod.map_map
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
⊢ RightInverse f₁ f₂ → RightInverse g₁ g₂ → RightInverse (map f₁ g₁) (map f₂ g₂)

Tactic:
LeftInverse.prodMap

Premises used: Function.LeftInverse.prodMap, Function.RightInverse
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ Involutive f → Involutive g → Involutive (map f g)

Tactic:
LeftInverse.prodMap

Premises used: Function.LeftInverse.prodMap, Function.Involutive
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabit : ∀ (inhabited_h : Inhabited β), a₁ = a₂
⊢ a₁ = a₂

Tactic:
inhabit β
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
a₁ a₂ : α
ha : f a₁ = f a₂
inhabited_h : Inhabited β
⊢ a₁ = a₂

Tactic:
injection
        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha :)

Premises used: Inhabited.default, Prod.mk, congr_arg
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabit : ∀ (inhabited_h : Inhabited α), b₁ = b₂
⊢ b₁ = b₂

Tactic:
inhabit α
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
inhabited_h : Inhabited α
⊢ b₁ = b₂

Tactic:
injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)

Premises used: Inhabited.default, Prod.mk, congr_arg
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabit : ∀ (inhabited_h : Inhabited δ), ∃ (a : α), f a = c
⊢ ∃ (a : α), f a = c

Tactic:
inhabit δ
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
obtain : ∀ (a : α) (b : β) (h : map f g (a, b) = (c, default)), ∃ (a : α), f a = c
⊢ ∃ (a : α), f a = c

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (c, default)

Premises used: Inhabited.default, Prod.mk
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h_1 : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ (a : α), f a = c

Tactic:
⟨a, congr_arg Prod.fst h⟩

Premises used: Prod.fst, congr_arg, Exists.intro
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h_1 : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ (a : α), f a = c

Tactic:
exact ⟨a, congr_arg Prod.fst h⟩
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabit : ∀ (inhabited_h : Inhabited γ), ∃ (a : β), g a = d
⊢ ∃ (a : β), g a = d

Tactic:
inhabit γ
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
obtain : ∀ (a : α) (b : β) (h : map f g (a, b) = (default, d)), ∃ (a : β), g a = d
⊢ ∃ (a : β), g a = d

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (default, d)

Premises used: Inhabited.default, Prod.mk
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h_1 : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ (a : β), g a = d

Tactic:
⟨b, congr_arg Prod.snd h⟩

Premises used: congr_arg, Exists.intro, Prod.snd
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty γ
inst_1 : Nonempty δ
f : α → γ
g : β → δ
h_1 : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ (a : β), g a = d

Tactic:
exact ⟨b, congr_arg Prod.snd h⟩
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
⊢ Nonempty γ

Tactic:
haveI := Nonempty.map f ‹_›
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Nonempty δ

Tactic:
haveI := Nonempty.map g ‹_›
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
this_1 : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
(map_injective.and map_surjective).trans and_and_and_comm

Premises used: Prod.map_surjective, and_and_and_comm, Iff.and, Prod.map_injective, Iff.trans, Function.Bijective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty β
f : α → γ
g : β → δ
this_1 : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
exact (map_injective.and map_surjective).trans and_and_and_comm

Premises used: Prod.map_surjective, and_and_and_comm, Iff.and, Prod.map_injective, Iff.trans
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabit : ∀ (inhabited_h : Inhabited δ), f₁ (f₂ b) = b
⊢ f₁ (f₂ b) = b

Tactic:
inhabit δ
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b

Tactic:
congr_arg Prod.fst (h (b, default))

Premises used: Inhabited.default, Prod.mk, Prod.fst, congr_arg
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
b : β
inhabited_h : Inhabited δ
⊢ f₁ (f₂ b) = b

Tactic:
exact congr_arg Prod.fst (h (b, default))

Premises used: Inhabited.default, Prod.mk, Prod.fst, congr_arg
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabit : ∀ (inhabited_h : Inhabited β), g₁ (g₂ d) = d
⊢ g₁ (g₂ d) = d

Tactic:
inhabit β
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d

Tactic:
congr_arg Prod.snd (h (default, d))

Premises used: Inhabited.default, Prod.mk, congr_arg, Prod.snd
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty β
inst_1 : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
inhabited_h : Inhabited β
⊢ g₁ (g₂ d) = d

Tactic:
exact congr_arg Prod.snd (h (default, d))

Premises used: Inhabited.default, Prod.mk, congr_arg, Prod.snd
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Nonempty α
inst_1 : Nonempty γ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
⊢ RightInverse (map f₁ g₁) (map f₂ g₂) ↔ RightInverse f₁ f₂ ∧ RightInverse g₁ g₂

Tactic:
map_leftInverse

Premises used: Function.RightInverse, Prod.map_leftInverse
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : Nonempty β
f : α → α
g : β → β
⊢ Involutive (map f g) ↔ Involutive f ∧ Involutive g

Tactic:
map_leftInverse

Premises used: Function.Involutive, Prod.map_leftInverse
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LE β
x y : α × β
⊢ LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β)) ↔
    x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2

Tactic:
Prod.lex_def

Premises used: Prod.lex_def
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LE β
x y : α × β
rw :
  LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β)) ↔
    y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 ≤ x.2
rw₁ rw₂ : y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 ≤ x.2 ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 ≤ x.2
⊢ LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β)) ↔
    y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 ≤ x.2

Tactic:
rw [eq_comm, toLex_le_toLex]

Premises used: eq_comm, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
x y : α × β
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β)) ↔
    x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2

Tactic:
Prod.lex_def

Premises used: Prod.lex_def
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
x y : α × β
rw :
  LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β)) ↔
    y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2
rw₁ rw₂ : y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2 ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β)) ↔
    y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 < x.2

Tactic:
rw [eq_comm, toLex_lt_toLex]

Premises used: Prod.Lex.toLex_lt_toLex, eq_comm
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LE β
x y : Lex (α × β)
⊢ x ≤ y ↔
    LT.lt.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∨
      Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∧
        LE.le.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) x).2 ((ofLex : (a : Lex (α × β)) → α × β) y).2

Tactic:
toLex_le_toLex

Premises used: Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
x y : Lex (α × β)
⊢ x < y ↔
    LT.lt.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∨
      Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∧
        LT.lt.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) x).2 ((ofLex : (a : Lex (α × β)) → α × β) y).2

Tactic:
toLex_lt_toLex

Premises used: Prod.Lex.toLex_lt_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
inst_2 : WellFoundedLT α
inst_3 : WellFoundedLT β
⊢ WellFoundedLT (Lex (α × β))

Tactic:
instIsWellFounded

Premises used: Lex, Prod.Lex.instIsWellFounded
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
x₁ x₂ : Lex (α × β)
⊢ x₁ < x₂ ↔ x₁ ≤ x₂ ∧ ¬x₂ ≤ x₁

Tactic:
grind [le_iff, lt_iff, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, Prod.Lex.le_iff, Prod.Lex.lt_iff
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 < c.1
⊢ LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) t).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1

Tactic:
h'.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 < c.1
⊢ LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) t).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1

Tactic:
exact h'.le

Premises used: LT.lt.le
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 = c.1 ∧ t.2 ≤ c.2
⊢ LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) t).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1

Tactic:
h'.1.le

Premises used: Eq.le, And.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LE β
t c : Lex (α × β)
h : t ≤ c
h' : t.1 = c.1 ∧ t.2 ≤ c.2
⊢ LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) t).1 ((ofLex : (a : Lex (α × β)) → α × β) c).1

Tactic:
exact h'.1.le

Premises used: Eq.le, And.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LE β
t c : Lex (α × β)
h : t ≤ c
⊢ t.1 < c.1 ∨ t.1 = c.1 ∧ t.2 ≤ c.2

Tactic:
cases toLex_le_toLex.mp h with
  | inl h' => exact h'.le
  | inr h' => exact h'.1.le

Premises used: Iff.mp, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (β := α) fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1

Tactic:
monotone_fst

Premises used: Prod.Lex.monotone_fst, Monotone
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : Lex (α × β)
h : a ⩿ b
⊢ WCovBy.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) a).1 ((ofLex : (a : Lex (α × β)) → α × β) b).1

Tactic:
⟨monotone_fst _ _ h.1, fun c hac hcb ↦ h.2 (c := toLex (c, a.2)) (.left _ _ hac) (.left _ _ hcb)⟩

Premises used: Prod.Lex.monotone_fst, And.right, And.left, And.intro, WCovBy, Prod.Lex.left, Prod.snd
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
simp :
  ((a₁ < a₂ ∨ a₁ = a₂ ∧ b₁ < b₂) ∧ ∀ (a : α) (b : β), a₁ < a ∨ a₁ = a ∧ b₁ < b → ¬(a < a₂ ∨ a = a₂ ∧ b < b₂)) ↔
    (a₁ = a₂ ∧ b₁ < b₂ ∧ ∀ ⦃c : β⦄, b₁ < c → ¬c < b₂) ∨
      (a₁ < a₂ ∧ ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂) ∧ (∀ (b : β), ¬b₁ < b) ∧ ∀ (b : β), ¬b < b₂
⊢ CovBy (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β)) ↔
    a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂

Tactic:
simp only [CovBy, toLex_lt_toLex, toLex.surjective.forall, Prod.forall, isMax_iff_forall_not_lt,
    isMin_iff_forall_not_lt]

Premises used: Function.Surjective.forall, CovBy, Prod.Lex.toLex_lt_toLex, isMax_iff_forall_not_lt, isMin_iff_forall_not_lt, Prod.forall, Equiv.surjective, toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ < a₂ ∨ a₁ = a₂ ∧ b₁ < b₂) ∧ ∀ (a : α) (b : β), a₁ < a ∨ a₁ = a ∧ b₁ < b → ¬(a < a₂ ∨ a = a₂ ∧ b < b₂)) ↔
    (a₁ = a₂ ∧ b₁ < b₂ ∧ ∀ ⦃c : β⦄, b₁ < c → ¬c < b₂) ∨
      (a₁ < a₂ ∧ ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂) ∧ (∀ (b : β), ¬b₁ < b) ∧ ∀ (b : β), ¬b < b₂

Tactic:
grind
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a b : Lex (α × β)
⊢ a ⋖ b ↔
    Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) a).1 ((ofLex : (a : Lex (α × β)) → α × β) b).1 ∧
        CovBy.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) a).2 ((ofLex : (a : Lex (α × β)) → α × β) b).2 ∨
      CovBy.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) a).1 ((ofLex : (a : Lex (α × β)) → α × β) b).1 ∧
        IsMax.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) a).2 ∧
          IsMin.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) b).2

Tactic:
toLex_covBy_toLex_iff

Premises used: Lex, Prod.Lex.toLex_covBy_toLex_iff
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
simp : x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
⊢ LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β)) ↔
    x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Tactic:
simp only [toLex_le_toLex, lt_iff_le_not_ge, le_antisymm_iff]

Premises used: lt_iff_le_not_ge, le_antisymm_iff, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
mp : x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mpr : x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2
mp₁ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₂ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₃ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₄ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)
mp₅ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1
mp₆ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2
mp₇ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1
mp₈ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁ mpr₂ :
  x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2
mpr₃ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.1 ≤ y.1
mpr₄ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → y.1 ≤ x.1
mpr₅ : x.1 ≤ y.1 → (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2) → ¬(x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1) → x.2 ≤ y.2
mp₉ : x.1 ≤ y.1 → ¬y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2
mp₁₀ mp₁₁ mp₁₂ : x.2 ≤ y.2 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.1 ≤ y.1 → y.1 ≤ x.1 → x.2 ≤ y.2
mpr₆ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₇ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₈ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₉ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₀ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₁ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₂ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₃ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₁₄ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₁₅ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₆ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₁₇ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₈ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₁₉ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₀ : x.1 ≤ y.1 → ¬(x.1 ≤ y.1 ∧ y.1 ≤ x.1) → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₁ : x.1 ≤ y.1 → x.2 ≤ y.2 → ¬¬y.1 ≤ x.1 → x.2 ≤ y.2
mpr₂₂ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬x.1 ≤ y.1 → y.1 ≤ x.1
mpr₂₃ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬y.1 ≤ x.1 → y.1 ≤ x.1
mpr₂₄ mpr₂₅ mpr₂₆ : x.1 ≤ y.1 → x.2 ≤ y.2 → y.1 ≤ x.1 → y.1 ≤ x.1
mpr₂₇ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬x.1 ≤ y.1 → x.2 ≤ y.2
mpr₂₈ : x.1 ≤ y.1 → y.1 ≤ x.1 → ¬y.1 ≤ x.1 → x.2 ≤ y.2
⊢ x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ↔ x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2)

Tactic:
tauto
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
rw : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) x : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) y : Lex (α × β)) ↔
    x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
rw [toLex_lt_toLex]

Premises used: Prod.Lex.toLex_lt_toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : α × β
simp :
  x.1 ≤ y.1 ∧ ¬y.1 ≤ x.1 ∨ (x.1 ≤ y.1 ∧ y.1 ≤ x.1) ∧ x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2 ↔
    x.1 ≤ y.1 ∧ (x.1 ≤ y.1 ∧ y.1 ≤ x.1 → x.2 ≤ y.2 ∧ ¬y.2 ≤ x.2)
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
simp only [lt_iff_le_not_ge, le_antisymm_iff]

Premises used: lt_iff_le_not_ge, le_antisymm_iff
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : Lex (α × β)
⊢ x ≤ y ↔
    LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∧
      (Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 →
        LE.le.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) x).2 ((ofLex : (a : Lex (α × β)) → α × β) y).2)

Tactic:
toLex_le_toLex'

Premises used: Prod.Lex.toLex_le_toLex'
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
x y : Lex (α × β)
⊢ x < y ↔
    LE.le.{u_1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 ∧
      (Eq.{u_1 + 1} (α := α) ((ofLex : (a : Lex (α × β)) → α × β) x).1 ((ofLex : (a : Lex (α × β)) → α × β) y).1 →
        LT.lt.{u_2} (α := β) ((ofLex : (a : Lex (α × β)) → α × β) x).2 ((ofLex : (a : Lex (α × β)) → α × β) y).2)

Tactic:
toLex_lt_toLex'

Premises used: Prod.Lex.toLex_lt_toLex'