awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ (f : Π₀ (i : ι), ↥(S i)),
      (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) ↦ (⇑(S x).subtype : (a : ↥(S x)) → γ)) = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
x : γ
⊢ Membership.mem (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i) x ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ)
          (filter (β := fun (i : ι) ↦ ↥(S i)) p f) =
        x

Tactic:
SetLike.ext_iff.mp (AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom p S) x

Premises used: Set.Mem, setOf, SetLike.ext_iff, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, Iff.mp, Set.range, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hs : s i ((x : (a : ι) → α a) i) (if i ∈ p then (x₁ : (a : ι) → α a) i else (x₂ : (a : ι) → α a) i)
pos :
  ∀ (hp : i ∈ p) (hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)),
    ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
      InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
        (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x
neg :
  ∀ (hp : i ∉ p) (hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)),
    ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
      InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
        (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x
⊢ ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
    InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
      (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x

Tactic:
split_ifs at hs with hp
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
⊢ ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
    InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
      (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x

Tactic:
⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩

Premises used: setOf, Prod.mk, And.intro, Exists.intro, DFinsupp.piecewise, Prod.GameAdd.fst
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos : ∀ (j : ι) (hj : r j i), (x₁.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₁ : (a : ι) → α a) j
pos₁ : (fun {i : ι} ↦ s i) ((x₁.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos₂ :
  (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1)
      ({j : ι | r j i → j ∈ p}, x₁.piecewise (β := α) x {j : ι | r j i}, x₂) =
    x
⊢ ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
    InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
      (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x

Tactic:
refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
hj : r j i
pos : (if r j i then (x₁ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₁ : (a : ι) → α a) j
⊢ (x₁.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₁ : (a : ι) → α a) j

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos : s i (if r i i then (x₁ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
⊢ (fun {i : ι} ↦ s i) ((x₁.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos : (x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} = x
⊢ (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1)
      ({j : ι | r j i → j ∈ p}, x₁.piecewise (β := α) x {j : ι | r j i}, x₂) =
    x

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
hj : r j i
⊢ (if r j i then (x₁ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₁ : (a : ι) → α a) j

Tactic:
simp only [if_pos hj]

Premises used: if_pos
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos : ∀ (hi : r i i), s i ((x₁ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
neg : ∀ (hi : ¬r i i), s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
⊢ s i (if r i i then (x₁ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)

Tactic:
split_ifs with hi
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
hi : r i i
pos :
  ∀ (hs : s i (if i ∈ p then (x₁ : (a : ι) → α a) i else (x₂ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)) (hi : r i i),
    s i ((x₁ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hs : s i ((x₁ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)) (hi : r i i),
    s i ((x₁ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
⊢ s i ((x₁ : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)

Tactic:
rwa [hr i hi, if_pos hp] at hs

Premises used: if_pos
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
hi : ¬r i i
⊢ s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)

Tactic:
assumption
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
pos :
  ∀ (j : ι),
    ((x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} : (a : ι) → α a) j =
      (x : (a : ι) → α a) j
⊢ (x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} = x

Tactic:
ext1 j
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
pos :
  (if r j i → j ∈ p then if r j i then (x₁ : (a : ι) → α a) j else (x : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j
⊢ ((x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} : (a : ι) → α a) j =
    (x : (a : ι) → α a) j

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
pos : ∀ (h₁ : r j i → j ∈ p) (h₂ : r j i), (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
neg : ∀ (h₁ : r j i → j ∈ p) (h₂ : ¬r j i), (x : (a : ι) → α a) j = (x : (a : ι) → α a) j
neg₁ : ∀ (h₁ : ¬(r j i → j ∈ p)), (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
⊢ (if r j i → j ∈ p then if r j i then (x₁ : (a : ι) → α a) j else (x : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ (x : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ (x : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
try rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
pos : (x₁ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
pos₁ pos₂ : (x₁ : (a : ι) → α a) j = (x₁ : (a : ι) → α a) j
⊢ (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rw [hr j h₂, if_pos (h₁ h₂)]

Premises used: if_pos
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ r j i ∧ j ∉ p

Tactic:
rw [Classical.not_imp] at h₁

Premises used: Classical.not_imp
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∈ p
hs : s i ((x : (a : ι) → α a) i) ((x₁ : (a : ι) → α a) i)
j : ι
h₁ : r j i ∧ j ∉ p
neg : (x₂ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
neg₁ neg₂ : (x₂ : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j
⊢ (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rw [hr j h₁.1, if_neg h₁.2]

Premises used: And.right, And.left, if_neg
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
⊢ ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
    InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
      (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x

Tactic:
⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩

Premises used: setOf, Membership.mem, Prod.mk, Prod.GameAdd.snd, And, And.intro, Exists.intro, DFinsupp.piecewise
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg : ∀ (j : ι) (hj : r j i), (x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j
neg₁ : (fun {i : ι} ↦ s i) ((x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg₂ :
  (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1)
      ({j : ι | r j i ∧ j ∈ p}, x₁, x₂.piecewise (β := α) x {j : ι | r j i}) =
    x
⊢ ∃ (a' : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i),
    InvImage (GameAdd (DFinsupp.Lex (α := α) r s) (DFinsupp.Lex (α := α) r s)) snd a' (p, x₁, x₂) ∧
      (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1) a' = x

Tactic:
refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
hj : r j i
neg : (if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₂ : (a : ι) → α a) j
⊢ (x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg : s i (if r i i then (x₂ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
⊢ (fun {i : ι} ↦ s i) ((x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg : x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} = x
⊢ (fun (x : Set ι × (Π₀ (i : ι), α i) × Π₀ (i : ι), α i) ↦ x.2.1.piecewise (β := α) x.2.2 x.1)
      ({j : ι | r j i ∧ j ∈ p}, x₁, x₂.piecewise (β := α) x {j : ι | r j i}) =
    x

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
hj : r j i
⊢ (if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₂ : (a : ι) → α a) j

Tactic:
if_pos hj

Premises used: if_pos
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
hj : r j i
⊢ (if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₂ : (a : ι) → α a) j

Tactic:
exact if_pos hj

Premises used: if_pos
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
pos : ∀ (hi : r i i), s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg : ∀ (hi : ¬r i i), s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
⊢ s i (if r i i then (x₂ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)

Tactic:
split_ifs with hi
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
hi : r i i
pos :
  ∀ (hs : s i (if i ∈ p then (x₁ : (a : ι) → α a) i else (x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)) (hi : r i i),
    s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hs : s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)) (hi : r i i),
    s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
⊢ s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)

Tactic:
rwa [hr i hi, if_neg hp] at hs

Premises used: if_neg
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
hi : ¬r i i
⊢ s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)

Tactic:
assumption
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
neg :
  ∀ (j : ι),
    (x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} : (a : ι) → α a) j =
      (x : (a : ι) → α a) j
⊢ x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} = x

Tactic:
ext1 j