awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (b : (i : (↑I : Type x)) → φ (↑i : ι)) (j : ι) (hj : j ∈ I),
    Eq.{i + 1} (α := φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))
      ((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 :
            (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι))
          b (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) :
        φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))
      ((id : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι)) b
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) :
        φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))
⊢ 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

Tactic:
ext b ⟨j, hj⟩
-- 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 : ι
hj : j ∈ I
refine_2 :
  eval (β := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j ⋯) b =
    (id : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι)) b
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj)
⊢ Eq.{i + 1} (α := φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))
    ((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 :
          (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι))
        b (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) :
      φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))
    ((id : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι)) b
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) :
      φ (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj) : ι))

Tactic:
simp only [dif_pos,
      LinearMap.coe_proj, LinearMap.pi_apply]

Premises used: dif_pos, LinearMap.coe_proj, LinearMap.pi_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 ι
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 : ι
hj : j ∈ I
⊢ eval (β := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j ⋯) b =
    (id : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι)) b
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj)

Tactic:
rfl
-- 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_3 :
  ∀ (b : (i : ι) → φ i) (hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b),
    Eq (α := ↥(⨅ 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)) :
            (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb) :
        ↥(⨅ i ∈ J, ker (proj (φ := φ) i)))
      ((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb) :
        ↥(⨅ i ∈ J, ker (proj (φ := φ) i)))
⊢ 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

Tactic:
ext1 ⟨b, hb⟩
-- 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
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
refine_3 :
  Eq (α := (i : ι) → φ 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)) :
            (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
      (i : ι) → φ i)
    (↑((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
      (i : ι) → φ i)
⊢ Eq (α := ↥(⨅ 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)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb) :
      ↥(⨅ i ∈ J, ker (proj (φ := φ) i)))
    ((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb) :
      ↥(⨅ i ∈ J, ker (proj (φ := φ) i)))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- 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
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
refine_3 :
  ∀ (j : ι),
    Eq.{i + 1} (α := φ j)
      ((↑((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)) :
                (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
              (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
                Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
          (i : ι) → φ i)
        j)
      ((↑((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
              (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
                Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
          (i : ι) → φ i)
        j)
⊢ Eq (α := (i : ι) → φ 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)) :
            (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
      (i : ι) → φ i)
    (↑((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb)) :
      (i : ι) → φ i)

Tactic:
ext j
-- 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
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
⊢ ∀ i ∈ J, b i = 0

Tactic:
simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb

Premises used: Submodule.mem_iInf, LinearMap.proj_apply, LinearMap.mem_ker, Iff.mp
-- 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
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
⊢ ∀ i ∈ J, b i = 0

Tactic:
have hb : ∀ i ∈ J, b i = 0 := by
      simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
-- 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
hb_1 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
hb : ∀ i ∈ J, b i = 0
refine_3 :
  (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)
      ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
            proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
    b j
⊢ Eq.{i + 1} (α := φ j)
    ((↑((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)) :
              (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
            (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
              Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) :
        (i : ι) → φ i)
      j)
    ((↑((id : (a : ↥(⨅ i ∈ J, (proj i).ker)) → ↥(⨅ i ∈ J, (proj i).ker))
            (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
              Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) :
        (i : ι) → φ i)
      j)

Tactic:
simp only [comp_apply, pi_apply, id_apply, codRestrict_apply]

Premises used: LinearMap.id_apply, LinearMap.comp_apply, LinearMap.pi_apply, LinearMap.codRestrict_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 ι
I J : Set ι
inst_8 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ι) → φ i
hb_1 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
hb : ∀ i ∈ J, b i = 0
pos :
  ∀ (h : j ∈ I),
    (proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j h) :
          (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
        ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
              proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
            (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
      b j
neg :
  ∀ (h : j ∉ I),
    (0 : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
        ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
              proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
            (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
          (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
            Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
      b 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)
      ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
            proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
    b j

Tactic:
split_ifs with h
-- 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
hb_1 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∈ I
⊢ (proj (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j h) :
        (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
      ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
            proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
    b j

Tactic:
rfl
-- 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
hb_1 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ (0 : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
      ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
            proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
    b j

Tactic:
(hb _ <| (hu trivial).resolve_left h).symm

Premises used: trivial, Or.resolve_left, Eq.symm
-- 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
hb_1 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ (0 : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j)
      ((pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
            proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)) :
          (a : ↥(⨅ i ∈ J, (proj i).ker)) → (i : (↑I : Type x)) → φ (↑i : ι))
        (Subtype.mk (p := fun (x : (i : ι) → φ i) ↦
          Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) x) b hb_1)) =
    b j

Tactic:
exact (hb _ <| (hu trivial).resolve_left h).symm

Premises used: trivial, Or.resolve_left, Eq.symm
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
inst_5 : DecidableEq ι
f : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
c : M₂
i j : ι
b : LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
pos :
  ∀ (h : j = i),
    Eq.{i + 1} (α := φ j)
      ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b j : (a : M₂) → φ j) c : φ j)
      (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)
neg :
  ∀ (h : ¬j = i),
    Eq.{i + 1} (α := φ j)
      ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b j : (a : M₂) → φ j) c : φ j)
      (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)
⊢ Eq.{i + 1} (α := φ j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b j : (a : M₂) → φ j) c : φ j)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)

Tactic:
by_cases h : j = i
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
inst_5 : DecidableEq ι
f : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
c : M₂
i j : ι
b : LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
h : j = i
pos :
  Eq.{i + 1} (α := φ i)
    ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b i : (a : M₂) → φ i) c : φ i)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) i : φ i)
pos₁ :
  Eq.{i + 1} (α := φ i) ((b : (a : M₂) → φ i) c : φ i)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) i : φ i)
pos₂ pos₃ : Eq.{i + 1} (α := φ i) ((b : (a : M₂) → φ i) c : φ i) ((b : (a : M₂) → φ i) c : φ i)
⊢ Eq.{i + 1} (α := φ j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b j : (a : M₂) → φ j) c : φ j)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)

Tactic:
rw [h, update_self, update_self]

Premises used: Function.update_self