awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ Icc a b = piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Fintype.piFinset, rfl
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Icc a b) = ∏ i : ι, #(Icc (a i) (b i))

Tactic:
card_piFinset _

Premises used: Finset.map, Fintype.card_piFinset, Finset.Icc, Fintype.piFinset
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
rw₁ rw₂ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
⊢ #(Ico a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

Premises used: Pi.card_Icc, Finset.card_Ico_eq_card_Icc_sub_one
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
rw₁ rw₂ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1
⊢ #(Ioc a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

Premises used: Pi.card_Icc, Finset.card_Ioc_eq_card_Icc_sub_one
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
rw : #(Icc a b) - 2 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
rw₁ rw₂ : HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2 = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2
⊢ #(Ioo a b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Icc (a i) (b i))) 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Premises used: Pi.card_Icc, Finset.card_Ioo_eq_card_Icc_sub_two
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b_1 b x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Iic (b i)) x ↔ x ≤ b
simp_rw₂ : (∀ (a : ι), x a ∈ Iic (b a)) ↔ x ≤ b
simp_rw₃ : (∀ (a : ι), x a ≤ b a) ↔ x ≤ b
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Iic (b i) : Finset ((a : ι) → α a))) b) x ↔
    x ≤ b

Tactic:
simp_rw [mem_piFinset, mem_Iic, le_def]

Premises used: Fintype.mem_piFinset, Finset.mem_Iic, Pi.le_def
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ #(Iic b) = ∏ i : ι, #(Iic (b i))

Tactic:
card_piFinset _

Premises used: Finset.map, Fintype.card_piFinset, Fintype.piFinset, Finset.Iic
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
rw : #(Iic b) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
rw₁ rw₂ : HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1
⊢ #(Iio b) = HSub.hSub (α := ℕ) (∏ i : ι, #(Iic (b i))) 1

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Premises used: Pi.card_Iic, Finset.card_Iio_eq_card_Iic_sub_one
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a_1 a x : (i : ι) → α i
simp_rw simp_rw₁ : Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Ici (a i)) x ↔ a ≤ x
simp_rw₂ : (∀ (a_2 : ι), x a_2 ∈ Ici (a a_2)) ↔ a ≤ x
simp_rw₃ : (∀ (a_2 : ι), a a_2 ≤ x a_2) ↔ a ≤ x
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Ici (a i) : Finset ((a : ι) → α a))) a) x ↔
    a ≤ x

Tactic:
simp_rw [mem_piFinset, mem_Ici, le_def]

Premises used: Fintype.mem_piFinset, Finset.mem_Ici, Pi.le_def
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ici a) = ∏ i : ι, #(Ici (a i))

Tactic:
card_piFinset _

Premises used: Finset.map, Fintype.card_piFinset, Finset.Ici, Fintype.piFinset
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
rw : #(Ici a) - 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
rw₁ rw₂ : HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1 = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1
⊢ #(Ioi a) = HSub.hSub (α := ℕ) (∏ i : ι, #(Ici (a i))) 1

Tactic:
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]

Premises used: Pi.card_Ici, Finset.card_Ioi_eq_card_Ici_sub_one
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → Lattice (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ uIcc a b = piFinset (δ := α) fun (i : ι) ↦ uIcc (a i) (b i)

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Fintype.piFinset, rfl, Finset.uIcc
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → Lattice (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(uIcc a b) = ∏ i : ι, #(uIcc (a i) (b i))

Tactic:
card_Icc _ _

Premises used: Pi.card_Icc, Finset.uIcc
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
x : α × β
y : β × α
⊢ x.swap = y ↔ x = y.swap

Tactic:
grind
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_5
w : x₁ = x₂ → y₁ = y₂ → P
refl : (w : x₁ = x₁ → y₁ = y₁ → P) → P
⊢ P

Tactic:
cases h
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
P : Sort u_5
w : x₁ = x₁ → y₁ = y₁ → P
⊢ P

Tactic:
exact w rfl rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → β → Prop
⊢ (∀ (x : α × β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a b

Tactic:
Prod.forall

Premises used: Prod.forall
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → β → Prop
⊢ (∃ (x : α × β), p x.fst x.snd) ↔ ∃ (a : α), ∃ (b : β), p a b

Tactic:
Prod.exists

Premises used: Prod.exists
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
⊢ Eq.{u_2 + 1} (α := β → β) (snd ∘ mk x) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
⊢ fst ∘ mk x = Function.const β x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
p : α × β
⊢ map f g p = (f p.fst, g p.snd)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
⊢ fst ∘ map f g = f ∘ fst

Tactic:
funext <| map_fst f g

Premises used: funext, Prod.map_fst
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
⊢ snd ∘ map f g = g ∘ snd

Tactic:
funext <| map_snd f g

Premises used: Prod.map_snd, funext
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂

Tactic:
simpa only [true_and, Prod.mk_inj, eq_self_iff_true] using h

Premises used: Prod.mk_inj, eq_self_iff_true, true_and
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : Eq (α := α × β) ((fun (a : α) ↦ (a, b)) b₁) ((fun (a : α) ↦ (a, b)) b₂)
⊢ b₁ = b₂

Tactic:
simpa only [and_true, eq_self_iff_true, mk_inj] using h

Premises used: and_true, Prod.mk_inj, eq_self_iff_true
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
⊢ (a, b₁) = (a, b₂) ↔ b₁ = b₂

Tactic:
(mk_right_injective _).eq_iff

Premises used: Function.Injective.eq_iff, Prod.mk_right_injective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
a₁ a₂ : α
b : β
⊢ (a₁, b) = (a₂, b) ↔ a₁ = a₂

Tactic:
(mk_left_injective _).eq_iff

Premises used: Function.Injective.eq_iff, Prod.mk_left_injective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
⊢ map f g = fun (p : α × β) ↦ (f p.fst, g p.snd)

Tactic:
funext fun p ↦ Prod.ext (map_fst f g p) (map_snd f g p)

Premises used: Prod.map_snd, funext, Prod.ext, Prod.map_fst
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := (p : α × β) → α × β) (fun (p : α × β) ↦ (p.fst, p.snd)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
zero : (map f g)^[0] = map f^[0] g^[0]
succ : ∀ (n : ℕ), (map f g)^[n] = map f^[n] g^[n] → (map f g)^[n + 1] = map f^[n + 1] g^[n + 1]
⊢ (map f g)^[n] = map f^[n] g^[n]

Tactic:
induction n
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ (map f g)^[0] = map f^[0] g^[0]

Tactic:
simp [*, Prod.map_comp_map]

Premises used: Prod.map_comp_map
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
h : (map f g)^[n] = map f^[n] g^[n]
⊢ (map f g)^[n + 1] = map f^[n + 1] g^[n + 1]

Tactic:
simp [*, Prod.map_comp_map]

Premises used: Prod.map_comp_map
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
h : Nonempty β
⊢ Function.Surjective (α := α × β) fst

Tactic:
fun x ↦ h.elim fun y ↦ ⟨⟨x, y⟩, rfl⟩

Premises used: Nonempty.elim, Prod.mk, Exists.intro, Function.Surjective, rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
h : Nonempty α
⊢ Function.Surjective (α := α × β) snd

Tactic:
fun y ↦ h.elim fun x ↦ ⟨⟨x, y⟩, rfl⟩

Premises used: Nonempty.elim, Prod.mk, Exists.intro, Function.Surjective, rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Subsingleton β
⊢ Function.Injective (α := α × β) fst

Tactic:
fun _ _ h ↦ Prod.ext h (Subsingleton.elim _ _)

Premises used: Prod.ext, Function.Injective, Subsingleton.elim, Prod.snd
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Subsingleton α
⊢ Function.Injective (α := α × β) snd

Tactic:
fun _ _ h ↦ Prod.ext (Subsingleton.elim _ _) h

Premises used: Prod.fst, Prod.ext, Function.Injective, Subsingleton.elim
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Function.LeftInverse (α := β × α) swap swap

Tactic:
swap_swap

Premises used: Function.LeftInverse, Prod.swap_swap
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Function.RightInverse (α := β × α) swap swap

Tactic:
swap_swap

Premises used: Function.LeftInverse, Prod.swap_swap, Function.RightInverse
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Function.Injective (α := α × β) swap

Tactic:
swap_leftInverse.injective

Premises used: Function.LeftInverse.injective, Prod.swap_leftInverse
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Function.Surjective (α := α × β) swap

Tactic:
swap_leftInverse.surjective

Premises used: Prod.swap_leftInverse, Function.LeftInverse.surjective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
⊢ Function.Bijective (α := α × β) swap

Tactic:
⟨swap_injective, swap_surjective⟩

Premises used: And.intro, Function.Bijective, Prod.swap_injective, Prod.swap_surjective
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
⊢ Function.Semiconj swap (map f g) (map g f)

Tactic:
Function.semiconj_iff_comp_eq.2 (map_comp_swap g f).symm

Premises used: Iff.mpr, Prod.map_comp_swap, Eq.symm, Function.semiconj_iff_comp_eq
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
p₁ : α
p₂ : β
q₁ : α
q₂ : β
⊢ (p₁, p₂) = (q₁, q₂) ↔ (p₁, p₂).fst = (q₁, q₂).fst ∧ (p₁, p₂).snd = (q₁, q₂).snd

Tactic:
simp
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
x : α
⊢ (a, b).fst = x ↔ (a, b) = (x, (a, b).snd)

Tactic:
simp
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
a : α
b x : β
⊢ (a, b).snd = x ↔ (a, b) = ((a, b).fst, x)

Tactic:
simp
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
x y : α × β
⊢ Prod.Lex r s x y ↔ r x.fst y.fst ∨ x.fst = y.fst ∧ s x.snd y.snd

Tactic:
lex_def

Premises used: Prod.lex_def
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
⊢ Std.Refl (Prod.Lex r s)

Tactic:
⟨Lex.refl_left _ _⟩

Premises used: Std.Refl.mk, Prod.Lex.refl_left
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl s
⊢ Std.Refl (Prod.Lex r s)

Tactic:
⟨Lex.refl_right _ _⟩

Premises used: Prod.Lex.refl_right, Std.Refl.mk
-- 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.Irrefl r
inst_1 : Std.Irrefl s
i : α
a : β
h : r i i
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- 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.Irrefl r
inst_1 : Std.Irrefl s
i : α
a : β
h : r i i
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- 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.Irrefl r
inst_1 : Std.Irrefl s
i : α
a : β
h : s a a
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- 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.Irrefl r
inst_1 : Std.Irrefl s
i : α
a : β
h : s a a
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
⊢ IsTrans (α × β) (Prod.Lex r s)

Tactic:
⟨fun _ _ _ ↦ Lex.trans⟩

Premises used: IsTrans.mk, Prod.Lex.trans
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : IsStrictOrder α r
inst_1 : Std.Antisymm s
⊢ Std.Antisymm (Prod.Lex r s)

Tactic:
⟨fun x₁ x₂ h₁₂ h₂₁ ↦
    match x₁, x₂, h₁₂, h₂₁ with
    | (a, _), (_, _), .left  _ _ hr₁, .left  _ _ hr₂ => (irrefl a (_root_.trans hr₁ hr₂)).elim
    | (_, _), (_, _), .left  _ _ hr₁, .right _ _     => (irrefl _ hr₁).elim
    | (_, _), (_, _), .right _ _,     .left  _ _ hr₂ => (irrefl _ hr₂).elim
    | (_, _), (_, _), .right _ hs₁,   .right _ hs₂   => antisymm hs₁ hs₂ ▸ rfl⟩

Premises used: trans, irrefl, False.elim, Eq.rec, _private.0.Prod.instAntisymmLexOfIsStrictOrder.match_1, antisymm, Std.Antisymm.mk, Eq, rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Total r
⊢ Std.Total (Prod.Lex r s)

Tactic:
⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ ↦ (Std.Total.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩

Premises used: _private.0.Prod.mk.eta.match_1, Prod.Lex, Prod.mk, Std.Total.total, Or, Std.Total.mk, Or.imp, Prod.Lex.left
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
inr : Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)
inr₁ : ∀ (hji : r j i), Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Premises used: trichotomous_of, rfl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

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

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

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

Premises used: Or.inl
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

Tactic:
(total_of s a b).imp (.right _) (.right _)

Premises used: total_of, Prod.Lex.right, Or.imp
-- Module: Mathlib.Data.Prod.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

Tactic:
exact (total_of s a b).imp (.right _) (.right _)

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

Tactic:
Or.inr (.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_1 : α → α → Prop
s_1 : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Total s
x_1 x_2 : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
exact Or.inr (.left _ _ hji)

Premises used: 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 : β
this : ∀ (j : α) (b : β), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
⊢ ∀ {b : α × β}, Prod.Lex r s (i, a) b ∨ (i, a) = b ∨ Prod.Lex r s b (i, a)

Tactic:
⟨j, b⟩
-- 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 : β
inl : ∀ (hij : r i j), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
inr : Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)
inr₁ : ∀ (hji : r j i), Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Premises used: trichotomous_of, rfl
-- 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 : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

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

Premises used: Or.inl, Prod.Lex.left
-- 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 : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

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

Premises used: Or.inl, Prod.Lex.left
-- 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 : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

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

Premises used: Or.inl, Prod.Lex.left
-- 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 b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

Tactic:
(trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)

Premises used: Or.imp3, congr_arg, Prod.Lex.right, trichotomous_of
-- 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 b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

Tactic:
exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _)

Premises used: Or.imp3, congr_arg, Prod.Lex.right, trichotomous_of
-- 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 b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

Tactic:
{ exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _) }

Premises used: Or.imp3, congr_arg, Prod.Lex.right, trichotomous_of
-- 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:
Or.inr (Or.inr <| Lex.left _ _ hji)

Premises used: Prod.Lex.left, Or.inr