awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
⊢ Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) j : M) ((single 0 y : (a : Fin (n + 1)) → M) j)
have h : Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) 0 : M) ((single 0 y : (a : Fin (n + 1)) → M) 0 : M)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
h : Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) 0 : M) ((single 0 y : (a : Fin (n + 1)) → M) 0 : M)
⊢ Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) j : M) ((single 0 y : (a : Fin (n + 1)) → M) j)
have h₁ : ∀ (i : Fin n),
  Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) i.succ : M) ((single 0 y : (a : Fin (n + 1)) → M) i.succ : M)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
⊢ Eq (α := Fin (n + 1) →₀ M) (cons 0 (single i y)) (single i.succ y)
have h : ∀ (j : Fin (n + 1)),
  Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) j : M) ((single i.succ y : (a : Fin (n + 1)) → M) j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
⊢ Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) j : M) ((single i.succ y : (a : Fin (n + 1)) → M) j)
have h : Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) 0 : M) ((single i.succ y : (a : Fin (n + 1)) → M) 0 : M)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
j : Fin (n + 1)
h : Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) 0 : M) ((single i.succ y : (a : Fin (n + 1)) → M) 0 : M)
⊢ Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) j : M) ((single i.succ y : (a : Fin (n + 1)) → M) j)
have h₁ : ∀ (i_1 : Fin n),
  Eq (α := M) ((cons 0 (single i y) : (a : Fin (n + 1)) → M) i_1.succ : M)
    ((single i.succ y : (a : Fin (n + 1)) → M) i_1.succ : M)
Tactic: cases j using Fin.cases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : y ≠ 0
⊢ cons y s ≠ 0
have contrapose : ∀ (c : cons y s = 0), y = 0
Tactic: contrapose h with c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ y = 0
have rw : Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
Tactic: rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
rw : Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
⊢ y = 0
have rw₁ : Eq.{u_1 + 1} (α := M) ((0 : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
Tactic: rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
rw : Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
rw₁ : Eq.{u_1 + 1} (α := M) ((0 : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
⊢ y = 0
have rw₂ : Eq.{u_1 + 1} (α := M) (0 0) 0
Tactic: rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
rw : Eq (α := M) ((cons y s : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
rw₁ : Eq.{u_1 + 1} (α := M) ((0 : (a : Fin (n + 1)) → M) 0 : M) (0 : M)
rw₂ : Eq.{u_1 + 1} (α := M) (0 0) 0
⊢ y = 0
have rw₃ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : s ≠ 0
⊢ cons y s ≠ 0
have contrapose : ∀ (c : cons y s = 0), s = 0
Tactic: contrapose h with c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ s = 0
have h : ∀ (a : Fin n), Eq (α := M) ((s : (a : Fin n) → M) a : M) ((0 : (a : Fin n) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
⊢ cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
have refine : ∀ (h : cons y s ≠ 0), y ≠ 0 ∨ s ≠ 0
Tactic: refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
⊢ y ≠ 0 ∨ s ≠ 0
have refine : ∀ (h' : y = 0) (c : s = 0), cons y s = 0
Tactic: refine imp_iff_not_or.1 fun h' c => h ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
⊢ cons y s = 0
have rw : cons 0 s = 0
Tactic: rw [h', c, Finsupp.cons_zero_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
rw : cons 0 s = 0
⊢ cons y s = 0
have rw₁ : Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) (cons 0 0) 0
Tactic: rw [h', c, Finsupp.cons_zero_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
h : cons y s ≠ 0
h' : y = 0
c : s = 0
rw : cons 0 s = 0
rw₁ : Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) (cons 0 0) 0
⊢ cons y s = 0
have rw₂ : Eq.{u_1 + 1} (α := Fin (n + 1) →₀ M) 0 0
Tactic: rw [h', c, Finsupp.cons_zero_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i ∈ insert 0 (Finset.map (Fin.succEmb n) s.support)
have suffices : i = 0 ∨ ∃ (a : Fin n), ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
Tactic: suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
i : Fin (n + 1)
hi : i ∈ (cons y s).support
⊢ i = 0 ∨ ∃ (a : Fin n), ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
have apply : ∀ (a : Fin n), i = a.succ → ¬Eq (α := M) ((s : (a : Fin n) → M) a : M) (0 : M) ∧ a.succ = i
Tactic: apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
⊢ Injective2.{u_1 + 1, u_1 + 1, u_1 + 1} (α := M) (β := Fin n →₀ M) cons
have refine : ∀ (x₀ y₀ : M) (x y : Fin n →₀ M) (h : cons x₀ x = cons y₀ y), x₀ = y₀ ∧ x = y
Tactic: refine fun x₀ y₀ x y h ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (hypothesis)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
⊢ x₀ = y₀ ∧ x = y
have this : Eq (α := M) ((cons x₀ x : (a : Fin (n + 1)) → M) 0 : M) ((cons y₀ y : (a : Fin (n + 1)) → M) 0 : M)
Tactic: have := DFunLike.congr_fun h 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y
have rw : cons x s = cons y 0 ↔ s = 0 ∧ x = y
Tactic: rw [← cons_zero_eq_single_zero, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons y 0 ↔ s = 0 ∧ x = y
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y
have rw₁ : x = y ∧ s = 0 ↔ s = 0 ∧ x = y
Tactic: rw [← cons_zero_eq_single_zero, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons y 0 ↔ s = 0 ∧ x = y
rw₁ : x = y ∧ s = 0 ↔ s = 0 ∧ x = y
⊢ cons x s = single 0 y ↔ s = 0 ∧ x = y
have rw₂ : s = 0 ∧ x = y ↔ s = 0 ∧ x = y
Tactic: rw [← cons_zero_eq_single_zero, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0
have rw : cons x s = cons 0 (single i y) ↔ s = single i y ∧ x = 0
Tactic: rw [← cons_zero_single_eq_single_succ, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons 0 (single i y) ↔ s = single i y ∧ x = 0
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0
have rw₁ : x = 0 ∧ s = single i y ↔ s = single i y ∧ x = 0
Tactic: rw [← cons_zero_single_eq_single_succ, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
s : Fin n →₀ M
x : M
rw : cons x s = cons 0 (single i y) ↔ s = single i y ∧ x = 0
rw₁ : x = 0 ∧ s = single i y ↔ s = single i y ∧ x = 0
⊢ cons x s = single i.succ y ↔ s = single i y ∧ x = 0
have rw₂ : s = single i y ∧ x = 0 ↔ s = single i y ∧ x = 0
Tactic: rw [← cons_zero_single_eq_single_succ, cons_injective2.eq_iff, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst_1 : DecidableEq ι
⊢ Eq.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (if hi : i ∈ s then f i hi else 0 : α)
have simp : Eq.{u_2 + 1} (α := α) (if H : i ∈ s then f i H else 0) (if hi : i ∈ s then f i hi else 0)
Tactic: simp only [indicator, ne_eq, coe_mk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
⊢ a = b
have h₁ : ∀ (i : ι) (hi : i ∈ s), a i hi = b i hi
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h :
  Eq (α := ι →₀ α) ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) a)
    ((fun (f : (i : ι) → i ∈ s → α) ↦ (indicator s f : ι →₀ α)) b)
i : ι
hi : i ∈ s
⊢ a i hi = b i hi
have h₁ : Eq.{u_2 + 1} (α := α) ((indicator s a : (a : ι) → α) i : α) ((indicator s b : (a : ι) → α) i : α)
Tactic: rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ support (indicator s f)
⊢ i ∈ s
have hi₁ : Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)
Tactic: rw [mem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : Ne.{u_2 + 1} (α := α) ((indicator s f : (a : ι) → α) i : α) (0 : α)
⊢ i ∈ s
have by_contra : ∀ (h : i ∉ s), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
⊢ Eq (α := ι →₀ α) (indicator {a} f) (single a (f a ⋯))
have h : ∀ (j : ι), Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a sorry) : (a : ι) → α) j : α)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
⊢ Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a ⋯) : (a : ι) → α) j : α)
have h : (if h : j = a then f j sorry else 0) = if j = a then f a sorry else 0
Tactic: simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
⊢ (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0
have pos : ∀ (h : j = a), f j sorry = f a sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
j : ι
pos : ∀ (h : j = a), f j ⋯ = f a ⋯
⊢ (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0
have neg : ∀ (h : ¬j = a), Eq.{u_2 + 1} (α := α) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
⊢ Eq (α := ι →₀ α) (indicator {a} f) (single a (f a ⋯))
have h : ∀ (j : ι), Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a sorry) : (a : ι) → α) j : α)
Tactic: classical
  ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
a : ι
f : (j : ι) → Membership.mem (γ := Finset ι) {a} j → α
h : ∀ (j : ι), Eq.{u_2 + 1} (α := α) ((indicator {a} f : (a : ι) → α) j : α) ((single a (f a ⋯) : (a : ι) → α) j : α)
⊢ Eq (α := ι →₀ α) (indicator {a} f) (single a (f a ⋯))
have h₁ : ∀ (j : ι), (if h : j = a then f j sorry else 0) = if j = a then f a sorry else 0
Tactic: classical
  ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
g : ι → α
⊢ (⇑(indicator s fun (i : ι) (x : i ∈ s) ↦ g i) : (a : ι) → α) = (↑s : Set ι).indicator g
have h : ∀ (i : ι), (indicator s fun (i : ι) (x : i ∈ s) ↦ g i : (a : ι) → α) i = (↑s : Set ι).indicator g i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
g : ι → α
⊢ (⇑(indicator s fun (i : ι) (x : i ∈ s) ↦ g i) : (a : ι) → α) = (↑s : Set ι).indicator g
have h : ∀ (i : ι), (indicator s fun (i : ι) (x : i ∈ s) ↦ g i : (a : ι) → α) i = (↑s : Set ι).indicator g i
Tactic: classical
  ext i
  simp [indicator_apply, Set.indicator_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
this :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
have simp : (∀ (x : ι), g x = if hi : x ∈ s then f x hi else 0) ↔ ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: simp only [this, funext_iff, indicator_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
have suffices : (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
  ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
have rw : ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
  ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: rw [Set.subset_def, and_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
have this : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
  (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0
Tactic: have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
have suffices : (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
  ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: classical
  suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
  rw [Set.subset_def, and_comm]
  have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
  simp [this, not_imp_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
suffices suffices₁ suffices₂ :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
have suffices₃ : ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
  ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: classical
  suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
  rw [Set.subset_def, and_comm]
  have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
  simp [this, not_imp_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Indicator (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
g : ι → α
suffices suffices₁ suffices₂ :
  (Function.support g ⊆ (↑s : Set ι) ∧ ∀ (i : ι) (hi : i ∈ s), f i hi = g i) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
suffices₃ :
  ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
⊢ g = (⇑(indicator s f) : (a : ι) → α) ↔ Function.support g ⊆ (↑s : Set ι) ∧ ∀ ⦃i : ι⦄ (hi : i ∈ s), f i hi = g i
have suffices₄ : ∀
  (this :
    (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      (∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ (i : ι) (hi : i ∉ s), g i = 0),
  ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ x ∈ Function.support g, x ∈ (↑s : Set ι)) ↔
    ∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0
Tactic: classical
  suffices g.support ⊆ s ∧ (∀ i (hi : i ∈ s), f i hi = g i) ↔
      (∀ i, if hi : i ∈ s then f i hi = g i else g i = 0) by
    simp only [this, funext_iff, indicator_apply]
    grind
  rw [Set.subset_def, and_comm]
  have : (∀ (i : ι), if hi : i ∈ s then f i hi = g i else g i = 0) ↔
      ((∀ (i : ι) (hi : i ∈ s), f i hi = g i) ∧ ∀ i (hi : i ∉ s), g i = 0) := by grind
  simp [this, not_imp_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
f_1 : ι →₀ α
i_1 : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∈ f.support ↔ Ne (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0
have rw : Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ↔
  Eq (α := Finset α) (singleton (α := α) ((f : (a : ι) → α) i : α)) 0
Tactic: rw [← not_iff_not, notMem_support_iff, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Zero α
inst_1 : PartialOrder α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
f_1 g_1 : ι →₀ α
i_1 : ι
a : α
f g : ι →₀ α
i : ι
⊢ i ∈ f.support ∪ g.support ↔
    Ne.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)
have rw : Eq.{u_2 + 1} (α := α) ((f : (a : ι) → α) i : α) (0 : α) ∧ Eq.{u_2 + 1} (α := α) ((g : (a : ι) → α) i : α) (0 : α) ↔
  Eq.{u_2 + 1} (α := Finset α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α) (0 : Finset α)
Tactic: rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
⊢ Membership.mem (γ := Finset (ι →₀ α))
      ((fun (f g : ι →₀ α) ↦ ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α) : Finset (ι →₀ α)))
        f g)
      x ↔
    f ≤ x ∧ x ≤ g
have rangeIcc_support : (∀ (i : ι),
    Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α)
      ((x : (a : ι) → α) i : α)) ↔
  f ≤ x ∧ x ≤ g
Tactic: refine
        (mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f_1 g_1 f g x : ι →₀ α
⊢ (∀ (i : ι),
      Membership.mem.{u_2, u_2} (α := α) (γ := Finset α) ((f.rangeIcc g : (a : ι) → Finset α) i : Finset α)
        ((x : (a : ι) → α) i : α)) ↔
    f ≤ x ∧ x ≤ g
have simp_rw : (∀ (i : ι),
    LE.le.{u_2} (α := α) ((f : (a : ι) → α) i : α) ((x : (a : ι) → α) i : α) ∧
      LE.le.{u_2} (α := α) ((x : (a : ι) → α) i : α) ((g : (a : ι) → α) i : α)) ↔
  f ≤ x ∧ x ≤ g
Tactic: simp_rw [mem_rangeIcc_apply_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
⊢ #(Icc f g) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
have simp_rw : card (α := ι →₀ α) ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α)) =
  ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
Tactic: simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Interval (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : PartialOrder α
inst_1 : Zero α
inst_2 : LocallyFiniteOrder α
inst_3 : DecidableEq ι
inst_4 : DecidableEq α
f g : ι →₀ α
simp_rw :
  card (α := ι →₀ α) ((f.support ∪ g.support).finsupp (⇑(f.rangeIcc g) : (a : ι) → Finset α)) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
⊢ #(Icc f g) =
    ∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α)
have simp_rw₁ : Eq (α := ℕ) (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) ((f.rangeIcc g : (a : ι) → Finset α) i))
  (∏ i ∈ f.support ∪ g.support, card.{u_2} (α := α) (Icc ((f : (a : ι) → α) i) ((g : (a : ι) → α) i) : Finset α))
Tactic: simp_rw [Icc_eq, card_finsupp, coe_rangeIcc]