awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Pi
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)
f : M₂ →ₗ[R] M₃
I : Type u_1
c : R
h : I → M₂
x : I
⊢ ((⇑f : (a : M₂) → M₃) ∘ (c • h)) x =
    HSMul.hSMul (α := R) (β := I → M₃) ((RingHom.id R : (a : R) → R) c : R) ((⇑f : (a : M₂) → M₃) ∘ h) x

Tactic:
exact f.map_smul' c (h x)

Premises used: LinearMap.map_smul'
-- Module: Mathlib.LinearAlgebra.Pi
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 : AddCommMonoid M
inst_4 : Module R M
inst_5 : DecidableEq ι
f : (i : ι) → LinearMap.{u, u, i, v} (RingHom.id R) (φ i) M
i j : ι
x : φ i
⊢ Eq.{v + 1} (α := M) ((f j : (a : φ j) → M) (Pi.single (M := φ) i x j) : M)
    (Pi.single (M := fun (a : ι) ↦ M) i ((f i : (a : φ i) → M) x) j : M)

Tactic:
Pi.apply_single (fun i => f i) (fun i => (f i).map_zero) _ _ _

Premises used: Pi.apply_single, LinearMap.map_zero, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Pi
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 : ι
v : φ i
⊢ (single R φ i : (a : φ i) → (i : ι) → φ i) v = Pi.single (M := φ) i v

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type x
φ : ι → Type i
inst : (i : ι) → AddCommMonoid (φ i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
v : (i : ι) → φ i
h : ∀ (x : ι), (∑ i : ι, Pi.single (M := φ) i (v i)) x = v x
⊢ ∑ i : ι, Pi.single (M := φ) i (v i) = v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type x
φ : ι → Type i
inst : (i : ι) → AddCommMonoid (φ i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
v : (i : ι) → φ i
x : ι
⊢ (∑ i : ι, Pi.single (M := φ) i (v i)) x = v x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
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 (α := (a : φ i) → (i : ι) → φ i) (⇑(single R φ i) : (a : φ i) → (i : ι) → φ i) (Pi.single (M := φ) i)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.LinearAlgebra.Pi
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) (proj (φ := φ) i ∘ₗ single R φ i) id

Tactic:
LinearMap.ext <| Pi.single_eq_same i

Premises used: LinearMap.ext, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Pi
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 : ι
h : i ≠ j
⊢ Eq (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ single R φ j) 0

Tactic:
LinearMap.ext <| Pi.single_eq_of_ne h

Premises used: LinearMap.ext, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))

Tactic:
iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_

Premises used: Iff.mpr, Set.Mem, LinearMap.range_le_iff_comap, iSup_le
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
refine : ∀ (i : ι) (hi : i ∈ I), Eq (α := Submodule R (φ i)) (comap (single R φ i) (⨅ i ∈ J, ker (proj (φ := φ) i))) ⊤
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))

Tactic:
refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_

Premises used: Iff.mpr, LinearMap.range_le_iff_comap, iSup_le
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
simp :
  ∀ ⦃x : φ i⦄,
    Membership.mem (γ := Submodule R (φ i)) ⊤ x →
      ∀ (i_1 : ι) (i_2 : i_1 ∈ J),
        Eq (α := φ i_1) ((proj (φ := φ) i_1 ∘ₗ single R φ i : (a : φ i) → φ i_1) x : φ i_1) (0 : φ i_1)
⊢ Eq (α := Submodule R (φ i)) (comap (single R φ i) (⨅ i ∈ J, ker (proj (φ := φ) i))) ⊤

Tactic:
simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]

Premises used: Submodule.mem_iInf, eq_top_iff, SetLike.le_def, Submodule.comap_iInf, LinearMap.ker_comp, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
rw : j ≠ i
⊢ Eq (α := φ j) ((proj (φ := φ) j ∘ₗ single R φ i : (a : φ i) → φ j) b : φ j) (0 : φ j)

Tactic:
rw [proj_comp_single_ne R φ j i, zero_apply]

Premises used: LinearMap.zero_apply, LinearMap.proj_comp_single_ne
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
j : ι
hj : j ∈ J
hi : j ∈ I
b : φ j
⊢ False

Tactic:
h.le_bot ⟨hi, hj⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
j : ι
hj : j ∈ J
hi : j ∈ I
b : φ j
⊢ False

Tactic:
exact h.le_bot ⟨hi, hj⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) b
⊢ ∀ (i : ι) (i_1 : i ∈ J), b i = 0

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at hb

Premises used: Submodule.mem_iInf, LinearMap.proj_apply, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
h : ∀ (i : ι), (∑ i ∈ I, Pi.single (M := φ) i (b i)) i = b i
⊢ ∑ i ∈ I, Pi.single (M := φ) i (b i) = b

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
h : ∑ c ∈ I, Pi.single (M := φ) c (b c) i = Pi.single (M := φ) i (b i) i
⊢ (∑ i ∈ I, Pi.single (M := φ) i (b i)) i = b i

Tactic:
rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]

Premises used: Finset.sum_apply, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single (M := φ) c (b c) i = Pi.single (M := φ) i (b i) i

Tactic:
Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_

Premises used: Pi.single_eq_of_ne, Ne.symm, Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
h : i ∉ I → Pi.single (M := φ) i (b i) i = 0
⊢ ∑ c ∈ I, Pi.single (M := φ) c (b c) i = Pi.single (M := φ) i (b i) i

Tactic:
refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
hiI : i ∉ I
h : b i = 0
⊢ Pi.single (M := φ) i (b i) i = 0

Tactic:
rw [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0

Tactic:
hb _ ((hu trivial).resolve_left hiI)

Premises used: trivial, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0

Tactic:
exact hb _ ((hu trivial).resolve_left hiI)

Premises used: trivial, Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
rw :
  Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i))
    (∑ i ∈ I, Pi.single (M := φ) i (b i))
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) b

Tactic:
rw [←
        show (∑ i ∈ I, Pi.single i (b i)) = b by
          ext i
          rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
          refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
          intro hiI
          rw [Pi.single_eq_same]
          exact hb _ ((hu trivial).resolve_left hiI)]
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i))
    (∑ i ∈ I, Pi.single (M := φ) i (b i))

Tactic:
sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i)

Premises used: LinearMap.single, LinearMap.mem_range_self, Submodule.sum_mem_biSup
-- Module: Mathlib.LinearAlgebra.Pi
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 : Finset ι
J : Set ι
hu : Set.univ ⊆ (↑I : Set ι) ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι) (i_1 : i ∈ J), b i = 0
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i))
    (∑ i ∈ I, Pi.single (M := φ) i (b i))

Tactic:
exact sum_mem_biSup fun i _ => mem_range_self (single R φ i) (b i)

Premises used: LinearMap.single, LinearMap.mem_range_self, Submodule.sum_mem_biSup
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))

Tactic:
le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_

Premises used: le_antisymm, LinearMap.iSup_range_single_le_iInf_ker_proj
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
refine : LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))

Tactic:
refine le_antisymm (iSup_range_single_le_iInf_ker_proj _ _ _ _ hd) ?_

Premises used: le_antisymm, LinearMap.iSup_range_single_le_iInf_ker_proj
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
rwa rwa₁ rwa₂ rwa₃ : Set.univ ⊆ I ∪ J
⊢ Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J

Tactic:
rwa [hI.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
⊢ Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J

Tactic:
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))

Tactic:
le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)

Premises used: LinearMap.iInf_ker_proj_le_iSup_range_single, iSup_mono, le_trans
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
refine :
  ∀ (i : ι),
    LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ hI.toFinset (s := I)), range (single R φ i))
      (⨆ (_ : i ∈ I), range (single R φ i))
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i)) (⨆ i ∈ I, range (single R φ i))

Tactic:
refine le_trans (iInf_ker_proj_le_iSup_range_single R φ this) (iSup_mono fun i => ?_)

Premises used: LinearMap.iInf_ker_proj_le_iSup_range_single, iSup_mono, le_trans
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : I.Finite
this : Set.univ ⊆ (↑(hI.toFinset (s := I)) : Set ι) ∪ J
i : ι
rw rw₁ :
  LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ I), range (single R φ i)) (⨆ (_ : i ∈ I), range (single R φ i))
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ (_ : i ∈ hI.toFinset (s := I)), range (single R φ i))
    (⨆ (_ : i ∈ I), range (single R φ i))

Tactic:
rw [Set.Finite.mem_toFinset]

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
intro : ∀ (val : Fintype ι), Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
val : Fintype ι
⊢ Eq (α := Submodule R ((i : ι) → φ i))
    (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ i), range (single R φ i)) ⊤

Tactic:
top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)

Premises used: Eq.ge, LinearMap.iInf_ker_proj_le_iSup_range_single, top_unique, LE.le.trans, iInf_emptyset
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
val : Fintype ι
h :
  ∀ (x : ι),
    Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ x))
      (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ x), range (single R φ x))
intro : Finset ι
intro₁ : Set.univ ⊆ (↑Finset.univ : Set ι) ∪ ∅
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), range (single R φ i)) ⊤

Tactic:
convert! top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)

Premises used: Eq.ge, LinearMap.iInf_ker_proj_le_iSup_range_single, top_unique, LE.le.trans, iInf_emptyset
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
val : Fintype ι
i : ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ i))
    (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ i), range (single R φ i))

Tactic:
((@iSup_pos _ _ _ fun _ => range <| single R φ i) <| Finset.mem_univ i).symm

Premises used: Finset.mem_univ, iSup_pos, Eq.symm
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
val : Fintype ι
i : ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (range (single R φ i))
    (⨆ (_ : Membership.mem (γ := Finset ι) Finset.univ i), range (single R φ i))

Tactic:
exact ((@iSup_pos _ _ _ fun _ => range <| single R φ i) <| Finset.mem_univ i).symm

Premises used: Finset.mem_univ, iSup_pos, Eq.symm
-- Module: Mathlib.LinearAlgebra.Pi
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 ι
inst_4 : Finite ι
val : Fintype ι
intro : Subset.{x} (α := Set ι) Set.univ (Set.univ ∪ ∅)
intro₁ intro₂ : Subset.{x} (α := Set ι) Set.univ Set.univ
⊢ Set.univ ⊆ (↑Finset.univ : Set ι) ∪ ∅

Tactic:
rw [Finset.coe_univ, Set.union_empty]

Premises used: Finset.coe_univ, Set.union_empty
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
⊢ Disjoint (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i))

Tactic:
Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_

Premises used: disjoint_compl_right, Disjoint.mono, LinearMap.iSup_range_single_le_iInf_ker_proj
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
_ : Disjoint (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ Iᶜ, ker (proj (φ := φ) i)) (⨅ i ∈ Jᶜ, ker (proj (φ := φ) i))
⊢ Disjoint (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨆ i ∈ J, range (single R φ i))

Tactic:
refine
    Disjoint.mono (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
      (iSup_range_single_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) ?_

Premises used: disjoint_compl_right, Disjoint.mono, LinearMap.iSup_range_single_le_iInf_ker_proj
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
simp :
  ∀ ⦃x : (i : ι) → φ i⦄,
    ((∀ (i : ι) (i_1 : i ∈ Iᶜ), x i = 0) ∧ ∀ (i : ι) (i_1 : i ∈ Jᶜ), x i = 0) → ∀ (x_1 : ι), x x_1 = 0 x_1
⊢ Disjoint (α := Submodule R ((i : ι) → φ i)) (⨅ i ∈ Iᶜ, ker (proj (φ := φ) i)) (⨅ i ∈ Jᶜ, ker (proj (φ := φ) i))

Tactic:
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply,
    funext_iff]

Premises used: Submodule.mem_iInf, Submodule.mem_bot, funext_iff, LinearMap.proj_apply, SetLike.le_def, Submodule.mem_inf, LinearMap.mem_ker, disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
pos : ∀ (hiI : i ∈ I), b i = 0 i
neg : ∀ (hiI : i ∉ I), b i = 0 i
⊢ b i = 0 i

Tactic:
by_cases hiI : i ∈ I
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
pos : ∀ (hiJ : i ∈ J), b i = 0 i
neg : ∀ (hiJ : i ∉ J), b i = 0 i
⊢ b i = 0 i

Tactic:
by_cases hiJ : i ∈ J
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = 0 i

Tactic:
(h.le_bot ⟨hiI, hiJ⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = 0 i

Tactic:
exact (h.le_bot ⟨hiI, hiJ⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
hJ i hiJ
-- Module: Mathlib.LinearAlgebra.Pi
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 : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι) (i_1 : i ∈ Iᶜ), b i = 0
hJ : ∀ (i : ι) (i_1 : i ∈ Jᶜ), b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
exact hJ i hiJ