awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
⊢ let n := s.max' ne;
  n = s.max' ne

Tactic:
set n := s.max' ne with hn

Premises used: Finset.max'
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
inr :
  ∀ (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
⊢ ∀ (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:
_
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
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)
⊢ x = y

Tactic:
rw [← x.single_add_erase 0, ← y.single_add_erase 0]

Premises used: Finsupp.single_add_erase, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
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) ⋯ : (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))
⊢ 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:
simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq]

Premises used: Finsupp.mapDomain_comapDomain_nat_add_one, LinearMap.fst_prodOfFinsuppNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
inr :
  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)
⊢ 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))

Tactic:
congr 2
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
inr :
  ∀
    (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
⊢ 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)

Tactic:
by_contra ne
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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
apply₂ :
  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)
⊢ False

Tactic:
apply ne (ih _ _ _ rfl (inj _))

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
contrapose! :
  ∀
    (ne :
      Eq (α := Finset ℕ)
        (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))
        ∅),
    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))

Tactic:
contrapose! ne
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 (α := Finset ℕ)
    (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))
    ∅
⊢ 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)

Tactic:
simp_all [-comapDomain_support]

Premises used: Finsupp.comapDomain_support
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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.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

Tactic:
simp +contextual [hn, s, ← Nat.succ_le_iff, Finset.le_max']

Premises used: Finset.le_max', Nat.succ_le_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
simp_rw :
  Eq.{u_2 + 1} (α := M) ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) x).2
    ((f.prodOfFinsuppNat : (a : ℕ →₀ P) → P × M) y).2
⊢ 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)

Tactic:
simp_rw [← snd_prodOfFinsuppNat, eq]

Premises used: LinearMap.snd_prodOfFinsuppNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : ℕ
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
⊢ ∀ ⦃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]

Premises used: Finsupp.mapDomain_comapDomain_nat_add_one, Finset.le_max', LinearMap.snd_prodOfFinsuppNat, Finsupp.comapDomain_support, Nat.succ_le_iff, LinearMap.fst_prodOfFinsuppNat
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
⊢ ∃ (g : LinearMap.{u_1, u_1, u_4, u_2} (RingHom.id R) (ℕ →₀ P) M),
    Injective.{u_4 + 1, u_2 + 1} (α := ℕ →₀ P) (β := M) (⇑g : (a : ℕ →₀ P) → M)

Tactic:
⟨f ∘ₗ prodOfFinsuppNat f, inj.comp (prodOfFinsuppNat_injective inj)⟩

Premises used: LinearMap.prodOfFinsuppNat_injective, LinearMap.comp, Function.Injective.comp, LinearMap.prodOfFinsuppNat, Exists.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
Goal:
R : Type u_1
P : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid P
inst_2 : Module R P
n : ℕ
f : (Fin (n + 1) → P) →ₗ[R] Fin n → P
inj : Injective (α := Fin (n + 1) → P) (β := Fin n → P) (⇑f : (a : Fin (n + 1) → P) → Fin n → P)
⊢ ∃ (g : (ℕ →₀ P) →ₗ[R] Fin n → P), Injective (α := ℕ →₀ P) (β := Fin n → P) (⇑g : (a : ℕ →₀ P) → Fin n → P)

Tactic:
have e := LinearEquiv.piCongrLeft R (fun _ ↦ P) (finSuccEquiv n) ≪≫ₗ .piOptionEquivProd _
  exists_finsupp_nat_of_prod_injective (f := f ∘ₗ e.symm.toLinearMap) <| inj.comp e.symm.injective

Premises used: LinearEquiv.symm, LinearMap.exists_finsupp_nat_of_prod_injective, LinearEquiv.piCongrLeft, finSuccEquiv, Function.Injective.comp, LinearEquiv.piOptionEquivProd, LinearEquiv.injective, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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)
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)
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : α
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 •
            ⋯.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)
⊢ 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:
dsimp [splittingOfFunOnFintypeSurjective]

Premises used: LinearMap.splittingOfFunOnFintypeSurjective
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : α
h :
  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
⊢ 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)

Tactic:
rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]

Premises used: Exists.choose_spec, Finsupp.sum_single_index, one_smul, Finsupp.linearEquivFunOnFinite_symm_single, Finsupp.single_eq_pi_single, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Pi
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 : α
h h₁ : Eq.{u_2 + 1} (α := M) 0 0
⊢ 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

Tactic:
rw [zero_smul]

Premises used: zero_smul