awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
have a : ∀ (i : ι) (hi : p i) (y : γ) (hy : y ∈ S i),
  (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
          (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
        (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y
Tactic: refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
          (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
        (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y
have a : (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ)
    (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
  y
Tactic: rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ Membership.mem.{w, w} (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    ((AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
            (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
          (a : Π₀ (i : ι), ↥(S i)) → γ)
        v :
      γ)
have a : ∀ (i : ι),
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
            Π₀ (i : ι), ↥(S i)) :
          (a : ι) → ↥(S a))
        i ≠
      0 →
    Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
      (((S i).subtype : (a : ↥(S i)) → γ)
          ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        γ)
Tactic: refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
have a : Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
  (((S i).subtype : (a : ↥(S i)) → γ)
      ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
            Π₀ (i : ι), ↥(S i)) :
          (a : ι) → ↥(S a))
        i) :
    γ)
Tactic: refine AddSubmonoid.mem_iSup_of_mem i ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
have pos : ∀ (hp : p i),
  Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
Tactic: by_cases hp : p i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
pos :
  ∀ (hp : p i),
    Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
      (((S i).subtype : (a : ↥(S i)) → γ)
          ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        γ)
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
have neg : ∀ (hp : ¬p i),
  Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
Tactic: by_cases hp : p i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x
have rw : (∃ (f : Π₀ (i : ι), ↥(S i)),
    (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) f = x) ↔
  ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x
Tactic: rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Submonoid (goal)
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)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) f = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x
have simp_rw : (∃ (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: simp_rw [sumAddHom_apply]
-- 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
hs : s i ((x : (a : ι) → α a) i) (if i ∈ p then (x₁ : (a : ι) → α a) i else (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 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
Tactic: split_ifs at hs with hp
Cleared hypotheses: hs
-- 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
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
⊢ ∃ (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 : ∀ (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: split_ifs at hs with hp
Cleared hypotheses: hs
-- 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 pos : ∀ (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 }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨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)
pos : ∀ (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 pos₁ : (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 }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨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)
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)
⊢ ∃ (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 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
Tactic: refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨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 pos : (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 pos : 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₁.piecewise (β := α) x {j : ι | r j i}, x₂) =
    x
have pos : (x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {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_pos 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_pos 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 {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} = x
have pos : ∀ (j : ι),
  ((x₁.piecewise (β := α) x {j : ι | r j i}).piecewise (β := α) x₂ {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 {j : ι | r j i}).piecewise (β := α) x₂ {j : ι | r j i → j ∈ p} : (a : ι) → α a) j =
    (x : (a : ι) → α a) j
have 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
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 if r j i then (x₁ : (a : ι) → α a) j else (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) (h₂ : r j i), (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
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 : ι
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
⊢ (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
have neg₁ : ∀ (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 : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ (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₂, if_pos (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
h₂ : r j i
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₂, if_pos (h₁ h₂)]