awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
mp : GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
mpr : rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Tactic:
constructor
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).1 (a₂, b).1 ∧ (a₁, b).2 = (a₂, b).2 ∨ rβ (a₁, b).2 (a₂, b).2 ∧ (a₁, b).1 = (a₂, b).1

Tactic:
Or.inl ⟨h, rfl⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b₁ b₂ : β
h : rβ b₁ b₂
⊢ rα (a, b₁).1 (a, b₂).1 ∧ (a, b₁).2 = (a, b₂).2 ∨ rβ (a, b₁).2 (a, b₂).2 ∧ (a, b₁).1 = (a, b₂).1

Tactic:
Or.inr ⟨h, rfl⟩

Premises used: And.intro, Or.inr, rfl
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b : β
h : rα a₁ a₂
⊢ rα (a₁, b).1 (a₂, b).1 ∧ (a₁, b).2 = (a₂, b).2 ∨ rβ (a₁, b).2 (a₂, b).2 ∧ (a₁, b).1 = (a₂, b).1

Tactic:
exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
mpr : ∀ {x y : α × β}, rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y

Tactic:
revert x y
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).1 (a₂, b₁).1
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

Tactic:
GameAdd.fst h

Premises used: Prod.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ b₂ : β
h : rβ (a₁, b₁).2 (a₁, b₂).2
⊢ GameAdd rα rβ (a₁, b₁) (a₁, b₂)

Tactic:
GameAdd.snd h

Premises used: Prod.GameAdd.snd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ : α
b₁ : β
a₂ : α
h : rα (a₁, b₁).1 (a₂, b₁).1
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₁)

Tactic:
exacts [GameAdd.fst h, GameAdd.snd h]

Premises used: Prod.GameAdd.snd, Prod.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b₁ b₂ : β
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂

Tactic:
gameAdd_iff

Premises used: Prod.gameAdd_iff
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₁ : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) ((a₂, b₂).2, (a₂, b₂).1) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₂ :
  rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
    GameAdd rα rβ (a₁, b₁) (a₂, b₂)
rw₃ :
  rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ∨ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ↔
    rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
rw₄ rw₅ :
  rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ∨ rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ↔
    rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)

Tactic:
rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]

Premises used: Prod.gameAdd_mk_iff, Prod.swap, or_comm
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a₁ a₂ : α
b₁ b₂ : β
⊢ GameAdd rα rβ (a₁, b₁) (a₂, b₂) ↔ GameAdd rβ rα (b₁, a₁) (b₂, a₂)

Tactic:
gameAdd_swap_swap rβ rα (b₁, a₁) (b₂, a₂)

Premises used: Prod.gameAdd_swap_swap, Prod.mk, Prod.swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
⊢ GameAdd rα rβ ≤ Prod.Lex rα rβ

Tactic:
fun _ _ h =>
  h.rec (Prod.Lex.left _ _) (Prod.Lex.right _)

Premises used: Prod.GameAdd.rec
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
h : RProd rα rβ x x_1
a₁ : α
_ : ∀ {b₁ : β} {a₂ : α} {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)
⊢ ∀ {b₁ : β} {a₂ : α} {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
_
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
h : RProd rα rβ x x_1
a₁ : α
b₁ : β
_ : ∀ {a₂ : α} {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)
⊢ ∀ {a₂ : α} {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
_
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
h : RProd rα rβ x x_1
a₁ : α
b₁ : β
a₂ : α
_ : ∀ {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)
⊢ ∀ {b₂ : β} (h₁ : rα a₁ a₂) (h₂ : rβ b₁ b₂), Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
_
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
h : RProd rα rβ x x_1
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hα : rα a₁ a₂
hβ : rβ b₁ b₂
⊢ Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ)

Premises used: Prod.GameAdd.snd, Relation.TransGen.tail, Relation.TransGen.single, Prod.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
h : RProd rα rβ x x_1
a₁ : α
b₁ : β
a₂ : α
b₂ : β
hα : rα a₁ a₂
hβ : rβ b₁ b₂
⊢ Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
exact Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ)

Premises used: Prod.GameAdd.snd, Relation.TransGen.tail, Relation.TransGen.single, Prod.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
intro :
  ∀ (a : α),
    (∀ (y : α), rα y a → Acc rα y) →
      ∀ (iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)) {b : β} (hb : Acc rβ b),
        Acc (Prod.GameAdd rα rβ) (a, b)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction ha generalizing b with | _ a _ iha
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
intro :
  ∀ (b : β) (hb : ∀ (y : β), rβ y b → Acc rβ y) (ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)),
    Acc (Prod.GameAdd rα rβ) (a, b)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction hb with | _ b hb ihb
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
Acc.intro _ fun h => ?_

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
intro : ∀ (h : α × β), Prod.GameAdd rα rβ h (a, b) → Acc (Prod.GameAdd rα rβ) h
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
refine Acc.intro _ fun h => ?_

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
a₁ : α
ra : rα a₁ a
⊢ Acc (Prod.GameAdd rα rβ) (a₁, b)

Tactic:
iha _ ra (Acc.intro b hb)

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
b₁ : β
rb : rβ b₁ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b₁)

Tactic:
ihb _ rb
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β} (hb : Acc rβ b), Acc (Prod.GameAdd rα rβ) (y, b)
b_1 b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
a₁ : α
ra : rα a₁ a
⊢ Acc (Prod.GameAdd rα rβ) (a₁, b)

Tactic:
exacts [iha _ ra (Acc.intro b hb), ihb _ rb]

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
hα : WellFounded rα
hβ : WellFounded rβ
⊢ WellFounded (Prod.GameAdd rα rβ)

Tactic:
⟨fun ⟨a, b⟩ => (hα.apply a).prod_gameAdd (hβ.apply b)⟩

Premises used: WellFounded.apply, Prod.GameAdd, Acc, _private.0.Prod.gameAdd_swap_swap.match_1, WellFounded.intro, Acc.prod_gameAdd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → β → Sort u_3
hα : WellFounded rα
hβ : WellFounded rβ
IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁
a : α
b : β
⊢ recursion (rα := rα) (rβ := rβ) (C := fun (x : α) (x_1 : β) ↦ C x x_1) hα hβ IH a b =
    IH a b fun (a' : α) (b' : β) (x : GameAdd rα rβ (a', b') (a, b)) ↦
      recursion (rα := rα) (rβ := rβ) (C := fun (x : α) (x_1 : β) ↦ C x x_1) hα hβ IH a' b'

Tactic:
WellFounded.fix_eq _ _ _

Premises used: Prod.GameAdd.recursion, WellFounded.fix_eq
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
C : α → β → Prop
⊢ WellFounded rα →
    WellFounded rβ →
      (∀ (a₁ : α) (b₁ : β), (∀ (a₂ : α) (b₂ : β), GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) →
        ∀ (a : α) (b : β), C a b

Tactic:
GameAdd.recursion

Premises used: Prod.GameAdd.recursion
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα_1 : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
rw :
  (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (a₁, b₁) (b₂, a₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (b₂, a₂))

Tactic:
rw [Prod.gameAdd_swap_swap_mk _ _ b₁ b₂ a₁ a₂, Prod.gameAdd_swap_swap_mk _ _ a₁ b₂ b₁ a₂]

Premises used: Prod.gameAdd_swap_swap_mk
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα_1 : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))

Tactic:
simp [or_comm]

Premises used: or_comm
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
fst snd fst_1 snd_1 : α
⊢ GameAdd rα s((fst, snd).1, (fst, snd).2) s((fst_1, snd_1).1, (fst_1, snd_1).2) ↔
    Prod.GameAdd rα rα (fst, snd) (fst_1, snd_1) ∨ Prod.GameAdd rα rα (fst, snd).swap (fst_1, snd_1)

Tactic:
rfl
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b₁ b₂ : α
⊢ GameAdd rα s(a₁, b₁) s(a₂, b₂) ↔ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym2.GameAdd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b₁ b₂ : α
h : Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)
⊢ GameAdd rα s(a₁, b₁) s(a₂, b₂)

Tactic:
gameAdd_iff.2 <| Or.inl <| h

Premises used: Iff.mpr, Or.inl, Sym2.gameAdd_iff
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)

Tactic:
(Prod.GameAdd.fst h).to_sym2

Premises used: Prod.GameAdd.to_sym2, Prod.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a b₁ b₂ : α
h : rα b₁ b₂
⊢ GameAdd rα s(a, b₁) s(a, b₂)

Tactic:
(Prod.GameAdd.snd h).to_sym2

Premises used: Prod.GameAdd.to_sym2, Prod.GameAdd.snd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
rw : GameAdd rα s(b, a₁) s(b, a₂)
⊢ GameAdd rα s(a₁, b) s(b, a₂)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(b, a₂)

Tactic:
GameAdd.snd h

Premises used: Sym2.GameAdd.snd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(b, a₂)

Tactic:
exact GameAdd.snd h

Premises used: Sym2.GameAdd.snd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
rw : GameAdd rα s(a₁, b) s(a₂, b)
⊢ GameAdd rα s(b, a₁) s(a₂, b)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)

Tactic:
GameAdd.fst h

Premises used: Sym2.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)

Tactic:
exact GameAdd.fst h

Premises used: Sym2.GameAdd.fst
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
intro :
  ∀ (a : α),
    (∀ (y : α), rα y a → Acc rα y) →
      ∀ (iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)) {b : α} (hb : Acc rα b),
        Acc (Sym2.GameAdd rα) s(a, b)
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
induction ha generalizing b with | _ a _ iha
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b : α
hb : Acc rα b
intro :
  ∀ (b : α) (hb : ∀ (y : α), rα y b → Acc rα y) (ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)),
    Acc (Sym2.GameAdd rα) s(a, b)
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
induction hb with | _ b hb ihb
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
Acc.intro _ fun s => ?_

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
intro : ∀ (s : Sym2 α), Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
refine Acc.intro _ fun s => ?_

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
s : Sym2 α
intro : ∀ (c d : α), Sym2.GameAdd rα s(c, d) s(a, b) → Acc (Sym2.GameAdd rα) s(c, d)
⊢ Sym2.GameAdd rα s s(a, b) → Acc (Sym2.GameAdd rα) s

Tactic:
induction s with | _ c d
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
intro :
  Prod.GameAdd rα rα (c, d) (a, b) ∨ Prod.GameAdd rα rα (d, c) (a, b) →
    Acc
      ((Sym2.lift₂ :
          (a :
              { f : α → α → α → α → Prop //
                ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
            Sym2 α → Sym2 α → Prop)
        (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
          ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
          (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
      s(c, d)
⊢ (Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯)
      s(c, d) s(a, b) →
    Acc
      ((Sym2.lift₂ :
          (a :
              { f : α → α → α → α → Prop //
                ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
            Sym2 α → Sym2 α → Prop)
        (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
          ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
          (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
      s(c, d)

Tactic:
dsimp
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c a
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(c, b)

Tactic:
iha c rc ⟨b, hb⟩

Premises used: Sym2.GameAdd, Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c a
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(c, b)

Tactic:
exact iha c rc ⟨b, hb⟩

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d b
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(a, d)

Tactic:
ihb d rd

Premises used: Sym2.GameAdd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d b
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(a, d)

Tactic:
exact ihb d rd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
intro :
  Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(d, b)
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(b, d)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(d, b)

Tactic:
iha d rd ⟨b, hb⟩

Premises used: Sym2.GameAdd, Acc.intro