awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
hI i hiI
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
exact hI i hiI
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
pos : ∀ (hiI : i ∈ I), b i = 0 i
neg neg₁ : ∀ (hiI : i ∉ I), b i = 0 i
⊢ b i = 0 i

Tactic:
classical
    by_cases hiI : i ∈ I
    · by_cases hiJ : i ∈ J
      · exact (h.le_bot ⟨hiI, hiJ⟩).elim
      · exact hJ i hiJ
    · exact hI i hiI
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f g : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
⊢ ∑ i : ι, (f + g) i ∘ₗ proj (φ := φ) i =
    HAdd.hAdd (α := ((i : ι) → φ i) →ₗ[R] M) (∑ i : ι, f i ∘ₗ proj (φ := φ) i) (∑ i : ι, g i ∘ₗ proj (φ := φ) i)

Tactic:
simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, LinearMap.add_comp, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
c : S
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
⊢ ∑ i : ι, (c • f) i ∘ₗ proj (φ := φ) i =
    HSMul.hSMul (α := S) (β := ((i : ι) → φ i) →ₗ[R] M) ((RingHom.id S : (a : S) → S) c : S)
      (∑ i : ι, f i ∘ₗ proj (φ := φ) i)

Tactic:
simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply]

Premises used: LinearMap.smul_comp, RingHom.id_apply, Finset.smul_sum, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
h :
  ∀ (i : ι) (x : φ i),
    Eq.{v + 1} (α := M)
      (((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i)
              ((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
                  (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
                f)
              i :
            (a : φ i) → M)
          x :
        M)
      ((f i : (a : φ i) → M) x : M)
⊢ (fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i)
      ((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
          (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
        f) =
    f

Tactic:
ext i x
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
⊢ Eq.{v + 1} (α := M)
    (((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i)
            ((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
                (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
              f)
            i :
          (a : φ i) → M)
        x :
      M)
    ((f i : (a : φ i) → M) x : M)

Tactic:
simp [apply_single]

Premises used: LinearMap.apply_single
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
h :
  ∀ (x : (i : ι) → φ i),
    Eq.{v + 1} (α := M)
      (((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
                (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
              ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) :
            (a : (i : ι) → φ i) → M)
          x :
        M)
      ((f : (a : (i : ι) → φ i) → M) x : M)
⊢ (fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
        (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
      ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) =
    f

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
this :
  Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (∑ j : ι, Pi.single (M := φ) j (x j)) : M)
    ((f : (a : (i : ι) → φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    (((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
              (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
            ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) :
          (a : (i : ι) → φ i) → M)
        x :
      M)
    ((f : (a : (i : ι) → φ i) → M) x : M)

Tactic:
simpa [apply_single]

Premises used: LinearMap.apply_single
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
h :
  Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (∑ j : ι, Pi.single (M := φ) j (x j)) : M)
    ((f : (a : (i : ι) → φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    (((fun (f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M) ↦
              (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M))
            ((fun (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι) ↦ f ∘ₗ single R φ i) f) :
          (a : (i : ι) → φ i) → M)
        x :
      M)
    ((f : (a : (i : ι) → φ i) → M) x : M)

Tactic:
suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
S : Type u_1
inst_8 : AddCommMonoid M
inst_9 : Module R M
inst_10 : Fintype ι
inst_11 : Semiring S
inst_12 : Module S M
inst_13 : SMulCommClass R S M
f : ((i : ι) → φ i) →ₗ[R] M
x : (i : ι) → φ i
h h₁ : Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) x : M) ((f : (a : (i : ι) → φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (∑ j : ι, Pi.single (M := φ) j (x j)) : M)
    ((f : (a : (i : ι) → φ i) → M) x : M)

Tactic:
rw [Finset.univ_sum_single]

Premises used: Finset.univ_sum_single
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
⊢ Eq (α := ((i : ι) → φ i) →ₗ[R] M)
    ((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M)
    (∑ i : ι, f i ∘ₗ proj (φ := φ) i : ((i : ι) → φ i) →ₗ[R] M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Fintype ι
inst_7 : Semiring S
inst_8 : Module S M
inst_9 : SMulCommClass R S M
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i : ι
x : φ i
simp_rw :
  Eq.{v + 1} (α := M) ((∑ i : ι, f i ∘ₗ proj (φ := φ) i : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₁ :
  Eq.{v + 1} (α := M) (∑ d : ι, (f d ∘ₗ proj (φ := φ) d : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₂ :
  Eq.{v + 1} (α := M)
    (∑ x_1 : ι,
        (f x_1 : (a : φ x_1) → M) ((proj (φ := φ) x_1 : (a : (i : ι) → φ i) → φ x_1) (Pi.single (M := φ) i x) : φ x_1) :
      M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₃ :
  Eq.{v + 1} (α := M) (∑ x_1 : ι, (f x_1 : (a : φ x_1) → M) (Pi.single (M := φ) i x x_1) : M)
    ((f i : (a : φ i) → M) x : M)
simp_rw₄ :
  Eq.{v + 1} (α := M) (∑ x_1 : ι, Pi.single (M := fun (a : ι) ↦ M) i ((f i : (a : φ i) → M) x) x_1 : M)
    ((f i : (a : φ i) → M) x : M)
⊢ Eq.{v + 1} (α := M)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] M) → ((i : ι) → φ i) →ₗ[R] M) f : ((i : ι) → φ i) →ₗ[R] M) :
          (a : (i : ι) → φ i) → M)
        (Pi.single (M := φ) i x) :
      M)
    ((f i : (a : φ i) → M) x : M)

Tactic:
simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']

Premises used: LinearMap.lsum_apply, LinearMap.proj_apply, LinearMap.comp_apply, LinearMap.apply_single, LinearMap.sum_apply, Fintype.sum_pi_single'
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
S : Type u_1
inst_4 : Fintype ι
inst_5 : Semiring S
inst_6 : (i : ι) → Module.{u_1, i} S (φ i)
inst_7 : ∀ (i : ι), SMulCommClass.{u, u_1, i} R S (φ i)
x : (i : ι) → φ i
⊢ Eq (α := (i : ι) → φ i)
    ((((lsum R φ S : (a : (i : ι) → φ i →ₗ[R] (i : ι) → φ i) → ((i : ι) → φ i) →ₗ[R] (i : ι) → φ i) (single R φ) :
            ((i : ι) → φ i) →ₗ[R] (i : ι) → φ i) :
          (a : (i : ι) → φ i) → (i : ι) → φ i)
        x :
      (i : ι) → φ i)
    ((id : (a : (i : ι) → φ i) → (i : ι) → φ i) x : (i : ι) → φ i)

Tactic:
simp [Finset.univ_sum_single]

Premises used: Finset.univ_sum_single
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h :
  ∀ (i : ι) (x : φ i),
    Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
      ((g : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
⊢ f = g

Tactic:
toAddMonoidHom_injective <| AddMonoidHom.functions_ext _ _ _ h

Premises used: AddMonoidHom.functions_ext, LinearMap.toAddMonoidHom_injective
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
⊢ f = g ↔
    ∀ (i : ι) (x : φ i),
      Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
        ((g : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)

Tactic:
⟨fun h _ _ => h ▸ rfl, pi_ext⟩

Premises used: LinearMap.pi_ext, Eq.rec, Iff.intro, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
⊢ f = g

Tactic:
pi_ext fun i x => ?_

Premises used: LinearMap.pi_ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
refine :
  ∀ (i : ι) (x : φ i),
    Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
      ((g : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
⊢ f = g

Tactic:
refine pi_ext fun i x => ?_

Premises used: LinearMap.pi_ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
i : ι
x : φ i
⊢ Eq.{v + 1} (α := M) ((f ∘ₗ single R φ i : (a : φ i) → M) x : M) ((g ∘ₗ single R φ i : (a : φ i) → M) x : M)

Tactic:
LinearMap.congr_fun (h i) x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
inst_5 : AddCommMonoid M
inst_6 : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
i : ι
x : φ i
⊢ Eq.{v + 1} (α := M) ((f : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)
    ((g : (a : (i : ι) → φ i) → M) (Pi.single (M := φ) i x) : M)

Tactic:
convert! LinearMap.congr_fun (h i) x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
refine_1 :
  ∀ (c : (i : (↑I : Type x)) → φ (↑i : ι)),
    Membership.mem (α := (i : ι) → φ i) (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))
      ((pi (φ := φ) fun (i : ι) ↦
              if h : i ∈ I then
                proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
              else 0 :
            (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : ι) → φ i)
          c :
        (i : ι) → φ i)
refine_2 :
  Eq (α := ((i : (↑I : Type x)) → φ (↑i : ι)) →ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι))
    ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
        proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i))) ∘ₗ
      codRestrict (⨅ i ∈ J, ker (proj (φ := φ) i))
        (pi (φ := φ) fun (i : ι) ↦
          if h : i ∈ I then proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
          else 0)
        ⋯)
    id
refine_3 :
  Eq (α := ↥(⨅ i ∈ J, ker (proj (φ := φ) i)) →ₗ[R] ↥(⨅ i ∈ J, ker (proj (φ := φ) i)))
    (codRestrict (⨅ i ∈ J, ker (proj (φ := φ) i))
        (pi (φ := φ) fun (i : ι) ↦
          if h : i ∈ I then proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
          else 0)
        ⋯ ∘ₗ
      pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
        proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)))
    id
⊢ ↥(⨅ i ∈ J, ker (proj (φ := φ) i)) ≃ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι)

Tactic:
refine
    LinearEquiv.ofLinear (pi fun i => (proj (i : ι)).comp (Submodule.subtype _))
      (codRestrict _ (pi fun i => if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) ?_) ?_ ?_

Premises used: LinearEquiv.ofLinear, Membership.mem, dite, LinearMap.proj, LinearMap.pi, LinearMap.comp, LinearMap.codRestrict, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : (↑I : Type x)) → φ (↑i : ι)
refine_1 :
  ∀ (i : ι) (i_1 : i ∈ J),
    Eq.{i + 1} (α := φ i)
      ((if h : i ∈ I then proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
            else 0 :
            (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ i)
          b :
        φ i)
      (0 : φ i)
⊢ Membership.mem (α := (i : ι) → φ i) (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))
    ((pi (φ := φ) fun (i : ι) ↦
            if h : i ∈ I then
              proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
            else 0 :
          (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : ι) → φ i)
        b :
      (i : ι) → φ i)

Tactic:
simp only [mem_iInf, mem_ker, proj_apply, pi_apply]

Premises used: Submodule.mem_iInf, LinearMap.proj_apply, LinearMap.pi_apply, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : (↑I : Type x)) → φ (↑i : ι)
j : ι
hjJ : j ∈ J
⊢ j ∉ I

Tactic:
have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : (↑I : Type x)) → φ (↑i : ι)
j : ι
hjJ : j ∈ J
this : j ∉ I
refine_1 : Eq.{i + 1} (α := φ j) ((0 : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j) b : φ j) (0 : φ j)
refine_1₁ refine_1₂ : Eq.{i + 1} (α := φ j) 0 0
⊢ Eq.{i + 1} (α := φ j)
    ((if h : j ∈ I then proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j h)
          else 0 :
          (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
        b :
      φ j)
    (0 : φ j)

Tactic:
rw [dif_neg this, zero_apply]

Premises used: LinearMap.zero_apply, dif_neg
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
inst_7 : DecidableEq ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
refine_2 :
  Eq (α := ((i : (↑I : Type x)) → φ (↑i : ι)) →ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι))
    (pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
      if h : True then
        proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)
      else 0)
    id
⊢ Eq (α := ((i : (↑I : Type x)) → φ (↑i : ι)) →ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι))
    ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
        proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i))) ∘ₗ
      codRestrict (⨅ i ∈ J, ker (proj (φ := φ) i))
        (pi (φ := φ) fun (i : ι) ↦
          if h : i ∈ I then proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
          else 0)
        ⋯)
    id

Tactic:
simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]

Premises used: LinearMap.subtype_comp_codRestrict, Subtype.coe_prop, LinearMap.comp_assoc, LinearMap.pi_comp, LinearMap.proj_pi