awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ Set.Finite.{u_1} (α := α) (Function.support.{u_1, u_4} (M := M) (⇑f : (a : α) → M))

Tactic:
f.fun_support_eq.symm ▸ f.support.finite_toSet

Premises used: Finsupp.fun_support_eq, Finsupp.support, Eq.rec, Finset.finite_toSet, Eq.symm
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
⊢ Set.Finite.{u_1} (α := α) (Function.support.{u_1, u_4} (M := M) (⇑f : (a : α) → M))

Tactic:
exact f.fun_support_eq.symm ▸ f.support.finite_toSet
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Set α
f : α →₀ M
⊢ (↑f.support : Set α) ⊆ s ↔ ∀ a ∉ s, Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
M : Type u_4
inst : Zero M
α : Type u_9
inst_1 : Finite α
f : α →₀ M
⊢ (Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) (⇑f : (a : α) → M) = f

Tactic:
equivFunOnFinite.symm_apply_apply f

Premises used: Equiv.symm_apply_apply, Finsupp.equivFunOnFinite
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
M : Type u_4
inst : Zero M
α : Type u_9
inst_1 : Finite α
f : α → M
⊢ (⇑((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f : α →₀ M) : (a : α) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
inst_1 : Unique α
f g : α →₀ M
h : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) default : M) ((g : (a : α) → M) default : M)
a : α
rwa rwa₁ rwa₂ rwa₃ : Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) default : M) ((g : (a : α) → M) default : M)
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) ((g : (a : α) → M) a : M)

Tactic:
rwa [Unique.eq_default a]

Premises used: Unique.eq_default
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ (a : α), a ∈ onFinsetSupport s f ↔ f a ≠ 0

Tactic:
simpa [onFinsetSupport]

Premises used: Finsupp.onFinsetSupport
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (⇑(onFinset s f hf) : (a : α) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ (onFinset s f hf : (a : α) → M) a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
inst_1 : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ {a ∈ s | f a ≠ 0} = {a ∈ s | ¬f a = 0}

Tactic:
congr
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
f : α →₀ M
⊢ ∀ (a : α), Ne.{u_4 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → a ∈ f.support

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
h :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := M) ((onFinset f.support (⇑f : (a : α) → M) ⋯ : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ onFinset f.support (⇑f : (a : α) → M) ⋯ = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((onFinset f.support (⇑f : (a : α) → M) ⋯ : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support ⊆ s

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
rw : Ne.{u_4 + 1} (α := M) ((onFinset s f hf : (a : α) → M) a : M) (0 : M) ↔ f a ≠ 0
rw₁ rw₂ : f a ≠ 0 ↔ f a ≠ 0
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0

Tactic:
rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]

Premises used: Finsupp.mem_support_iff, Finsupp.onFinset_apply
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α → M
hf : (Function.support f).Finite
⊢ (⇑(ofSupportFinite f hf) : (a : α) → M) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α → M
hf : (Function.support f).Finite
h : ∀ (a : α), a ∈ (ofSupportFinite f hf).support ↔ a ∈ hf.toFinset (s := Function.support f)
⊢ (ofSupportFinite f hf).support = hf.toFinset (s := Function.support f)

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
f : α → M
hf : (Function.support f).Finite
a : α
⊢ a ∈ (ofSupportFinite f hf).support ↔ a ∈ hf.toFinset (s := Function.support f)

Tactic:
simp [ofSupportFinite_coe]

Premises used: Finsupp.ofSupportFinite_coe
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
rw : Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M) → (f ∘ (⇑g : (a : α) → M)) a = 0
⊢ (f ∘ (⇑g : (a : α) → M)) a ≠ 0 → a ∈ g.support

Tactic:
rw [mem_support_iff, not_imp_not]

Premises used: Finsupp.mem_support_iff, not_imp_not
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M) → (f ∘ (⇑g : (a : α) → M)) a = 0

Tactic:
fun H => (congr_arg f H).trans hf

Premises used: congr_arg, Eq.trans
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((g : (a : α) → M) a : M) (0 : M) → (f ∘ (⇑g : (a : α) → M)) a = 0

Tactic:
exact fun H => (congr_arg f H).trans hf

Premises used: congr_arg, Eq.trans
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (mapRange f hf g : (a : α) → N) a = f ((g : (a : α) → M) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
f : M → N
hf : f 0 = 0
x : α
⊢ Eq.{u_5 + 1} (α := N) ((mapRange f hf 0 : (a : α) → N) x : N) ((0 : (a : α) → N) x : N)

Tactic:
simp only [hf, zero_apply, mapRange_apply]

Premises used: Finsupp.mapRange_apply, Finsupp.zero_apply
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
a : α →₀ M
f : M → N
hf : Injective f
h : f 0 = 0
⊢ mapRange f h a = 0 ↔ a = 0

Tactic:
simp [Finsupp.ext_iff, ← h, hf.eq_iff]

Premises used: Function.Injective.eq_iff, Finsupp.ext_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
g : α →₀ M
⊢ mapRange id ⋯ g = g

Tactic:
ext fun _ => rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : N → O
hf : f 0 = 0
f₂ : M → N
hf₂ : f₂ 0 = 0
h : (f ∘ f₂) 0 = 0
g : α →₀ M
⊢ mapRange (f ∘ f₂) h g = mapRange f hf (mapRange f₂ hf₂ g)

Tactic:
ext fun _ => rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e₁ : N → O
e₂ : M → N
he₁ : e₁ 0 = 0
he₂ : e₂ 0 = 0
f : α →₀ M
⊢ (e₁ ∘ e₂) 0 = 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e₁ : N → O
e₂ : M → N
he₁ : e₁ 0 = 0
he₂ : e₂ 0 = 0
f : α →₀ M
⊢ mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) ⋯ f

Tactic:
ext fun _ ↦ rfl

Premises used: Finsupp.ext, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
f : M → N
hf : f 0 = 0
g : α →₀ M
⊢ (mapRange f hf g).support ⊆ g.support

Tactic:
support_onFinset_subset

Premises used: Set.Mem, setOf, Finsupp.support_onFinset_subset
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he0 : e 0 = 0
f : ι →₀ M
he : Injective e
⊢ (mapRange e he0 f).support = f.support

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
h :
  ∀ (g : α →₀ N),
    Membership.mem (γ := Set (α →₀ N)) (Set.range (mapRange e he₀)) g ↔
      Membership.mem (γ := Set (α →₀ N))
        {g : α →₀ N | ∀ (i : α), Membership.mem (α := N) (Set.range e) ((g : (a : α) → N) i : N)} g
⊢ Eq (α := Set (α →₀ N)) (Set.range (mapRange e he₀))
    {g : α →₀ N | ∀ (i : α), Membership.mem (α := N) (Set.range e) ((g : (a : α) → N) i : N)}

Tactic:
ext g
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : (∃ (y : α →₀ M), mapRange e he₀ y = g) → ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
h₁ : (∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i) → ∃ (y : α →₀ M), mapRange e he₀ y = g
⊢ (∃ (y : α →₀ M), mapRange e he₀ y = g) ↔ ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ (y : α →₀ M), mapRange e he₀ y = g) → ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
h₁ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i), ∃ (y : α →₀ M), mapRange e he₀ y = g
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g

Tactic:
choose f h using h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : (i : α) → M
h : ∀ (i : α), e (f i) = (g : (a : α) → N) i
⊢ ∀ (a : α), Ne.{u_4 + 1} (α := M) ((fun (x : α) ↦ if x ∈ g.support then f x else 0) a) 0 → a ∈ g.support

Tactic:
simp_all
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : (i : α) → M
h : ∀ (i : α), e (f i) = (g : (a : α) → N) i
h₁ : mapRange e he₀ (onFinset g.support (fun (x : α) ↦ if x ∈ g.support then f x else 0) ⋯) = g
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g

Tactic:
use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)

Premises used: Finsupp.support, Membership.mem, Finsupp.onFinset, OfNat.ofNat, ite
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : (i : α) → M
h : ∀ (i : α), e (f i) = (g : (a : α) → N) i
⊢ mapRange e he₀ (onFinset g.support (fun (x : α) ↦ if x ∈ g.support then f x else 0) ⋯) = g

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ (y : M), e y = (g : (a : α) → N) i
h₁ : ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i), ∃ (y : α →₀ M), mapRange e he₀ y = g
h₂ :
  ∀ (f : (i : α) → M) (h : ∀ (i : α), e (f i) = (g : (a : α) → N) i),
    mapRange e he₀ (onFinset g.support (fun (x : α) ↦ if x ∈ g.support then f x else 0) ⋯) = g
⊢ ∃ (y : α →₀ M), mapRange e he₀ y = g

Tactic:
classical
    choose f h using h
    use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
    grind
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h : mapRange e he₀ a = mapRange e he₀ b
rw :
  ∀
    (h :
      ∀ (a_1 : α),
        Eq.{u_5 + 1} (α := N) ((mapRange e he₀ a : (a : α) → N) a_1 : N) ((mapRange e he₀ b : (a : α) → N) a_1 : N))
    (a_1 : α), Eq.{u_4 + 1} (α := M) ((a : (a : α) → M) a_1 : M) ((b : (a : α) → M) a_1 : M)
⊢ a = b

Tactic:
rw [Finsupp.ext_iff] at h ⊢

Premises used: Finsupp.ext_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Injective e
a b : α →₀ M
h :
  ∀ (a_1 : α),
    Eq.{u_5 + 1} (α := N) ((mapRange e he₀ a : (a : α) → N) a_1 : N) ((mapRange e he₀ b : (a : α) → N) a_1 : N)
⊢ ∀ (a_1 : α), Eq.{u_4 + 1} (α := M) ((a : (a : α) → M) a_1 : M) ((b : (a : α) → M) a_1 : M)

Tactic:
simpa only [mapRange_apply, he.eq_iff] using h

Premises used: Finsupp.mapRange_apply, Function.Injective.eq_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
rw :
  Eq (α := Set (α →₀ N))
    {g : α →₀ N | ∀ (i : α), Membership.mem.{u_5, u_5} (α := N) (γ := Set N) Set.univ ((g : (a : α) → N) i : N)}
    Set.univ
⊢ Surjective (α := α →₀ M) (mapRange e he₀)

Tactic:
rw [← Set.range_eq_univ, range_mapRange, he.range_eq]

Premises used: Finsupp.range_mapRange, Set.range_eq_univ, Function.Surjective.range_eq
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M → N
he₀ : e 0 = 0
he : Surjective e
⊢ Eq (α := Set (α →₀ N))
    {g : α →₀ N | ∀ (i : α), Membership.mem.{u_5, u_5} (α := N) (γ := Set N) Set.univ ((g : (a : α) → N) i : N)}
    Set.univ

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_4 + 1} (α := M) ((e.symm : (a : N) → M) 0 : M) (0 : M)

Tactic:
simp [← hf]
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ M
h :
  ∀ (a : ι),
    Eq.{u_4 + 1} (α := M) ((mapRange (⇑e.symm : (a : N) → M) ⋯ (mapRange (⇑e : (a : M) → N) hf x) : (a : ι) → M) a : M)
      ((x : (a : ι) → M) a : M)
⊢ mapRange (⇑e.symm : (a : N) → M) ⋯ (mapRange (⇑e : (a : M) → N) hf x) = x

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ M
a : ι
⊢ Eq.{u_4 + 1} (α := M) ((mapRange (⇑e.symm : (a : N) → M) ⋯ (mapRange (⇑e : (a : M) → N) hf x) : (a : ι) → M) a : M)
    ((x : (a : ι) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ N
h :
  ∀ (a : ι),
    Eq.{u_5 + 1} (α := N) ((mapRange (⇑e : (a : M) → N) hf (mapRange (⇑e.symm : (a : N) → M) ⋯ x) : (a : ι) → N) a : N)
      ((x : (a : ι) → N) a : N)
⊢ mapRange (⇑e : (a : M) → N) hf (mapRange (⇑e.symm : (a : N) → M) ⋯ x) = x

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
x : ι →₀ N
a : ι
⊢ Eq.{u_5 + 1} (α := N) ((mapRange (⇑e : (a : M) → N) hf (mapRange (⇑e.symm : (a : N) → M) ⋯ x) : (a : ι) → N) a : N)
    ((x : (a : ι) → N) a : N)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
inst : Zero M
H :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_4 + 1} (α := M) ((((equiv (Equiv.refl M) ⋯ : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
      ((((Equiv.refl (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
⊢ Eq (α := (ι →₀ M) ≃ (ι →₀ M)) (equiv (Equiv.refl M) ⋯) (Equiv.refl (ι →₀ M))

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
inst : Zero M
x : ι →₀ M
a : ι
⊢ Eq.{u_4 + 1} (α := M) ((((equiv (Equiv.refl M) ⋯ : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((Equiv.refl (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
rw : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) ((e : (a : M) → N) 0 : N) : O) (0 : O)
rw₁ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
rw₂ rw₃ : Eq.{u_6 + 1} (α := O) 0 0
⊢ Eq.{u_6 + 1} (α := O) ((e.trans f₂ : (a : M) → O) 0 : O) (0 : O)

Tactic:
rw [Equiv.trans_apply, hf, hf₂]

Premises used: Equiv.trans_apply
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
H :
  ∀ (x : ι →₀ M) (a : ι),
    Eq.{u_6 + 1} (α := O) ((((equiv (e.trans f₂) ⋯ : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
      ((((Equiv.trans (equiv e hf) (equiv f₂ hf₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
⊢ Eq (α := (ι →₀ M) ≃ (ι →₀ O)) (equiv (e.trans f₂) ⋯) (Equiv.trans (equiv e hf) (equiv f₂ hf₂))

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
f₂ : N ≃ O
hf₂ : Eq.{u_6 + 1} (α := O) ((f₂ : (a : N) → O) 0 : O) (0 : O)
x : ι →₀ M
a : ι
⊢ Eq.{u_6 + 1} (α := O) ((((equiv (e.trans f₂) ⋯ : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((Equiv.trans (equiv e hf) (equiv f₂ hf₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
ι : Type u_3
M : Type u_4
N : Type u_5
inst : Zero M
inst_1 : Zero N
e : M ≃ N
hf : Eq.{u_5 + 1} (α := N) ((e : (a : M) → N) 0 : N) (0 : N)
⊢ Eq (α := (ι →₀ N) ≃ (ι →₀ M)) (Equiv.symm (equiv e hf)) (equiv e.symm ⋯)

Tactic:
rfl

Premises used: Finsupp.mapRange.equiv, Finsupp.onFinset, Equiv.symm, Finsupp.mapRange, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
this : DecidableEq β
h : a₂ ∈ map f v.support
rcases :
  ∀ (a : α) (ha : a ∈ v.support) (h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β)),
    ∃! a_1 : α,
      a_1 ∈ v.support ∧ (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) a_1
⊢ ∃! a : α, a ∈ v.support ∧ (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) a

Tactic:
rcases Finset.mem_map.1 h with ⟨a, ha, rfl⟩

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
this : DecidableEq β
a : α
ha : a ∈ v.support
h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β)
⊢ ∃! a_1 : α,
    a_1 ∈ v.support ∧ (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) a_1

Tactic:
ExistsUnique.intro a ⟨ha, rfl⟩ fun b ⟨_, hb⟩ => f.injective hb

Premises used: ExistsUnique.intro, _private.0.Finsupp.embDomain.match_1, And.intro, Function.Embedding.injective, Eq, rfl
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
this : DecidableEq β
a : α
ha : a ∈ v.support
h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β)
⊢ ∃! a_1 : α,
    a_1 ∈ v.support ∧ (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) a_1

Tactic:
exact ExistsUnique.intro a ⟨ha, rfl⟩ fun b ⟨_, hb⟩ => f.injective hb

Premises used: ExistsUnique.intro
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
pos :
  ∀ (h : a₂ ∈ map f v.support),
    a₂ ∈ map f v.support ↔
      ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M)
          (0 : M)
neg : ∀ (h : a₂ ∉ map f v.support), a₂ ∈ map f v.support ↔ ¬Eq.{u_4 + 1} (α := M) 0 0
⊢ a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M)
        (if h : a₂ ∈ map f v.support then
          (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
        else 0)
        0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
pos :
  ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M) (0 : M)
⊢ a₂ ∈ map f v.support ↔
    ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M)
        (0 : M)

Tactic:
simp only [h, true_iff]

Premises used: true_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
pos : choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯ ∈ v.support
⊢ ¬Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯) : M) (0 : M)

Tactic:
rw [← notMem_support_iff, not_not]

Premises used: Classical.not_not, Finsupp.notMem_support_iff
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯ ∈ v.support

Tactic:
apply Finset.choose_mem

Premises used: Finset.choose_mem
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∈ map f v.support
⊢ choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯ ∈ v.support

Tactic:
classical apply Finset.choose_mem

Premises used: Finset.choose_mem
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst : Zero M
inst_1 : Zero N
f : α ↪ β
v : α →₀ M
a₂ : β
h : a₂ ∉ map f v.support
⊢ a₂ ∈ map f v.support ↔ ¬Eq.{u_4 + 1} (α := M) 0 0

Tactic:
simp only [h, not_true_eq_false]

Premises used: not_true_eq_false
-- Module: Mathlib.Data.Finsupp.Defs
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
⊢ (embDomain f v).support = map f v.support

Tactic:
rfl

Premises used: Finset.map, rfl