awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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
have 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)
Tactic: refine pi_ext fun i x => ?_
-- 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
⊢ ↥(⨅ i ∈ J, ker (proj (φ := φ) i)) ≃ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι)
have 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)
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) ?_) ?_ ?_
-- 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
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)
⊢ ↥(⨅ i ∈ J, ker (proj (φ := φ) i)) ≃ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι)
have 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)
      sorry)
  id
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) ?_) ?_ ?_
-- 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
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
⊢ ↥(⨅ i ∈ J, ker (proj (φ := φ) i)) ≃ₗ[R] (i : (↑I : Type x)) → φ (↑i : ι)
have 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)
      sorry ∘ₗ
    pi (φ := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) fun (i : (↑I : Type x)) ↦
      proj (φ := φ) (↑i : ι) ∘ₗ Submodule.subtype (⨅ i ∈ J, ker (proj (φ := φ) i)))
  id
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) ?_) ?_ ?_
-- 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 : 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)
        b :
      (i : ι) → φ i)
have 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)
Tactic: simp only [mem_iInf, mem_ker, proj_apply, pi_apply]
-- 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 : Type x)) → φ (↑i : ι)
j : ι
hjJ : j ∈ J
⊢ 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)
have this : j ∉ I
Tactic: have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
-- 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 : Type x)) → φ (↑i : ι)
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ 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)
have refine_1 : Eq.{i + 1} (α := φ j) ((0 : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → φ j) b : φ j) (0 : φ j)
Tactic: rw [dif_neg this, zero_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 : 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)
⊢ 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)
have refine_1₁ : Eq.{i + 1} (α := φ j) 0 0
Tactic: rw [dif_neg this, zero_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
⊢ 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
have 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 : ι) sorry)
    else 0)
  id
Tactic: simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]
-- 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
⊢ 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
have 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 : ι) sorry)
            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: ext b ⟨j, hj⟩
-- 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 : 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) : ι))
have refine_2 : eval (β := fun (i : (↑I : Type x)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j sorry) b =
  (id : (a : (i : (↑I : Type x)) → φ (↑i : ι)) → (i : (↑I : Type x)) → φ (↑i : ι)) b
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) j hj)
Tactic: simp only [dif_pos,
      LinearMap.coe_proj, LinearMap.pi_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
⊢ 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
have 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)
              sorry ∘ₗ
            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: ext1 ⟨b, 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 : 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)))
have 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)
              sorry ∘ₗ
            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: apply Subtype.ext
-- 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 : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
⊢ 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)
have 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)
                  sorry ∘ₗ
                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)
Tactic: ext j