awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
have inl : ∀ (eq : s = ∅),
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
Tactic: obtain eq | ne := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
inl :
  ∀ (eq : s = ∅),
    Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
      x = y
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
have inr : ∀ (ne : s.Nonempty),
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
Tactic: obtain eq | ne := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
have hn : let n := s.max' ne;
n = s.max' ne
Tactic: set n := s.max' ne with hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ := s.max' ne
hn : n = s.max' ne
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
have inr : ∀ (n : ℕ) (hn : n = s.max' ne),
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
Tactic: clear_value n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ
hn : n = s.max' ne
⊢ Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
    x = y
have inr : ∀ ⦃x y : ℕ →₀ P⦄,
  let s := x.support ∪ y.support;
  ∀ (ne : s.Nonempty) (hn : n = s.max' ne),
    Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
      x = y
Tactic: revert x y
Cleared hypotheses: x, y, s, ne, hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
hn : n = s.max' ne
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
⊢ x = y
have inr : HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((x : (a : ℕ) → P) 0) : ℕ →₀ P) (erase 0 x) =
  HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((y : (a : ℕ) → P) 0) : ℕ →₀ P) (erase 0 y)
Tactic: rw [← x.single_add_erase 0, ← y.single_add_erase 0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
hn : n = s.max' ne
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
⊢ HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((x : (a : ℕ) → P) 0) : ℕ →₀ P) (erase 0 x) =
    HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((y : (a : ℕ) → P) 0) : ℕ →₀ P) (erase 0 y)
have inr : HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).1)
    (mapDomain (fun (x : ℕ) ↦ x + 1)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x)) =
  HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).1)
    (mapDomain (fun (x : ℕ) ↦ x + 1)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y))
Tactic: simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
hn : n = s.max' ne
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
⊢ HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).1)
      (mapDomain (fun (x : ℕ) ↦ x + 1)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x)) =
    HAdd.hAdd (α := ℕ →₀ P) (Finsupp.single 0 ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).1)
      (mapDomain (fun (x : ℕ) ↦ x + 1)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y))
have inr : Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
  ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
hn : n = s.max' ne
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
⊢ Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
    ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
have inr : ∀
  (ne :
    ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)),
  False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne_1 : s.Nonempty
hn : n = s.max' ne_1
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
ne :
  ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
⊢ False
have apply : Finset.Nonempty (α := ℕ)
  (Finsupp.support.{0, u_4} (M := P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
    Finsupp.support.{0, u_4} (M := P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y))
Tactic: apply ne (ih _ _ _ rfl (inj _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne_1 : s.Nonempty
hn : n = s.max' ne_1
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
ne :
  ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
apply :
  Finset.Nonempty (α := ℕ)
    (Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
      Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y))
⊢ False
have apply₁ : Finset.max'
    (Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
      Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y))
    sorry <
  n
Tactic: apply ne (ih _ _ _ rfl (inj _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne_1 : s.Nonempty
hn : n = s.max' ne_1
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
ne :
  ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
apply :
  Finset.Nonempty (α := ℕ)
    (Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
      Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y))
apply₁ :
  Finset.max'
      (Finsupp.support.{0, u_4} (M := P)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
        Finsupp.support.{0, u_4} (M := P)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y))
      ⋯ <
    n
⊢ False
have apply₂ : Eq.{u_2 + 1} (α := M)
  ((f : (a : P × M) → M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x) :
        P × M) :
    M)
  ((f : (a : P × M) → M)
      ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y) :
        P × M) :
    M)
Tactic: apply ne (ih _ _ _ rfl (inj _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne_1 : s.Nonempty
hn : n = s.max' ne_1
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
ne :
  ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
⊢ Finset.Nonempty (α := ℕ)
    (Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
      Finsupp.support.{0, u_4} (M := P)
        ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y))
have contrapose! : ∀
  (ne :
    Eq (α := Finset ℕ)
      (Finsupp.support.{0, u_4} (M := P)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x) ∪
        Finsupp.support.{0, u_4} (M := P)
          ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y))
      ∅),
  Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
    ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) sorry : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
Tactic: contrapose! ne
Cleared hypotheses: ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
        Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
            ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
          x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne_1 : s.Nonempty
hn : n = s.max' ne_1
eq :
  Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M)
ne :
  ¬Eq (α := ℕ →₀ P) ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x : ℕ →₀ P)
      ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y : ℕ →₀ P)
⊢ Eq.{u_2 + 1} (α := M)
    ((f : (a : P × M) → M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M)
            ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) x) :
          P × M) :
      M)
    ((f : (a : P × M) → M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M)
            ((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ x + 1) ⋯ : (a : ℕ →₀ P) → ℕ →₀ P) y) :
          P × M) :
      M)
have simp_rw : Eq.{u_2 + 1} (α := M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x).2
  ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).2
Tactic: simp_rw [← snd_prodOfFinsuppNat, eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
f : P × M →ₗ[R] M
inj : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
n : ℕ
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty) (hn : n = s.max' ne),
      Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
          ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
        x = y
have inr : ∀ (n : ℕ)
  (ih :
    ∀ m < n,
      ∀ ⦃x y : ℕ →₀ P⦄,
        let s := x.support ∪ y.support;
        ∀ (ne : s.Nonempty) (hn : m = s.max' ne),
          Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
              ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
            x = y)
  ⦃x y : ℕ →₀ P⦄,
  let s := x.support ∪ y.support;
  ∀ (ne : s.Nonempty) (hn : n = s.max' ne),
    Eq (α := P × M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x : P × M)
        ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y : P × M) →
      x = y
Tactic: induction n using Nat.strong_induction_on with | h n ih =>
  intro x y s _ hn eq
  rw [← x.single_add_erase 0, ← y.single_add_erase 0]
  simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq]
  congr 2
  by_contra ne
  apply ne (ih _ _ _ rfl (inj _))
  · contrapose! ne; simp_all [-comapDomain_support]
  · simp +contextual [hn, s, ← Nat.succ_le_iff, Finset.le_max']
  simp_rw [← snd_prodOfFinsuppNat, eq]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id
have h : ∀ (x y : α),
  Eq.{u_1 + 1} (α := R)
    (((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun (i : α) ↦ R) x : (a : R) → α → R) 1 y : R)
    (((id ∘ₗ single R (fun (i : α) ↦ R) x : R →ₗ[R] α → R) : (a : R) → α → R) 1 y : R)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
x y : α
⊢ Eq.{u_1 + 1} (α := R)
    (((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun (i : α) ↦ R) x : (a : R) → α → R) 1 y : R)
    (((id ∘ₗ single R (fun (i : α) ↦ R) x : R →ₗ[R] α → R) : (a : R) → α → R) 1 y : R)
have h : Eq.{u_1 + 1} (α := R)
  ((f : (a : M) → α → R)
      (sum
        ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : (i : α) → R) → α →₀ R)
          (Pi.single (M := fun (i : α) ↦ R) x 1))
        fun (x : α) (r : R) ↦
        r •
          sorry.choose (p := fun (a : M) ↦
            Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R)))
      y :
    R)
  (Pi.single (M := fun (i : α) ↦ R) x 1 y : R)
Tactic: dsimp [splittingOfFunOnFintypeSurjective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
x y : α
⊢ Eq.{u_1 + 1} (α := R)
    ((f : (a : M) → α → R)
        (sum
          ((LinearEquiv.symm (linearEquivFunOnFinite R R α) : (a : (i : α) → R) → α →₀ R)
            (Pi.single (M := fun (i : α) ↦ R) x 1))
          fun (x : α) (r : R) ↦
          r •
            ⋯.choose (p := fun (a : M) ↦
              Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R)))
        y :
      R)
    (Pi.single (M := fun (i : α) ↦ R) x 1 y : R)
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
    (sorry.choose (p := fun (a : M) ↦
      Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R))) =
  0
Tactic: rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
x y : α
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0
      (⋯.choose (p := fun (a : M) ↦
        Eq (α := α → R) ((f : (a : M) → α → R) a : α → R) ((⇑(Finsupp.single x 1) : (a : α) → R) : (a : α) → R))) =
    0
have h : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Pi (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
inst_3 : Finite α
f : M →ₗ[R] α → R
s : Surjective (α := M) (β := α → R) (⇑f : (a : M) → α → R)
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id
have h : ∀ (x y : α),
  Eq.{u_1 + 1} (α := R)
    (((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun (i : α) ↦ R) x : (a : R) → α → R) 1 y : R)
    (((id ∘ₗ single R (fun (i : α) ↦ R) x : R →ₗ[R] α → R) : (a : R) → α → R) 1 y : R)
Tactic: classical
  ext x y
  dsimp [splittingOfFunOnFintypeSurjective]
  rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
  rw [zero_smul]