awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
rw :
  (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i))
            ((coeLinearMap A : (a : ⨁ (i : ι), ↥(A i)) → M)
              (((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i))
                  x :
                ⨁ (i : ι), ↥(A i))) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
have rw₁ : ((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
        ⨁ (i : ι), ↥(A i)) :
      (a : ι) → ↥(A a))
    j =
  0
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_of_ne i j _ hij.symm]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
i j : ι
hij : i ≠ j
x : ↥(A i)
rw :
  (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i))
            ((coeLinearMap A : (a : ⨁ (i : ι), ↥(A i)) → M)
              (((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i))
                  x :
                ⨁ (i : ι), ↥(A i))) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
rw₁ :
  ((((of.{v, u_1} (fun (i : ι) ↦ ↥(A i)) i : ↥(A i) →+ ⨁ (i : ι), ↥(A i)) : (a : ↥(A i)) → ⨁ (i : ι), ↥(A i)) x :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) (↑x : M) :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0
have rw₂ : Eq.{u_1 + 1} (α := ↥(A j)) 0 0
Tactic: rw [← coeLinearMap_of, LinearEquiv.ofBijective_symm_apply_apply, of_eq_of_ne i j _ hij.symm]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤
have rw : Function.Surjective (α := Π₀ (i : ι), ↥(A i)) (β := M)
  (⇑((DFinsupp.lsum ℕ (M := fun (i : ι) ↦ ↥(A i)) : (a : (i : ι) → ↥(A i) →ₗ[R] M) → (Π₀ (i : ι), ↥(A i)) →ₗ[R] M)
        fun (i : ι) ↦ (A i).subtype) :
    (a : Π₀ (i : ι), ↥(A i)) → M)
Tactic: rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis.{u_2, u, u_1} (α i) R ↥(A i)
x : M
i : ι
a : α i
hx : x ∈ A i
⊢ Eq.{u + 1} (α := R)
    (((((h.collectedBasis (α := α) v).repr : (a : M) → (i : ι) × α i →₀ R) x : (i : ι) × α i →₀ R) :
          (a : (i : ι) × α i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ α i) i a) :
      R)
    (((((v i).repr : (a : ↥(A i)) → α i →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ A i) x hx) :
            Finsupp.{u_2, u} (α i) R) :
          (a : α i) → R)
        a :
      R)
have change : Eq.{u + 1} (α := R)
  ((((LinearEquiv.symm (sigmaFinsuppLequivDFinsupp R (η := α)) : (a : Π₀ (i : ι), α i →₀ R) → (i : ι) × α i →₀ R)
            (DFinsupp.mapRange (β₁ := fun (i : ι) ↦ ↥(A i)) (β₂ := fun (i : ι) ↦ Finsupp.{u_2, u} (α i) R)
              (fun (i : ι) ↦ (⇑(v i).repr : (a : ↥(A i)) → α i →₀ R)) sorry
              (((↑(LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h)) : M →ₗ[R] ⨁ (i : ι), ↥(A i)) :
                  (a : M) → ⨁ (i : ι), ↥(A i))
                x)) :
          (i : ι) × α i →₀ R) :
        (a : (i : ι) × α i) → R)
      (Sigma.mk (β := fun (i : ι) ↦ α i) i a) :
    R)
  (((((v i).repr : (a : ↥(A i)) → α i →₀ R) (Subtype.mk (p := fun (x : M) ↦ x ∈ A i) x hx) : Finsupp.{u_2, u} (α i) R) :
        (a : α i) → R)
      a :
    R)
Tactic: change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis.{u_2, u, u_1} (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ Eq.{u + 1} (α := R)
    (((((h.collectedBasis (α := α) v).repr : (a : M) → (i : ι) × α i →₀ R) x : (i : ι) × α i →₀ R) :
          (a : (i : ι) × α i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ α i) j a) :
      R)
    (0 : R)
have change : Eq.{u + 1} (α := R)
  ((((LinearEquiv.symm (sigmaFinsuppLequivDFinsupp R (η := α)) : (a : Π₀ (i : ι), α i →₀ R) → (i : ι) × α i →₀ R)
            (DFinsupp.mapRange (β₁ := fun (i : ι) ↦ ↥(A i)) (β₂ := fun (i : ι) ↦ Finsupp.{u_2, u} (α i) R)
              (fun (i : ι) ↦ (⇑(v i).repr : (a : ↥(A i)) → α i →₀ R)) sorry
              (((↑(LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h)) : M →ₗ[R] ⨁ (i : ι), ↥(A i)) :
                  (a : M) → ⨁ (i : ι), ↥(A i))
                x)) :
          (i : ι) × α i →₀ R) :
        (a : (i : ι) × α i) → R)
      (Sigma.mk (β := fun (i : ι) ↦ α i) j a) :
    R)
  (0 : R)
Tactic: change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j
have rw : iSup A = sSup {A i, A j}
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
rw : iSup A = sSup {A i, A j}
⊢ iSup A = A i ⊔ A j
have rw₁ : sSup (Set.range A) = sSup {A i, A j}
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
rw : iSup A = sSup {A i, A j}
rw₁ : sSup (Set.range A) = sSup {A i, A j}
⊢ iSup A = A i ⊔ A j
have rw₂ : sSup (A '' Set.univ) = sSup {A i, A j}
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
rw : iSup A = sSup {A i, A j}
rw₁ : sSup (Set.range A) = sSup {A i, A j}
rw₂ : sSup (A '' Set.univ) = sSup {A i, A j}
⊢ iSup A = A i ⊔ A j
have rw₃ : sSup (A '' {i, j}) = sSup {A i, A j}
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
rw : iSup A = sSup {A i, A j}
rw₁ : sSup (Set.range A) = sSup {A i, A j}
rw₂ : sSup (A '' Set.univ) = sSup {A i, A j}
rw₃ : sSup (A '' {i, j}) = sSup {A i, A j}
⊢ iSup A = A i ⊔ A j
have rw₄ : sSup (insert (A i) (A '' {j})) = sSup {A i, A j}
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
hi : IsInternal A
rw : iSup A = sSup {A i, A j}
rw₁ : sSup (Set.range A) = sSup {A i, A j}
rw₂ : sSup (A '' Set.univ) = sSup {A i, A j}
rw₃ : sSup (A '' {i, j}) = sSup {A i, A j}
rw₄ : sSup (insert (A i) (A '' {j})) = sSup {A i, A j}
⊢ iSup A = A i ⊔ A j
have rw₅ : Eq (α := Submodule R M) (sSup {A i, A j}) (sSup {A i, A j})
Tactic: rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (hypothesis)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)
have this : ∀ (k : ι), k = i ∨ k = j
Tactic: have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Eq (α := Set ι) Set.univ {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)
have rw : Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)
Tactic: rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h,
    Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
⊢ IsInternal (S := Submodule R ↥(⨆ i ∈ s, A i)) fun (i : (↑s : Type v)) ↦
    Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))
have refine : iSupIndep.{v + 1, u_1} (α := Submodule R ↥(⨆ i ∈ s, A i)) fun (i : (↑s : Type v)) ↦
  Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))
Tactic: refine (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (hypothesis)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
⊢ iSupIndep.{v + 1, u_1} (α := Submodule R ↥(⨆ i ∈ s, A i)) fun (i : (↑s : Type v)) ↦
    Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))
have hp : ∀ i ∈ s, A i ≤ p
Tactic: have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
this :
  Eq (α := (↑s : Type v) → (↑(Set.Iic p) : Type u_1))
    (Function.comp (β := Submodule R ↥p) (⇑e : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_1))
      fun (i : (↑s : Type v)) ↦ Submodule.comap p.subtype (A (↑i : ι)))
    fun (i : (↑s : Type v)) ↦ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯
⊢ iSupIndep.{v + 1, u_1} (α := Submodule R ↥(⨆ i ∈ s, A i)) fun (i : (↑s : Type v)) ↦
    Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))
have rw : iSupIndep.{v + 1, u_1} (α := (↑(Set.Iic p) : Type u_1)) fun (i : (↑s : Type v)) ↦
  Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry
Tactic: rw [← iSupIndep_map_orderIso_iff e, this]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
⊢ iSupIndep.{v + 1, u_1} (α := Submodule R ↥(⨆ i ∈ s, A i)) fun (i : (↑s : Type v)) ↦
    Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))
have suffices : Eq (α := (↑s : Type v) → (↑(Set.Iic p) : Type u_1))
  (Function.comp (β := Submodule R ↥p) (⇑e : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_1)) fun (i : (↑s : Type v)) ↦
    Submodule.comap p.subtype (A (↑i : ι)))
  fun (i : (↑s : Type v)) ↦ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry
Tactic: suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
    rw [← iSupIndep_map_orderIso_iff e, this]
    exact .of_coe_Iic_comp h
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
⊢ Eq (α := (↑s : Type v) → (↑(Set.Iic p) : Type u_1))
    (Function.comp (β := Submodule R ↥p) (⇑e : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_1))
      fun (i : (↑s : Type v)) ↦ Submodule.comap p.subtype (A (↑i : ι)))
    fun (i : (↑s : Type v)) ↦ Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯
have h₁ : ∀ (i : (↑s : Type v)) (m : M),
  Membership.mem (γ := Submodule R M)
      (↑(Function.comp (β := Submodule R ↥p) (⇑e : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_1))
            (fun (i : (↑s : Type v)) ↦ Submodule.comap p.subtype (A (↑i : ι))) i) :
        Submodule R M)
      m ↔
    m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry) : Submodule R M)
Tactic: ext i m
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
i : (↑s : Type v)
m : M
⊢ Membership.mem (γ := Submodule R M)
      (↑(Function.comp (β := Submodule R ↥p) (⇑e : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_1))
            (fun (i : (↑s : Type v)) ↦ Submodule.comap p.subtype (A (↑i : ι))) i) :
        Submodule R M)
      m ↔
    m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯) : Submodule R M)
have h₁ : m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A (↑i : ι))) ↔
  m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry) : Submodule R M)
Tactic: change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
i : (↑s : Type v)
m : M
⊢ m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A (↑i : ι))) ↔
    m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯) : Submodule R M)
have h₁ : m ∈ p ⊓ A (↑i : ι) ↔ m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry) : Submodule R M)
Tactic: rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Module (goal)
Goal:
R : Type u
inst : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep.{v + 1, u_1} (α := Submodule R M) fun (i : (↑s : Type v)) ↦ A (↑i : ι)
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o (↑(Set.Iic p) : Type u_1) := p.mapIic
i : (↑s : Type v)
m : M
h₁ :
  m ∈ p ⊓ A (↑i : ι) ↔ m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯) : Submodule R M)
⊢ m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A (↑i : ι))) ↔
    m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) ⋯) : Submodule R M)
have h₂ : m ∈ A (↑i : ι) ↔ m ∈ (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ Set.Iic p) (A (↑i : ι)) sorry) : Submodule R M)
Tactic: rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
⊢ 1 * x = x
have suffices : Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
  ((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one) (AddMonoidHom.id (⨁ (i : ι), A i))
Tactic: suffices mulHom A One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
⊢ Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one) (AddMonoidHom.id (⨁ (i : ι), A i))
have H : ∀ (i : ι) (y : A i),
  Eq (α := ⨁ (i : ι), A i)
    (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
      ⨁ (i : ι), A i)
Tactic: apply addHom_ext
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
have H : Eq (α := ⨁ (i : ι), A i)
  ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
            ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
          (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
        (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
    ⨁ (i : ι), A i)
  ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
    ⨁ (i : ι), A i)
Tactic: simp only [One.one]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
have H : Eq (α := ⨁ (i : ι), A i)
  ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
      (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GOne.one (A := A)) xi) :
    ⨁ (i : ι), A i)
  ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
    ⨁ (i : ι), A i)
Tactic: rw [mulHom_of_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
⊢ x * 1 = x
have suffices : Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
  ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one)
  (AddMonoidHom.id (⨁ (i : ι), A i))
Tactic: suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
⊢ Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one)
    (AddMonoidHom.id (⨁ (i : ι), A i))
have H : ∀ (i : ι) (y : A i),
  Eq (α := ⨁ (i : ι), A i)
    (((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
      ⨁ (i : ι), A i)
Tactic: apply addHom_ext
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    (((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
have H : Eq (α := ⨁ (i : ι), A i)
  ((((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
            ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
          (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
        (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
    ⨁ (i : ι), A i)
  ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
    ⨁ (i : ι), A i)
Tactic: simp only [One.one]