awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
⊢ Monotone (α := α × β) (β := Lex (α × β)) (⇑toLex : (a : α × β) → Lex (α × β))

Tactic:
fun _x _y hxy ↦ toLex_le_toLex'.2 ⟨hxy.1, fun _ ↦ hxy.2⟩

Premises used: Iff.mpr, Prod.Lex.toLex_le_toLex', Monotone, And.right, And.left, And.intro
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ a₁ = a₂ ∨ (a₁, b₁).1 < (a₂, b₂).1

Tactic:
h.le.1.eq_or_lt

Premises used: LE.le.eq_or_lt, LT.lt.le, And.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
inl :
  ∀ (h : (a₁, b₁) < (a₁, b₂)),
    LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₂) : Lex (α × β))
inr :
  ∀ (ha : (a₁, b₁).1 < (a₂, b₂).1),
    LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))

Tactic:
obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt

Premises used: LE.le.eq_or_lt, LT.lt.le, And.left, rfl
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₂) : Lex (α × β))

Tactic:
right _ (Prod.mk_lt_mk_iff_right.1 h)

Premises used: Prod.Lex.right, Prod.mk_lt_mk_iff_right, Iff.mp
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₂) : Lex (α × β))

Tactic:
exact right _ (Prod.mk_lt_mk_iff_right.1 h)

Premises used: Prod.Lex.right, Prod.mk_lt_mk_iff_right, Iff.mp
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))

Tactic:
left _ _ ha

Premises used: Prod.Lex.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a₁, b₁) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a₂, b₂) : Lex (α × β))

Tactic:
exact left _ _ ha

Premises used: Prod.Lex.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Ord α
inst_1 : Ord β
⊢ Eq (α := Lex (α × β) → Lex (α × β) → Ordering) compare
    (compareLex (compareOn (β := α) fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1)
      (compareOn (β := β) fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2))

Tactic:
rfl

Premises used: Lex, Ordering.then, rfl
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Ord α
inst_1 : Ord β
⊢ Eq (α := Ord (α × β)) lexOrd instOrdLexProd

Tactic:
rfl

Premises used: Lex, rfl
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
oα : Ord α
oβ : Ord β
⊢ oα.lex oβ = instOrdLexProd

Tactic:
rfl

Premises used: Lex, rfl
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Ord α
inst_1 : Ord β
inst_2 : Std.OrientedOrd α
inst_3 : Std.OrientedOrd β
⊢ Std.OrientedOrd (Lex (α × β))

Tactic:
inferInstanceAs (Std.OrientedCmp (compareLex _ _))

Premises used: _private.0.Prod.Lex.instOrientedOrdLex._proof_1
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Ord α
inst_1 : Ord β
inst_2 : Std.TransOrd α
inst_3 : Std.TransOrd β
⊢ Std.TransOrd (Lex (α × β))

Tactic:
inferInstanceAs (Std.TransCmp (compareLex _ _))

Premises used: _private.0.Prod.Lex.instTransOrdLex._proof_1
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
have : ∀ (this : DecidableLT (Lex (α × β))), compare a b = compareOfLessAndEq a b
⊢ compare a b = compareOfLessAndEq a b

Tactic:
have : DecidableLT (α ×ₗ β) := Prod.Lex.decidable _ _
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ ∀ {a b : Lex (α × β)}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]

Premises used: Prod.Lex.compare_def, compareLex, compareOn, Ordering.then_eq_eq
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ Std.LawfulBEqOrd (Lex (α × β))

Tactic:
have : Std.LawfulBEqOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]⟩
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this_1 : DecidableLT (Lex (α × β))
this : Std.LawfulBEqOrd (Lex (α × β))
⊢ ∀ {x y : Lex (α × β)}, compare x y = Ordering.lt ↔ x < y

Tactic:
simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
        compare_lt_iff_lt]

Premises used: Prod.Lex.compare_def, compareLex, Prod.Lex.toLex_lt_toLex, Ordering.then_eq_lt, compareOn, compare_lt_iff_lt
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this_1 : DecidableLT (Lex (α × β))
this : Std.LawfulBEqOrd (Lex (α × β))
⊢ Std.LawfulLTOrd (Lex (α × β))

Tactic:
have : Std.LawfulLTOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
        compare_lt_iff_lt]⟩
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this_1 : DecidableLT (Lex (α × β))
this_2 : Std.LawfulBEqOrd (Lex (α × β))
this : Std.LawfulLTOrd (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b

Tactic:
Std.LawfulLTCmp.eq_compareOfLessAndEq (cmp := compare) a b

Premises used: Std.LawfulLTCmp.eq_compareOfLessAndEq
-- Module: Mathlib.Data.Prod.Lex
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : LinearOrder β
a b : Lex (α × β)
this_1 : DecidableLT (Lex (α × β))
this_2 : Std.LawfulBEqOrd (Lex (α × β))
this : Std.LawfulLTOrd (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b

Tactic:
convert! Std.LawfulLTCmp.eq_compareOfLessAndEq (cmp := compare) a b

Premises used: Std.LawfulLTCmp.eq_compareOfLessAndEq
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
left : ∀ (c : α) (h₁ : a₁ < c) (h₂ : c < a₂), ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)
⊢ ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)

Tactic:
obtain ⟨c, h₁, h₂⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
c : α
h₁ : a₁ < c
h₂ : c < a₂
⊢ ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)

Tactic:
⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩

Premises used: Prod.mk, And.intro, Exists.intro, Prod.Lex.left
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
c : α
h₁ : a₁ < c
h₂ : c < a₂
⊢ ∃ (a : Lex (α × β)), (a₁, b₁) < a ∧ a < (a₂, b₂)

Tactic:
exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
right : ∀ (c : β) (h₁ : b₁ < c) (h₂ : c < b₂), ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)
⊢ ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)

Tactic:
obtain ⟨c, h₁, h₂⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
c : β
h₁ : b₁ < c
h₂ : c < b₂
⊢ ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)

Tactic:
⟨(a, c), right _ h₁, right _ h₂⟩

Premises used: Prod.mk, Prod.Lex.right, And.intro, Exists.intro
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a : α
b₁ b₂ : β
h : b₁ < b₂
c : β
h₁ : b₁ < c
h₂ : c < b₂
⊢ ∃ (a_1 : Lex (α × β)), (a, b₁) < a_1 ∧ a_1 < (a, b₂)

Tactic:
exact ⟨(a, c), right _ h₁, right _ h₂⟩
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
rw : ∀ (a : α) (b : β), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
⊢ ∀ (a : Lex (α × β)), ∃ (b : Lex (α × β)), a < b

Tactic:
rw [Lex.forall, Prod.forall]

Premises used: Lex.forall, Prod.forall
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
a : α
b : β
obtain : ∀ (c : α) (h : a < c), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1

Tactic:
obtain ⟨c, h⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
a : α
b : β
c : α
h : a < c
h₁ :
  LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (c, b) : Lex (α × β))
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1

Tactic:
use toLex (c, b)

Premises used: Prod.mk, DFunLike.coe, toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (c, b) : Lex (α × β))

Tactic:
simpa [lt_iff]

Premises used: Prod.Lex.lt_iff
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
rw : ∀ (a : α) (b : β), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
⊢ ∀ (a : Lex (α × β)), ∃ (b : Lex (α × β)), a < b

Tactic:
rw [Lex.forall, Prod.forall]

Premises used: Lex.forall, Prod.forall
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
a : α
b : β
obtain : ∀ (c : β) (h : b < c), ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1

Tactic:
obtain ⟨c, h⟩ := exists_gt b

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
a : α
b c : β
h : b < c
h₁ :
  LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a, c) : Lex (α × β))
⊢ ∃ (b_1 : Lex (α × β)), (toLex : (a : α × β) → Lex (α × β)) (a, b) < b_1

Tactic:
use toLex (a, c)

Premises used: Prod.mk, DFunLike.coe, toLex
-- Module: Mathlib.Data.Prod.Lex
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ LT.lt (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a, c) : Lex (α × β))

Tactic:
simpa [lt_iff]

Premises used: Prod.Lex.lt_iff
-- Module: Mathlib.Data.Prod.PProd
Goal:
α_1 : Sort u_1
β_1 : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_7
w : x₁ = x₂ → y₁ = y₂ → P
refl : (w : x₁ = x₁ → y₁ = y₁ → P) → P
⊢ P

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

Tactic:
exact w rfl rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.PProd
Goal:
α : Sort u_1
β : Sort u_2
p : α ×' β
⊢ ⟨p.fst, p.snd⟩ = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.PProd
Goal:
α : Sort u_1
β : Sort u_2
p : α ×' β → Prop
⊢ (∀ (x : α ×' β), p x) ↔ ∀ (a : α) (b : β), p ⟨a, b⟩

Tactic:
⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩

Premises used: _private.0.PProd.forall.match_1, PProd.mk, Iff.intro
-- Module: Mathlib.Data.Prod.PProd
Goal:
α : Sort u_1
β : Sort u_2
p : α ×' β → Prop
⊢ (∃ (x : α ×' β), p x) ↔ ∃ (a : α), ∃ (b : β), p ⟨a, b⟩

Tactic:
⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

Premises used: PProd.mk, Exists, Iff.intro, Exists.intro, _private.0.PProd.exists.match_1, _private.0.PProd.exists.match_2
-- Module: Mathlib.Data.Prod.PProd
Goal:
α : Sort u_1
β : Sort u_2
p : α → β → Prop
⊢ (∀ (x : α ×' β), p x.fst x.snd) ↔ ∀ (a : α) (b : β), p a b

Tactic:
PProd.forall

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

Tactic:
PProd.exists

Premises used: PProd.exists
-- Module: Mathlib.Data.Prod.PProd
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → β
g : γ → δ
hf : Injective f
hg : Injective g
⊢ Injective (β := β ×' δ) fun (x : α ×' γ) ↦ ⟨f x.fst, g x.snd⟩

Tactic:
fun _ _ h ↦
  have A := congr_arg PProd.fst h
  have B := congr_arg PProd.snd h
  congr_arg₂ PProd.mk (hf A) (hg B)

Premises used: PProd.mk, PProd.fst, PProd.snd, congr_arg, Function.Injective, congr_arg₂
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
f : (i : ι) → α i
⊢ (TProd.mk (α := α) (i :: l) f).1 = f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
f : (i : ι) → α i
⊢ (TProd.mk (α := α) (i :: l) f).2 = TProd.mk (α := α) l f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i_1 j_1 : ι
l : List ι
inst : DecidableEq ι
i : ι
is : List ι
v : TProd α (i :: is)
j : ι
hj : j ∈ i :: is
hji : j = i
subst : (v : TProd α (j :: is)) → (hj : j ∈ j :: is) → α j
⊢ α j

Tactic:
subst hji
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i j_1 : ι
l : List ι
inst : DecidableEq ι
is : List ι
j : ι
v : TProd α (j :: is)
hj : j ∈ j :: is
⊢ α j

Tactic:
exact v.1

Premises used: Prod.fst
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
inst : DecidableEq ι
v : TProd α (i :: l)
⊢ v.elim (α := α) ⋯ = v.1

Tactic:
simp [TProd.elim]

Premises used: List.TProd.elim
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst : DecidableEq ι
hj : j ∈ i :: l
hji : j ≠ i
v : TProd α (i :: l)
⊢ v.elim (α := α) hj = TProd.elim (α := α) v.2 ⋯

Tactic:
simp [TProd.elim, hji]

Premises used: List.TProd.elim
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
hji : j ≠ i
⊢ v.elim (α := α) ⋯ = TProd.elim (α := α) v.2 hj

Tactic:
apply elim_of_ne

Premises used: List.TProd.elim_of_ne
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
j : ι
l : List ι
inst : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False

Tactic:
hl.notMem hj

Premises used: List.Nodup.notMem
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
j : ι
l : List ι
inst : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False

Tactic:
exact hl.notMem hj

Premises used: List.Nodup.notMem
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
pos : ∀ (hji : j = i), (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
neg : ∀ (hji : ¬j = i), (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j

Tactic:
by_cases hji : j = i
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
pos : ∀ (hj : j ∈ j :: is), (TProd.mk (α := α) (j :: is) f).elim (α := α) hj = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j

Tactic:
subst hji
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ (TProd.mk (α := α) (j :: is) f).elim (α := α) hj = f j

Tactic:
simp
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
neg : TProd.elim (α := α) (TProd.mk (α := α) (i :: is) f).2 ⋯ = f j
neg₁ : (TProd.mk (α := α) is f).elim (α := α) ⋯ = f j
neg₂ neg₃ : f j = f j
⊢ (TProd.mk (α := α) (i :: is) f).elim (α := α) hj = f j

Tactic:
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

Premises used: List.TProd.snd_mk, List.TProd.elim_of_ne
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
fst : v.1 = w.1
snd : v.2 = w.2
⊢ v = w

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
fst : v.elim (α := α) ⋯ = w.1
fst₁ : w.elim (α := α) ⋯ = w.1
fst₂ fst₃ : w.1 = w.1
⊢ v.1 = w.1

Tactic:
rw [← elim_self v, hvw, elim_self]

Premises used: List.TProd.elim_self
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
⊢ v.2 = w.2

Tactic:
ext (nodup_cons.mp hl).2 fun j hj => ?_

Premises used: List.nodup_cons, And.right, Iff.mp
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
snd : ∀ (j : ι) (hj : j ∈ is), TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj
⊢ v.2 = w.2

Tactic:
refine ext (nodup_cons.mp hl).2 fun j hj => ?_

Premises used: List.nodup_cons, And.right, Iff.mp
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
inst : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim (α := α) hi = w.elim (α := α) hi
j : ι
hj : j ∈ is
snd : v.elim (α := α) ⋯ = TProd.elim (α := α) w.2 hj
snd₁ : w.elim (α := α) ⋯ = TProd.elim (α := α) w.2 hj
snd₂ : TProd.elim (α := α) w.2 hj = TProd.elim (α := α) w.2 hj
snd₃ : j ∈ is
snd₄ : TProd.elim (α := α) w.2 hj = TProd.elim (α := α) w.2 hj
snd₅ : j ∈ is
⊢ TProd.elim (α := α) v.2 hj = TProd.elim (α := α) w.2 hj

Tactic:
rw [← elim_of_mem hl, hvw, elim_of_mem hl]

Premises used: List.TProd.elim_of_mem
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
l : List ι
inst : DecidableEq ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
v : TProd α l
i : ι
hi : i ∈ l
⊢ (TProd.mk (α := α) l (TProd.elim' (α := α) h v)).elim (α := α) hi = v.elim (α := α) hi

Tactic:
simp [elim_mk]

Premises used: List.TProd.elim_mk
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
t : (i : ι) → Set (α i)
⊢ preimage (β := TProd α []) (TProd.mk (α := α) []) (Set.tprod (α := α) [] t) =
    pi (α := α) {i : ι | Membership.mem (γ := List ι) [] i} t

Tactic:
simp [Set.tprod]

Premises used: Set.tprod
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
h :
  ∀ (f : (i : ι) → α i),
    f ∈ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t ↔ f ∈ pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t
⊢ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t = pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t

Tactic:
ext f
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
change : f ∈ TProd.mk (α := α) l ⁻¹' Set.tprod (α := α) l t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t
⊢ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i

Tactic:
change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t

Premises used: Set.tprod, setOf, Membership.mem, Set.pi, List.TProd.mk
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
rw rw₁ : f ∈ pi (α := α) {i : ι | i ∈ l} t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t
⊢ f ∈ TProd.mk (α := α) l ⁻¹' Set.tprod (α := α) l t ↔ f ∈ pi (α := α) {x : ι | x ∈ l} t

Tactic:
rw [mk_preimage_tprod l t]
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i

Tactic:
have h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i : ι, i ∈ l → f i ∈ t i := by
      change f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ { x | x ∈ l }.pi t
      rw [mk_preimage_tprod l t]
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
h₁ :
  f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔
    ∀ (i_1 : ι), Membership.mem (γ := Set ι) {i_2 : ι | i_2 ∈ i :: l} i_1 → f i_1 ∈ t i_1
⊢ f ∈ TProd.mk (α := α) (i :: l) ⁻¹' Set.tprod (α := α) (i :: l) t ↔ f ∈ pi (α := α) {i_1 : ι | i_1 ∈ i :: l} t

Tactic:
rw [Set.tprod, TProd.mk, mem_preimage, mem_pi, prodMk_mem_set_prod_eq]

Premises used: Set.tprod, Set.prodMk_mem_set_prod_eq, Set.mem_pi, List.TProd.mk, Set.mem_preimage
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
h₁ : f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
⊢ f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔
    ∀ (i_1 : ι), Membership.mem (γ := Set ι) {i_2 : ι | i_2 ∈ i :: l} i_1 → f i_1 ∈ t i_1

Tactic:
simp_rw [mem_setOf_eq, mem_cons]

Premises used: Set.mem_setOf_eq, List.mem_cons
-- Module: Mathlib.Data.Prod.TProd
Goal:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
h₁ : f i ∈ t i → (TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (a : ι), a ∈ l → f a ∈ t a)
⊢ f i ∈ t i ∧ TProd.mk (α := α) l f ∈ Set.tprod (α := α) l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1

Tactic:
rw [forall_eq_or_imp, and_congr_right_iff]

Premises used: and_congr_right_iff, forall_eq_or_imp