awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Module
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 : M
hx : x ∈ A i
⊢ (((LinearEquiv.symm (LinearEquiv.ofBijective (coeLinearMap A) h) : (a : M) → ⨁ (i : ι), ↥(A i)) x :
          ⨁ (i : ι), ↥(A i)) :
        (a : ι) → ↥(A a))
      j =
    0

Tactic:
h.ofBijective_coeLinearMap_of_ne hij ⟨x, hx⟩

Premises used: Subtype.mk, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne
-- Module: Mathlib.Algebra.DirectSum.Module
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
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)
⊢ iSup A = ⊤

Tactic:
rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ 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:
Function.Bijective.surjective h

Premises used: Function.Bijective.surjective
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ 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:
exact Function.Bijective.surjective h

Premises used: Function.Bijective.surjective
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ iSupIndep A

Tactic:
iSupIndep_of_dfinsupp_lsum_injective _ h.injective

Premises used: Function.Bijective.injective, iSupIndep_of_dfinsupp_lsum_injective
-- Module: Mathlib.Algebra.DirectSum.Module
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)
⊢ Eq (α := (a : (i : ι) × α i) → M) (⇑(h.collectedBasis (α := α) v) : (a : (i : ι) × α i) → M) fun (a : (i : ι) × α i) ↦
    (↑((v (a.fst (β := fun (i : ι) ↦ α i)) : (a_1 : α a.fst) → ↥(A a.fst)) (a.snd (β := fun (i : ι) ↦ α i))) : M)

Tactic:
simp [IsInternal.collectedBasis, coeLinearMap, DFinsupp.mapRange.linearEquiv,
    toModule, DFinsupp.lsum]

Premises used: DFinsupp.lsum, DirectSum.IsInternal.collectedBasis, DirectSum.toModule, DFinsupp.mapRange.linearEquiv, DirectSum.coeLinearMap
-- Module: Mathlib.Algebra.DirectSum.Module
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)
a : (i : ι) × α i
⊢ Membership.mem (α := M) (A (a.fst (β := fun (i : ι) ↦ α i)))
    ((h.collectedBasis (α := α) v : (a : (i : ι) × α i) → M) a : M)

Tactic:
simp
-- Module: Mathlib.Algebra.DirectSum.Module
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
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)) ⋯
                (((↑(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)
⊢ 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)

Tactic:
change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _

Premises used: LinearEquiv.symm, sigmaFinsuppLequivDFinsupp, map_zero, DFinsupp.mapRange, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Module
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)
    ((((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)) ⋯
                (((↑(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:
simp [h.ofBijective_coeLinearMap_of_mem hx]

Premises used: DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem
-- Module: Mathlib.Algebra.DirectSum.Module
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
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)) ⋯
                (((↑(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)
⊢ 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)

Tactic:
change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _

Premises used: LinearEquiv.symm, sigmaFinsuppLequivDFinsupp, map_zero, DFinsupp.mapRange, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Module
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)
    ((((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)) ⋯
                (((↑(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:
simp [h.ofBijective_coeLinearMap_of_mem_ne hij hx]

Premises used: DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne
-- Module: Mathlib.Algebra.DirectSum.Module
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}
rw₅ rw₆ : Eq (α := Submodule R M) (sSup {A i, A j}) (sSup {A i, A j})
⊢ iSup A = A i ⊔ A j

Tactic:
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]

Premises used: Set.image_univ, Set.image_singleton, iSup, sSup_pair, Set.image_insert_eq
-- Module: Mathlib.Algebra.DirectSum.Module
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
hi : iSupIndep A
hs : iSup A = ⊤
⊢ IsInternal A

Tactic:
⟨hi.dfinsupp_lsum_injective,
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify value of `f`
    (LinearMap.range_eq_top (f := DFinsupp.lsum _ _)).1 <|
      (Submodule.iSup_eq_range_dfinsupp_lsum _).symm.trans hs⟩

Premises used: iSupIndep.dfinsupp_lsum_injective, DirectSum.IsInternal, Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top, And.intro, Iff.mp, Function.Bijective, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ IsInternal A ↔ iSupIndep A ∧ iSup A = ⊤

Tactic:
⟨fun i ↦ ⟨i.submodule_iSupIndep, i.submodule_iSup_eq_top⟩,
    And.rec isInternal_submodule_of_iSupIndep_of_iSup_eq_top⟩

Premises used: DirectSum.IsInternal.submodule_iSupIndep, And.rec, And.intro, Iff.intro, DirectSum.IsInternal.submodule_iSup_eq_top
-- Module: Mathlib.Algebra.DirectSum.Module
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}
k : ι
⊢ k = i ∨ k = j

Tactic:
simpa using Set.ext_iff.mp h k

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Algebra.DirectSum.Module
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}
⊢ ∀ (k : ι), k = i ∨ k = j

Tactic:
have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
-- Module: Mathlib.Algebra.DirectSum.Module
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
rw : Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)
⊢ IsInternal A ↔ 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]

Premises used: Set.image_univ, Set.image_singleton, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, iSupIndep_pair, sSup_pair, Set.image_insert_eq
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩

Premises used: Iff.mpr, codisjoint_iff, Disjoint, _private.0.DirectSum.isInternal_submodule_iff_isCompl.match_1, And, IsCompl, Max.max, And.intro, Iff.intro, _private.0.DirectSum.isInternal_submodule_iff_isCompl.match_2, IsCompl.mk, Top.top, Eq, Codisjoint.eq_top
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ (IsInternal (S := Submodule R M) fun (i : { i : ι // A i ≠ ⊥ }) ↦ A (↑i : ι)) ↔ IsInternal A

Tactic:
simp [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top]

Premises used: DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top
-- Module: Mathlib.Algebra.DirectSum.Module
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 : ι)
⊢ Eq.{u_1 + 1} (α := Submodule R ↥(⨆ i ∈ s, A i))
    (⨆ (i : (↑s : Type v)), Submodule.comap (Submodule.subtype (⨆ i ∈ s, A i)) (A (↑i : ι))) ⊤

Tactic:
simp [iSup_subtype]

Premises used: iSup_subtype
-- Module: Mathlib.Algebra.DirectSum.Module
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 : ι)
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 : ι))
⊢ IsInternal (S := 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]⟩

Premises used: Iff.mpr, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, And.intro
-- Module: Mathlib.Algebra.DirectSum.Module
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
⊢ ∀ i ∈ s, A i ≤ p

Tactic:
have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi
-- Module: Mathlib.Algebra.DirectSum.Module
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 : ι)) ⋯
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 : ι)) ⋯
⊢ 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:
rw [← iSupIndep_map_orderIso_iff e, this]

Premises used: iSupIndep_map_orderIso_iff
-- Module: Mathlib.Algebra.DirectSum.Module
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} (α := (↑(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 : ι)) ⋯

Tactic:
.of_coe_Iic_comp h

Premises used: iSupIndep.of_coe_Iic_comp
-- Module: Mathlib.Algebra.DirectSum.Module
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} (α := (↑(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 : ι)) ⋯

Tactic:
exact .of_coe_Iic_comp h
-- Module: Mathlib.Algebra.DirectSum.Module
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
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 : ι)) ⋯
⊢ 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:
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
-- Module: Mathlib.Algebra.DirectSum.Module
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
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 : ι)) ⋯) : Submodule R M)
⊢ 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 : ι)) ⋯

Tactic:
ext i m
-- Module: Mathlib.Algebra.DirectSum.Module
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 ∈ 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)
⊢ 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)

Tactic:
change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _

Premises used: Submodule.comap, Submodule.subtype, Submodule.map, Subtype.val
-- Module: Mathlib.Algebra.DirectSum.Module
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)
h₂ h₃ :
  m ∈ 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)

Tactic:
rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]

Premises used: inf_of_le_right, Submodule.map_comap_subtype, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
dec_ι : DecidableEq ι
M : Type u_2
inst : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSupIndep A

Tactic:
iSupIndep_of_dfinsuppSumAddHom_injective _ h.injective

Premises used: Function.Bijective.injective, iSupIndep_of_dfinsuppSumAddHom_injective
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
dec_ι : DecidableEq ι
G : Type u_2
inst : AddCommGroup G
A : ι → AddSubgroup G
h : IsInternal A
⊢ iSupIndep A

Tactic:
iSupIndep_of_dfinsuppSumAddHom_injective' _ h.injective

Premises used: iSupIndep_of_dfinsuppSumAddHom_injective', Function.Bijective.injective