awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (hypothesis)
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 : ι
⊢ 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)
have hb₁ : ∀ 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
⊢ 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)
have 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
Tactic: simp only [comp_apply, pi_apply, id_apply, codRestrict_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
⊢ 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)
have 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)
Tactic: rw [h, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ 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)
have pos₂ : Eq.{i + 1} (α := φ i) ((b : (a : M₂) → φ i) c : φ i) ((b : (a : M₂) → φ i) c : φ i)
Tactic: rw [h, update_self, update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
⊢ 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)
have neg : Eq.{i + 1} (α := φ j) ((f 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 [update_of_ne h, update_of_ne h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
neg :
  Eq.{i + 1} (α := φ j) ((f 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)
have neg₁ : Eq.{i + 1} (α := φ j) ((f j : (a : M₂) → φ j) c : φ j) ((f j : (a : M₂) → φ j) c : φ j)
Tactic: rw [update_of_ne h, update_of_ne h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 : ι
⊢ Eq (α := φ i →ₗ[R] (i : ι) → φ i) (single R φ i) (pi (φ := φ) (diag (φ := φ) i))
have h : ∀ (x : φ i) (j : ι),
  Eq.{i + 1} (α := φ j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
    ((pi (φ := φ) (diag (φ := φ) i) : (a : φ i) → (i : ι) → φ i) x j : φ j)
Tactic: ext x j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 : ι
x : φ i
j : ι
⊢ Eq.{i + 1} (α := φ j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
    ((pi (φ := φ) (diag (φ := φ) i) : (a : φ i) → (i : ι) → φ i) x j : φ j)
have h : x = (id : (a : φ i) → φ i) x
Tactic: convert! (update_apply 0 x i j _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 : ι
⊢ Eq (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ single R φ j) (diag (φ := φ) j i)
have rw : Eq.{i + 1} (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ pi (φ := φ) (diag (φ := φ) j)) (diag (φ := φ) j i)
Tactic: rw [single_eq_pi_diag, proj_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 : ι
rw : Eq.{i + 1} (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ pi (φ := φ) (diag (φ := φ) j)) (diag (φ := φ) j i)
⊢ Eq (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ single R φ j) (diag (φ := φ) j i)
have rw₁ : Eq.{i + 1} (α := φ j →ₗ[R] φ i) (diag (φ := φ) j i) (diag (φ := φ) j i)
Tactic: rw [single_eq_pi_diag, proj_pi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
| ((f : (a : ι → R) → M₂) x : M₂)
have rw : ∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0)
Tactic: rw [pi_eq_sum_univ x, map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ Eq.{w + 1} (α := M₂) ((f : (a : ι → R) → M₂) x : M₂)
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂) : M₂)
have conv_lhs : Eq.{w + 1} (α := M₂)
  (∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0))
  (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂))
Tactic: conv_lhs => rw [pi_eq_sum_univ x, map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ Eq.{w + 1} (α := M₂)
    (∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0))
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂))
have refine : ∀ (x_1 : ι),
  Membership.mem (γ := Finset ι) Finset.univ x_1 →
    (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0) =
      HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)
Tactic: refine Finset.sum_congr rfl (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
⊢ (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0) =
    HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)
have rw : HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂) =
  HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i ∈ I, comap (proj (φ := φ) i) (p i) = pi (φ := φ) I p
have h : ∀ (x : (i : ι) → φ i),
  Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ I, comap (proj (φ := φ) i) (p i)) x ↔ x ∈ pi (φ := φ) I p
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ (i : ι), comap (proj (φ := φ) i) (p i) = pi (φ := φ) Set.univ p
have h : ∀ (x : (i : ι) → φ i),
  Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ (i : ι), comap (proj (φ := φ) i) (p i)) x ↔
    x ∈ pi (φ := φ) Set.univ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
⊢ Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
have inl : ∀ ⦃x : φ j⦄ (hx : x ∈ p j), Membership.mem (α := φ j) (p j) ((single R φ j : (a : φ j) → (i : ι) → φ i) x j : φ j)
Tactic: rcases eq_or_ne j i with rfl | hne
Cleared hypotheses: i, x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
inl : ∀ ⦃x : φ j⦄ (hx : x ∈ p j), Membership.mem (α := φ j) (p j) ((single R φ j : (a : φ j) → (i : ι) → φ i) x j : φ j)
⊢ Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
have inr : ∀ (hne : j ≠ i), Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
Tactic: rcases eq_or_ne j i with rfl | hne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
⊢ ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p
have intro : ∀ (val : Fintype ι), ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
⊢ ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p
have intro : ∀ (x : (i : ι) → φ i) (hx : x ∈ pi (φ := φ) Set.univ p),
  Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i)) x
Tactic: refine iSup_map_single_le.antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi (φ := φ) Set.univ p
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i)) x
have intro : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i))
  (∑ i : ι, Pi.single (M := φ) i (x i))
Tactic: rw [← Finset.univ_sum_single x]