R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨅ (i : ι) (_ : i ∈ Iᶜ), ker (proj i)) (⨅ (i : ι) (_ : i ∈ Jᶜ), ker (proj i))
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)) (⨆ (i : ι) (_ : i ∈ J), range (stdBasis R φ i))
refine'
  Disjoint.mono (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
    (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) _
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄,
    ((∀ (i : ι), i ∈ Iᶜ → x i = 0) ∧ ∀ (i : ι), i ∈ Jᶜ → x i = 0) → ∀ (a : ι), x a = OfNat.ofNat 0 a
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨅ (i : ι) (_ : i ∈ Iᶜ), ker (proj i)) (⨅ (i : ι) (_ : i ∈ Jᶜ), ker (proj i))
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
  funext_iff]
case intro
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄,
    ((∀ (i : ι), i ∈ Iᶜ → x i = 0) ∧ ∀ (i : ι), i ∈ Jᶜ → x i = 0) → ∀ (a : ι), x a = OfNat.ofNat 0 a
rintro b ⟨hI, hJ⟩ i
case pos
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
⊢ b i = OfNat.ofNat 0 i

case neg
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = OfNat.ofNat 0 i
case intro
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
by_cases hiI : i ∈ I
case pos
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = OfNat.ofNat 0 i

case neg
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : ¬i ∈ J
⊢ b i = OfNat.ofNat 0 i
case pos
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
⊢ b i = OfNat.ofNat 0 i
by_cases hiJ : i ∈ J
no goals
case pos
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = OfNat.ofNat 0 i
exact (h.le_bot ⟨hiI, hiJ⟩).elim
no goals
case neg
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : ¬i ∈ J
⊢ b i = OfNat.ofNat 0 i
exact hJ i hiJ
no goals
case neg
R : Type u_3
ι : Type u_1
inst✝³ : Semiring R
φ : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = OfNat.ofNat 0 i
exact hI i hiI