awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ')
⊢ 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
have right : Finsupp.support.{u_1, u_3} (M := μ') (mapRange (⇑e : (a : μ) → μ') sorry g : ι →₀ μ') ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ')
have left : Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b : μ') ((e : (a : μ) → μ') n : μ')
Tactic: rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ')
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ')
have left₁ : Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b : μ')
  ((e : (a : μ) → μ') (g.sum fun (x : ι) (x_1 : μ) ↦ x_1) : μ')
Tactic: rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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) : μ')
⊢ Eq.{u_3 + 1} (α := μ') (sum (M := μ') (mapRange (⇑e : (a : μ) → μ') ⋯ g : ι →₀ μ') fun (x : ι) (x_1 : μ') ↦ x_1 : μ')
    ((e : (a : μ) → μ') n : μ')
have left₂ : Eq.{u_3 + 1} (α := μ') (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b)
  (g.sum fun (a : ι) (b : μ) ↦ (e : (a : μ) → μ') b)
Tactic: rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ
⊢ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) =
    s.finsuppAntidiag ((e : (a : μ) → μ') n)
have h : ∀ (f : ι →₀ μ'),
  f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) ↔
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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
have h : f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) →
  Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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
⊢ f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n) ↔
    Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f
have h₁ : Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f →
  f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : ι →₀ μ'
⊢ Membership.mem (γ := Finset (ι →₀ μ')) (s.finsuppAntidiag ((e : (a : μ) → μ') n) : Finset (ι →₀ μ')) f →
    f ∈ map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))) (s.finsuppAntidiag n)
have 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)
Tactic: set h := (mapRange.addEquiv e).toEquiv with hh
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (hypothesis)
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
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)
have this : n = (e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')
Tactic: have : n = e.symm (e n) := (AddEquiv.eq_symm_apply e).mpr rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ')
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)
have h₁ : Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
  (s.finsuppAntidiag ((e.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')) : Finset (ι →₀ μ))
  ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
Tactic: rw [mem_map_equiv, this]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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.symm : (a : μ') → μ) ((e : (a : μ) → μ') n : μ')) : Finset (ι →₀ μ))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
have h₁ : Membership.mem (α := ι →₀ μ) (γ := Finset (ι →₀ μ))
  (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
  ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
Tactic: apply mapRange_finsuppAntidiag_subset
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 (ι →₀ μ))
    (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
    ((h.symm : (a : ι →₀ μ') → ι →₀ μ) f : ι →₀ μ)
have h₁ : f ∈
  map h.toEmbedding
    (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
Tactic: rw [← mem_map_equiv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ')
⊢ f ∈
    map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n)))
have h₁ : map h.toEmbedding
    (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm))) (s.finsuppAntidiag ((e : (a : μ) → μ') n))) =
  s.finsuppAntidiag ((e : (a : μ) → μ') n)
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 : μ')
⊢ map h.toEmbedding
      (map (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
        (s.finsuppAntidiag ((e : (a : μ) → μ') n))) =
    s.finsuppAntidiag ((e : (a : μ) → μ') n)
have 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))
Tactic: rw [map_map, hh]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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.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))
have h₁ : Eq (α := (ι →₀ μ') ↪ ι →₀ μ')
  (Embedding.trans (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e.symm)))
    (Equiv.toEmbedding (AddEquiv.toEquiv (mapRange.addEquiv e))))
  (Embedding.refl (ι →₀ μ'))
Tactic: convert! map_refl
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Finsupp (goal)
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 ι
⊢ Eq (α := Finset (ι →₀ μ)) (s.finsuppAntidiag 0) {0}
have h : ∀ (f : ι →₀ μ),
  Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag 0) f ↔ Membership.mem (γ := Finset (ι →₀ μ)) {0} f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.FinsuppEquiv (hypothesis)
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)
⊢ (sum (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) fun (x : ↥s) ↦ id) = n
have hf : Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) (↑f : ι →₀ μ)
Tactic: have hf := f.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.FinsuppEquiv (hypothesis)
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 : ι →₀ μ)
⊢ (sum (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) fun (x : ↥s) ↦ id) = n
have hf₁ : ((↑f : ι →₀ μ).sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ (↑f : ι →₀ μ).support ⊆ s
Tactic: rw [mem_finsuppAntidiag'] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.FinsuppEquiv (hypothesis)
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)
⊢ (fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
        (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
            ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
          ↥(s.finsuppAntidiag n)))
      ((fun (f : ↥(s.finsuppAntidiag n)) ↦
          (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
              (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
            { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
        f) =
    f
have hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
Tactic: obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.FinsuppEquiv (hypothesis)
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)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
⊢ (fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
        (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
            ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
          ↥(s.finsuppAntidiag n)))
      ((fun (f : ↥(s.finsuppAntidiag n)) ↦
          (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
              (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
            { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
        f) =
    f
have hs : (↑f : ι →₀ μ).support ⊆ s
Tactic: obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.FinsuppEquiv (goal)
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)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
hs : (↑f : ι →₀ μ).support ⊆ s
⊢ (fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
        (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
            ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
          ↥(s.finsuppAntidiag n)))
      ((fun (f : ↥(s.finsuppAntidiag n)) ↦
          (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
              (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
            { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
        f) =
    f
have a : (↑((fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
          (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
              ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) sorry :
            ↥(s.finsuppAntidiag n)))
        ((fun (f : ↥(s.finsuppAntidiag n)) ↦
            (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
                (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) sorry :
              { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
          f)) :
    ι →₀ μ) =
  (↑f : ι →₀ μ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
divisorsAntidiagonal : (n : ℕ+) → Finset (ℕ+ × ℕ+) :=
  fun (n : ℕ+) ↦
    map
      {
        toFun := fun (x : ↥(↑n : ℕ).divisorsAntidiagonal) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).1 ⋯,
            Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).2 ⋯),
        inj' := ⋯ }
      (↑n : ℕ).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n
have simp_rw : (∃ (a : ℕ × ℕ) (h : a ∈ (↑n : ℕ).divisorsAntidiagonal),
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.1 sorry) : ℕ) = (↑x.1 : ℕ) ∧
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.2 sorry) : ℕ) = (↑x.2 : ℕ)) ↔
  (↑(x.1 * x.2) : ℕ) = (↑n : ℕ)
Tactic: simp_rw [divisorsAntidiagonal, Finset.mem_map, Finset.mem_attach, Function.Embedding.coeFn_mk,
      Prod.ext_iff, true_and, ← coe_inj, Subtype.exists]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : Fin d → ℕ
⊢ Membership.mem (γ := Finset (Fin d → ℕ))
      (if hn : 0 < n then
        map
          (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
              { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
          (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn)))
      else ∅)
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
have pos : ∀ (h : 0 < n),
  Membership.mem (γ := Finset (Fin d → ℕ))
      (map
        (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
            { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
        (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h))))
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : Fin d → ℕ
pos :
  ∀ (h : 0 < n),
    Membership.mem (γ := Finset (Fin d → ℕ))
        (map
          (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
              { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
          (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h))))
        f ↔
      ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ Membership.mem (γ := Finset (Fin d → ℕ))
      (if hn : 0 < n then
        map
          (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
              { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
          (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn)))
      else ∅)
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
have neg : ∀ (h : ¬0 < n), Membership.mem (γ := Finset (Fin d → ℕ)) ∅ f ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ Membership.mem (γ := Finset (Fin d → ℕ))
      (map
        (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
            { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
        (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h))))
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
have pos : (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) ↔
  ∏ i : Fin d, f i = n ∧ n ≠ 0
Tactic: simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply,
      Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
      toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
      PNat.coe_prod]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
have pos : (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) →
  ∏ i : Fin d, f i = n ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : Fin d → ℕ
h : 0 < n
pos :
  (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) →
    ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
have pos₁ : ∏ i : Fin d, f i = n ∧ n ≠ 0 →
  ∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
f : Fin d → ℕ
h : LT.lt (α := ℕ) 0 (∏ i : Fin d, f i)
right : Ne (α := ℕ) (∏ i : Fin d, f i) 0
⊢ ∃ (x : (a : Fin d) → ℕ+),
    Eq (α := ℕ) (∏ i : Fin d, (↑(x i) : ℕ)) (∏ i : Fin d, f i) ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f
have pos : ∀ (i : Fin d), 0 < f i
Tactic: refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩