awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s_1 : Finset ι
n_1 : μ
f_1 : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x_1 x_2 : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) f
g : ι →₀ μ
hg_1 : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag p.2) g
hf : s.sum (⇑f : (a : ι) → μ) = p.2 ∧ f.support ⊆ s
hg : s.sum (⇑g : (a : ι) → μ) = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), Eq.{u_2 + 1} (α := μ) ((f.update a p.1 : (a : ι) → μ) x : μ) ((g.update a p.1 : (a : ι) → μ) x : μ)
x : ι
hx : x ≠ a
⊢ Eq.{u_2 + 1} (α := μ) ((f : (a : ι) → μ) x : μ) ((g : (a : ι) → μ) x : μ)

Tactic:
simpa only [coe_update, Function.update, dif_neg hx] using hfg x

Premises used: Function.update, Finsupp.coe_update, dif_neg
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
h₁ :
  ∀ (f : ι →₀ μ),
    Membership.mem (γ := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n) f ↔
      Membership.mem (γ := Finset (ι →₀ μ))
        ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
          map (α := ↥(s.finsuppAntidiag p.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag p.2)))
        f
⊢ Eq (α := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n)
    ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
      map (α := ↥(s.finsuppAntidiag p.2))
        { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := ⋯ }
        (attach (s.finsuppAntidiag p.2)))

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
h₁ :
  (∃ m ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag m.2) g) ↔
    ∃ a_1 ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n,
      Membership.mem (γ := Finset (ι →₀ μ))
        (map (α := ↥(s.finsuppAntidiag a_1.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag a_1.2)) ↦ (↑f : ι →₀ μ).update a a_1.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag a_1.2)))
        f
⊢ Membership.mem (γ := Finset (ι →₀ μ)) ((insert a s).finsuppAntidiag n) f ↔
    Membership.mem (γ := Finset (ι →₀ μ))
      ((@antidiagonal _ AddCommMonoid.toAddMonoid _ n).biUnion fun (p : μ × μ) ↦
        map (α := ↥(s.finsuppAntidiag p.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ μ).update a p.1, inj' := ⋯ }
          (attach (s.finsuppAntidiag p.2)))
      f

Tactic:
rw [mem_finsuppAntidiag_insert h, mem_biUnion]

Premises used: Finset.mem_finsuppAntidiag_insert, Finset.mem_biUnion
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
a : ι →₀ μ
simp_rw :
  (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ s → (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ t
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) a →
    Membership.mem (γ := Finset (ι →₀ μ)) (t.finsuppAntidiag n) a

Tactic:
simp_rw [mem_finsuppAntidiag']

Premises used: Finset.mem_finsuppAntidiag'
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
a : ι →₀ μ
hsum : (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hmem : a.support ⊆ s
⊢ (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ t

Tactic:
⟨hsum, hmem.trans h⟩

Premises used: HasSubset.Subset.trans, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s t : Finset ι
h : s ⊆ t
n : μ
a : ι →₀ μ
hsum : (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hmem : a.support ⊆ s
⊢ (a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ t

Tactic:
exact ⟨hsum, hmem.trans h⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
simp :
  (∃ (a : ι →₀ μ),
      ((a.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ a.support ⊆ s) ∧
        (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') a = f) →
    Eq (α := μ') (f.sum fun (x : ι) (x_1 : μ') ↦ x_1 : μ') ((e : (a : μ) → μ') n : μ') ∧ f.support ⊆ s
⊢ f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) →
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f

Tactic:
simp only [mem_map, mem_finsuppAntidiag']

Premises used: Finset.mem_map, Finset.mem_finsuppAntidiag'
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
simp :
  Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
      ((e : (a : μ) → μ') n : μ') ∧
    Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s
⊢ Eq.{u_3 + 1} (α := μ')
      (sum ((Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') g)
          fun (x : ι) (x_1 : μ') ↦ x_1 :
        μ')
      ((e : (a : μ) → μ') n : μ') ∧
    Finsupp.support.{u_1, u_3} (M := μ')
        ((Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e)) : (a : ι →₀ μ) → ι →₀ μ') g) ⊆
      s

Tactic:
simp only [AddEquiv.toEquiv_eq_coe, mapRange.addEquiv_toEquiv, Equiv.coe_toEmbedding,
    mapRange.equiv_apply, EquivLike.coe_coe]

Premises used: Equiv.coe_toEmbedding, Finsupp.mapRange.addEquiv_toEquiv, Finsupp.mapRange.equiv_apply, AddEquiv.toEquiv_eq_coe, EquivLike.coe_coe
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
left :
  Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ')
right : Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
      ((e : (a : μ) → μ') n : μ') ∧
    Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
left : Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b : μ') ((e : (a : μ) → μ') n : μ')
left₁ :
  Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b : μ')
    ((e : (a : μ) → μ') (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) : μ')
left₂ left₃ :
  Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b)
    (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b)
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ')

Tactic:
rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]

Premises used: map_finsuppSum, Finsupp.sum_mapRange_index
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s

Tactic:
subset_trans (support_mapRange) hsupp

Premises used: subset_trans, Finsupp.support_mapRange
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') ⊆ s

Tactic:
exact subset_trans (support_mapRange) hsupp

Premises used: subset_trans, Finsupp.support_mapRange
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
h :
  ∀ (f : ι →₀ μ'),
    f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) ↔
      Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
⊢ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) =
    s.finsuppAntidiag ((e : (a : μ) → μ') n)

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h :
  f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) →
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
h₁ :
  Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f →
    f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n)
⊢ f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) ↔
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) →
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f

Tactic:
apply mapRange_finsuppAntidiag_subset

Premises used: Finset.mapRange_finsuppAntidiag_subset
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h :
  let h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e);
  ∀ (hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)),
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f →
      f ∈ map h.toEmbedding (s.finsuppAntidiag n)
⊢ Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f →
    f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n)

Tactic:
set h := (mapRange.addEquiv e).toEquiv with hh

Premises used: Finsupp.mapRange.addEquiv, AddEquiv.toEquiv
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
⊢ n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')

Tactic:
have : n = e.symm (e n) := (AddEquiv.eq_symm_apply e).mpr rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
    (s.finsuppAntidiag ((e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')) : Finset (ι →₀ μ))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)

Tactic:
rw [mem_map_equiv, this]

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
    (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
⊢ Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
    (s.finsuppAntidiag ((e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')) : Finset (ι →₀ μ))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)

Tactic:
apply mapRange_finsuppAntidiag_subset

Premises used: Finset.mapRange_finsuppAntidiag_subset
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  f ∈
    map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
⊢ Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
    (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)

Tactic:
rw [← mem_map_equiv]

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
⊢ Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f

Tactic:
hf
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
        (s.finsuppAntidiag ((e : (a : μ) → μ') n))) =
    s.finsuppAntidiag ((e : (a : μ) → μ') n)
⊢ f ∈
    map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))

Tactic:
convert! hf
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  Eq (α := Finset (ι →₀ μ'))
    (map
      (Embedding.trans (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
        (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))))
      (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
    (s.finsuppAntidiag ((e : (a : μ) → μ') n))
⊢ map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
        (s.finsuppAntidiag ((e : (a : μ) → μ') n))) =
    s.finsuppAntidiag ((e : (a : μ) → μ') n)

Tactic:
rw [map_map, hh]

Premises used: Finset.map_map
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
⊢ Eq (α := Finset (ι →₀ μ'))
    (map (Embedding.refl (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n)) : Finset (ι →₀ μ'))
    (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ'))

Tactic:
map_refl

Premises used: Finset.map_refl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
h₁ :
  Eq (α := (ι →₀ μ') ↪ ι →₀ μ')
    (Embedding.trans (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
      (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))))
    (Embedding.refl (ι →₀ μ'))
⊢ Eq (α := Finset (ι →₀ μ'))
    (map
      (Embedding.trans (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
        (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))))
      (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
    (s.finsuppAntidiag ((e : (a : μ) → μ') n))

Tactic:
convert! map_refl

Premises used: Finset.map_refl
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
inst_4 : AddCommMonoid μ'
inst_5 : HasAntidiagonal μ'
inst_6 : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := AddEquiv.toEquiv (mapRange.addEquiv e)
hh : h = AddEquiv.toEquiv (mapRange.addEquiv e)
hf : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
⊢ Eq (α := (ι →₀ μ') ↪ ι →₀ μ')
    (Embedding.trans (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
      (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))))
    (Embedding.refl (ι →₀ μ'))

Tactic:
apply Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding

Premises used: Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq μ
inst_2 : AddCommMonoid μ
inst_3 : PartialOrder μ
inst_4 : CanonicallyOrderedAdd μ
inst_5 : HasAntidiagonal μ
s : Finset ι
h :
  ∀ (f : ι →₀ μ),
    Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f
⊢ Eq (α := Finset (ι →₀ μ)) (s.finsuppAntidiag 0) {0}

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Finsupp
Goal:
ι : Type u_1
μ : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq μ
inst_2 : AddCommMonoid μ
inst_3 : PartialOrder μ
inst_4 : CanonicallyOrderedAdd μ
inst_5 : HasAntidiagonal μ
s : Finset ι
f : ι →₀ μ
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]

Premises used: Finset.finsuppAntidiag, eq_comm, DFunLike.coe_fn_eq
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
⊢ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) (↑f : ι →₀ μ)

Tactic:
have hf := f.2
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hf : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) (↑f : ι →₀ μ)
⊢ ((↑f : ι →₀ μ).sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ (↑f : ι →₀ μ).support ⊆ s

Tactic:
rw [mem_finsuppAntidiag'] at hf

Premises used: Finset.mem_finsuppAntidiag'