awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
⊢ f = 0
have h : ∀ (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
have by_cases : ∀ (hs₂ : i ∈ (↑s : Multiset ι)), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: by_cases hs₂ : i ∈ s.val
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0
i : ι
this : (a : Prop) → Decidable a := Classical.propDecidable
by_cases : ∀ (hs₂ : i ∈ (↑s : Multiset ι)), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
have by_cases₁ : ∀ (hs₂ : i ∉ (↑s : Multiset ι)), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: by_cases hs₂ : i ∈ s.val
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
case case₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0), f = 0
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0
have h : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        letI := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
case case₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0), f = 0
h : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
h₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0
have case₂ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι) (hs₂ : i ∈ (↑s : Multiset ι)),
  (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        letI := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }
case case₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0), f = 0
h : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
h₁ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι), (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
case₂ :
  ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι) (hs₂ : i ∈ (↑s : Multiset ι)),
    (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
⊢ (∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) → f = 0
have case₃ : ∀ (hs₁ : ∀ i ∈ (↑s : Multiset ι), (f : (a : ι) → β a) i = 0) (i : ι) (hs₂ : i ∉ (↑s : Multiset ι)),
  (f : (a : ι) → β a) i = (0 : (a : ι) → β a) i
Tactic: case mp =>
        intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        letI := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf g =
    mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
      f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι))
have h : ∀ (i : ι),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i =
    (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
          f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
        (a : ι) → β₂ a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
have pos : ∀ (h : i = i'),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
Tactic: by_cases h : i = i'
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
pos :
  ∀ (h : i = i'),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
      (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
have neg : ∀ (h : ¬i = i'),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
Tactic: by_cases h : i = i'
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
h : i = i'
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i' =
    (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i'
have pos : (mapRange (β₁ := β₁) (β₂ := β₂) f hf (single (β := β₁) i b) : (a : ι) → β₂ a) i =
  (single (β := β₂) i (f i b) : (a : ι) → β₂ a) i
Tactic: subst i'
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)
have refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
Tactic: refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)
have refine_2 : ∀ (h : ∀ (i : ι), Function.Surjective (f i)) (x : Π₀ (i : ι), β₂ i),
  ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x
Tactic: refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)
i : ι
u : β₂ i
⊢ ∃ (a : β₁ i), f i a = u
have refine_1 : ∀ (x : Π₀ (i : ι), β₁ i) (hx : mapRange (β₁ := β₁) (β₂ := β₂) f hf x = single (β := β₂) i u), ∃ (a : β₁ i), f i a = u
Tactic: obtain ⟨x, hx⟩ := h (single i u)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : Π₀ (i : ι), β₂ i
⊢ ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x
have refine_2 : ∀ (x : (i : ι) → β₂ i) (support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }) (s : Multiset ι)
  (hs : ∀ (i : ι), i ∈ s ∨ x i = 0),
  ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
Tactic: obtain ⟨x, s, hs⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
⊢ ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
have obtain : ∀ (u : β₁ i) (hu : f i u = x i), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
Tactic: obtain ⟨u, hu⟩ := h i (x i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (hypothesis)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
have this : ∀ (i : ι), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
Tactic: have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
this : ∀ (i : ι), ∃ (u : β₁ i), f i u = x i ∧ (x i = 0 → u = 0)
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
have refine_2 : ∀ (y : (i : ι) → β₁ i) (hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)),
  ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
Tactic: choose y hy using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
have refine_2 : ∀ (i : ι), i ∈ s ∨ y i = 0
Tactic: refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support' : Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
refine_2 : ∀ (i : ι), i ∈ s ∨ y i = 0
⊢ ∃ (a : Π₀ (i : ι), β₁ i),
    mapRange (β₁ := β₁) (β₂ := β₂) f hf a =
      mk' (β := fun (i : ι) ↦ β₂ i) x
        (Quot.mk
          (⇑trueSetoid :
            { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs))
have refine_2₁ : ∀ (i : ι),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf
          (mk' (β := fun (i : ι) ↦ β₁ i) y
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ y i = 0) s sorry))) :
        (a : ι) → β₂ a)
      i =
    (mk' (β := fun (i : ι) ↦ β₂ i) x
          (Quot.mk
            (⇑trueSetoid :
              { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } →
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ x i = 0 } → Prop)
            (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ x i = 0) s hs)) :
        (a : ι) → β₂ a)
      i
Tactic: refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)
have refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
Tactic: classical
  refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨x, hx⟩ := h (single i u)
    exact ⟨x i, by simpa using congr($hx i)⟩
  · obtain ⟨x, s, hs⟩ := x
    have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
    choose y hy using this
    refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
    · exact (hs i).imp_right (hy i).2
    · simp [(hy i).1]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → Zero (β₁ i)
inst_1 : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
refine_1 : ∀ (h : Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf)) (i : ι) (u : β₂ i), ∃ (a : β₁ i), f i a = u
⊢ Function.Surjective (mapRange (β₁ := β₁) (β₂ := β₂) f hf) ↔ ∀ (i : ι), Function.Surjective (f i)
have refine_2 : ∀ (h : ∀ (i : ι), Function.Surjective (f i)) (x : Π₀ (i : ι), β₂ i),
  ∃ (a : Π₀ (i : ι), β₁ i), mapRange (β₁ := β₁) (β₂ := β₂) f hf a = x
Tactic: classical
  refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨x, hx⟩ := h (single i u)
    exact ⟨x i, by simpa using congr($hx i)⟩
  · obtain ⟨x, s, hs⟩ := x
    have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
    choose y hy using this
    refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
    · exact (hs i).imp_right (hy i).2
    · simp [(hy i).1]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase (β := β) i f).support (β := β) = f.support (β := β).erase i
have h : ∀ (a : ι), a ∈ (erase (β := β) i f).support (β := β) ↔ a ∈ f.support (β := β).erase i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ (f.update (β := β) i b).support (β := β) = insert i (f.support (β := β))
have h₁ : ∀ (j : ι), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
have h₁ : i ∈ (f.update (β := β) i b).support (β := β) ↔ i ∈ insert i (f.support (β := β))
Tactic: rcases eq_or_ne i j with (rfl | hi)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
h₁ : i ∈ (f.update (β := β) i b).support (β := β) ↔ i ∈ insert i (f.support (β := β))
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
have h₂ : ∀ (hi : i ≠ j), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
Tactic: rcases eq_or_ne i j with (rfl | hi)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst_3 : Decidable (b = 0)
⊢ (f.update (β := β) i b).support (β := β) =
    if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))
have h : ∀ (j : ι),
  j ∈ (f.update (β := β) i b).support (β := β) ↔
    j ∈ if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔
    j ∈ if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))
have pos : ∀ (hb : b = 0), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
Tactic: split_ifs with hb
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
pos : ∀ (hb : b = 0), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔
    j ∈ if b = 0 then (erase (β := β) i f).support (β := β) else insert i (f.support (β := β))
have neg : ∀ (hb : ¬b = 0), j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
Tactic: split_ifs with hb
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
have pos : ∀ [Decidable (Eq.{v + 1} (α := β i) 0 0)],
  j ∈ (f.update (β := β) i 0).support (β := β) ↔ j ∈ (erase (β := β) i f).support (β := β)
Tactic: subst hb
Cleared hypotheses: b, inst_3, hb
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst_3 : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update (β := β) i b).support (β := β) ↔ j ∈ insert i (f.support (β := β))
have neg : j ∈ insert i (f.support (β := β)) ↔ j ∈ insert i (f.support (β := β))
Tactic: rw [support_update_ne_zero f _ hb]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst_3 : DecidablePred p
f : Π₀ (i : ι), β i
⊢ subtypeDomain (β := β) p f =
    mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
      fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
      (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι)
have h : ∀ (i : Subtype p),
  (subtypeDomain (β := β) p f : (a : Subtype p) → β (↑a : ι)) i =
    (mk (β := fun (i : Subtype p) ↦ β (↑i : ι)) (Finset.subtype p (f.support (β := β)))
          fun (i : (↑(↑(Finset.subtype p (f.support (β := β))) : Set (Subtype p)) : Type u)) ↦
          (f : (a : ι) → β a) (↑(↑i : Subtype p) : ι) :
        (a : Subtype p) → β (↑a : ι))
      i
Tactic: ext i