awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (hypothesis)
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)
⊢ (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
have h₂ : r j i ∧ j ∉ p
Tactic: rw [Classical.not_imp] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
have neg : (x₂ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
Tactic: rw [hr j h₁.1, if_neg h₁.2]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
have neg₁ : (x₂ : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j
Tactic: rw [hr j h₁.1, if_neg h₁.2]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
have neg : ∀ (j : ι) (hj : r j i), (x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j
Tactic: refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ ∃ (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
have neg₁ : (fun {i : ι} ↦ s i) ((x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
Tactic: refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ ∃ (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
have 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
Tactic: refine ⟨⟨{ j | r j i ∧ j ∈ p }, x₁, piecewise x₂ x { j | r j i }⟩,
      .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ (x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) j = (x₂ : (a : ι) → α a) j
have neg : (if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) = (x₂ : (a : ι) → α a) j
Tactic: simp only [piecewise_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ (fun {i : ι} ↦ s i) ((x₂.piecewise (β := α) x {j : ι | r j i} : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
have neg : s i (if r i i then (x₂ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
Tactic: simp only [piecewise_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ (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
have neg : x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} = x
Tactic: simp only [piecewise_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ s i (if r i i then (x₂ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
have pos : ∀ (hi : r i i), s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ s i (if r i i then (x₂ : (a : ι) → α a) i else (x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
have neg : ∀ (hi : ¬r i i), s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
have 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)
Tactic: rwa [hr i hi, if_neg hp] at hs
Cleared hypotheses: hs, hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ s i ((x₂ : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
have 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)
Tactic: rwa [hr i hi, if_neg hp] at hs
Cleared hypotheses: hs, hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} = x
have neg : ∀ (j : ι),
  (x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} : (a : ι) → α a) j =
    (x : (a : ι) → α a) j
Tactic: ext1 j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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 : ι
⊢ (x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} : (a : ι) → α a) j =
    (x : (a : ι) → α a) j
have neg : (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
  (x : (a : ι) → α a) j
Tactic: simp only [piecewise_apply, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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 : ι
⊢ (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j
have pos : ∀ (h₁ : r j i ∧ j ∈ p), (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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), (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
⊢ (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j
have pos₁ : ∀ (h₁ : ¬(r j i ∧ j ∈ p)) (h₂ : r j i), (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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), (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
pos₁ : ∀ (h₁ : ¬(r j i ∧ j ∈ p)) (h₂ : r j i), (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
⊢ (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j
have neg : ∀ (h₁ : ¬(r j i ∧ j ∈ p)) (h₂ : ¬r j i), (x : (a : ι) → α a) j = (x : (a : ι) → α a) j
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
have pos : (x₁ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
Tactic: rw [hr j h₁.1, if_pos h₁.2]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
pos : (x₁ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
⊢ (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
have pos₁ : (x₁ : (a : ι) → α a) j = (x₁ : (a : ι) → α a) j
Tactic: rw [hr j h₁.1, if_pos h₁.2]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
have pos : j ∉ p
Tactic: rw [hr j h₂, if_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have h : piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
    ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
    ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1 =
  x
Tactic: convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have h : piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
    ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
    ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1 =
  x
Tactic: classical
    convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)
    convert! piecewise_single_erase x i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ i ∈ x.support (β := α),
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
have generalize : ∀ (t : Finset ι) (ht : x.support (β := α) = t),
  (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: generalize ht : x.support = t
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : x.support (β := α) = t
⊢ (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
have revert : ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
  (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: revert x
Cleared hypotheses: x, ht
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : x.support (β := α) = ∅
⊢ (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
have empty : (∀ (i : ι),
    Membership.mem (γ := Finset ι) ∅ i →
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((0 : (a : ι) → α a) i))) →
  Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0
Tactic: rw [support_eq_empty.1 ht]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = insert b t),
    (∀ i ∈ insert b t,
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
have insert : ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = insert b t)
  (h :
    ∀ i ∈ insert b t,
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))),
  Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) b x)
Tactic: refine fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
x : Π₀ (i : ι), α i
ht : x.support (β := α) = insert b t
h : ∀ i ∈ insert b t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
⊢ (erase (β := α) b x).support (β := α) = t
have rw : x.support (β := α).erase b = t
Tactic: rw [support_erase, ht, Finset.erase_insert hb]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
x : Π₀ (i : ι), α i
ht : x.support (β := α) = insert b t
h : ∀ i ∈ insert b t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
rw : x.support (β := α).erase b = t
⊢ (erase (β := α) b x).support (β := α) = t
have rw₁ : (insert b t).erase b = t
Tactic: rw [support_erase, ht, Finset.erase_insert hb]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
x : Π₀ (i : ι), α i
ht : x.support (β := α) = insert b t
h : ∀ i ∈ insert b t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
rw : x.support (β := α).erase b = t
rw₁ : (insert b t).erase b = t
⊢ (erase (β := α) b x).support (β := α) = t
have rw₂ : t = t
Tactic: rw [support_erase, ht, Finset.erase_insert hb]