awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
inst_5 : DecidableEq ι
f : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
c : M₂
i j : ι
b : LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
h : ¬j = i
neg :
  Eq.{i + 1} (α := φ j) ((f j : (a : M₂) → φ j) c : φ j)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)
neg₁ neg₂ : Eq.{i + 1} (α := φ j) ((f j : (a : M₂) → φ j) c : φ j) ((f j : (a : M₂) → φ j) c : φ j)
⊢ Eq.{i + 1} (α := φ j)
    ((update (β := fun (a : ι) ↦ LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ a)) f i b j : (a : M₂) → φ j) c : φ j)
    (update (β := φ) (fun (i : ι) ↦ (f i : (a : M₂) → φ i) c) i ((b : (a : M₂) → φ i) c) j : φ j)

Tactic:
rw [update_of_ne h, update_of_ne h]

Premises used: Function.update_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 : ι
h :
  ∀ (x : φ i) (j : ι),
    Eq.{i + 1} (α := φ j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
      ((pi (φ := φ) (diag (φ := φ) i) : (a : φ i) → (i : ι) → φ i) x j : φ j)
⊢ Eq (α := φ i →ₗ[R] (i : ι) → φ i) (single R φ i) (pi (φ := φ) (diag (φ := φ) i))

Tactic:
ext x 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 : ι
x : φ i
j : ι
⊢ Eq.{i + 1} (α := φ j) (update (β := φ) (fun (i_1 : ι) ↦ (0 i_1 : (a : φ i) → φ i_1) x) i ((id : (a : φ i) → φ i) x) j)
    (((update (β := fun (a : ι) ↦ φ i →ₗ[R] φ a) 0 i (id : φ i →ₗ[R] φ i) j : φ i →ₗ[R] φ j) : (a : φ i) → φ j) x)

Tactic:
(update_apply 0 x i j _).symm

Premises used: LinearMap.update_apply, OfNat.ofNat, 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 ι
i : ι
x : φ i
j : ι
h : x = (id : (a : φ i) → φ i) x
⊢ Eq.{i + 1} (α := φ j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
    ((pi (φ := φ) (diag (φ := φ) i) : (a : φ i) → (i : ι) → φ i) x j : φ j)

Tactic:
convert! (update_apply 0 x i j _).symm

Premises used: LinearMap.update_apply, OfNat.ofNat, 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 ι
i : ι
x : φ i
j : ι
⊢ x = (id : (a : φ i) → φ i) x

Tactic:
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 (α := Submodule R (φ i)) (ker (single R φ i)) ⊥

Tactic:
ker_eq_bot_of_injective <| Pi.single_injective _

Premises used: Pi.single_injective, LinearMap.ker_eq_bot_of_injective
-- 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 : ι
rw : Eq.{i + 1} (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ pi (φ := φ) (diag (φ := φ) j)) (diag (φ := φ) j i)
rw₁ rw₂ : Eq.{i + 1} (α := φ j →ₗ[R] φ i) (diag (φ := φ) j i) (diag (φ := φ) j i)
⊢ Eq (α := φ j →ₗ[R] φ i) (proj (φ := φ) i ∘ₗ single R φ j) (diag (φ := φ) j i)

Tactic:
rw [single_eq_pi_diag, proj_pi]

Premises used: LinearMap.proj_pi, LinearMap.single_eq_pi_diag
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
rw : ∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0)
| ((f : (a : ι → R) → M₂) x : M₂)

Tactic:
rw [pi_eq_sum_univ x, map_sum]

Premises used: map_sum, pi_eq_sum_univ
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
conv_lhs :
  Eq.{w + 1} (α := M₂)
    (∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0))
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂))
⊢ Eq.{w + 1} (α := M₂) ((f : (a : ι → R) → M₂) x : M₂)
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂) : M₂)

Tactic:
conv_lhs => rw [pi_eq_sum_univ x, map_sum]

Premises used: map_sum, pi_eq_sum_univ
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ Eq.{w + 1} (α := M₂)
    (∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0))
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂))

Tactic:
Finset.sum_congr rfl (fun _ _ => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
refine :
  ∀ (x_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ x_1 →
      (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0) =
        HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)
⊢ Eq.{w + 1} (α := M₂)
    (∑ x_1 : ι, (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0))
    (∑ i : ι, HSMul.hSMul (β := M₂) (x i) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if i = j then 1 else 0 : M₂))

Tactic:
refine Finset.sum_congr rfl (fun _ _ => ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
x_1 : ι
h : Membership.mem (γ := Finset ι) Finset.univ x_1
rw rw₁ :
  HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂) =
    HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)
⊢ (f : (a : ι → R) → M₂) (HSMul.hSMul (β := (j : ι) → R) (x x_1) fun (j : ι) ↦ if x_1 = j then 1 else 0) =
    HSMul.hSMul (β := M₂) (x x_1) ((f : (a : ι → R) → M₂) fun (j : ι) ↦ if x_1 = j then 1 else 0 : M₂)

Tactic:
rw [map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ pi (φ := φ) I p ↔ ∀ i ∈ I, x i ∈ p i

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.pi
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
⊢ pi (φ := φ) ∅ p = ⊤

Tactic:
SetLike.coe_injective <| Set.empty_pi _

Premises used: Set.empty_pi, SetLike.coe_injective
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
s : Set ι
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (pi (φ := φ) s fun (i : ι) ↦ ⊤) ⊤

Tactic:
SetLike.coe_injective <| Set.pi_univ _

Premises used: SetLike.coe_injective, Set.pi_univ
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (pi (φ := φ) Set.univ fun (i : ι) ↦ ⊥) ⊥

Tactic:
le_bot_iff.mp fun _ h ↦ funext fun i ↦ h i trivial

Premises used: le_bot_iff, trivial, funext, Iff.mp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p q : (i : ι) → Submodule R (φ i)
s : Set ι
h : ∀ i ∈ s, p i ≤ q i
⊢ pi (φ := φ) s p ≤ pi (φ := φ) s q

Tactic:
Set.pi_mono h

Premises used: Set.Mem, setOf, Set.Subset, Set.pi, Set.pi_mono
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
h :
  ∀ (x : (i : ι) → φ i),
    Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ I, comap (proj (φ := φ) i) (p i)) x ↔ x ∈ pi (φ := φ) I p
⊢ ⨅ i ∈ I, comap (proj (φ := φ) i) (p i) = pi (φ := φ) I p

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ i ∈ I, comap (proj (φ := φ) i) (p i)) x ↔ x ∈ pi (φ := φ) I p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
h :
  ∀ (x : (i : ι) → φ i),
    Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ (i : ι), comap (proj (φ := φ) i) (p i)) x ↔
      x ∈ pi (φ := φ) Set.univ p
⊢ ⨅ (i : ι), comap (proj (φ := φ) i) (p i) = pi (φ := φ) Set.univ p

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ (i : ι), comap (proj (φ := φ) i) (p i)) x ↔
    x ∈ pi (φ := φ) Set.univ p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
inl : ∀ ⦃x : φ j⦄ (hx : x ∈ p j), Membership.mem (α := φ j) (p j) ((single R φ j : (a : φ j) → (i : ι) → φ i) x j : φ j)
inr : ∀ (hne : j ≠ i), Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)
⊢ Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)

Tactic:
rcases eq_or_ne j i with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
j : ι
x : φ j
hx : x ∈ p j
⊢ Membership.mem (α := φ j) (p j) ((single R φ j : (a : φ j) → (i : ι) → φ i) x j : φ j)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
j : ι
hne : j ≠ i
⊢ Membership.mem (α := φ j) (p j) ((single R φ i : (a : φ i) → (i : ι) → φ i) x j : φ j)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
⊢ ⨆ (i : ι), map (single R φ i) (p i) ≤ pi (φ := φ) I p

Tactic:
iSup_le fun _ => map_le_iff_le_comap.mpr <| le_comap_single_pi _

Premises used: Iff.mpr, Set.Mem, iSup_le, Submodule.le_comap_single_pi, Submodule.map_le_iff_le_comap
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
intro : ∀ (val : Fintype ι), ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p
⊢ ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
⊢ ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p

Tactic:
iSup_map_single_le.antisymm fun x hx => ?_

Premises used: Submodule.iSup_map_single_le, LE.le.antisymm
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
intro :
  ∀ (x : (i : ι) → φ i) (hx : x ∈ pi (φ := φ) Set.univ p),
    Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i)) x
⊢ ⨆ (i : ι), map (single R φ i) (p i) = pi (φ := φ) Set.univ p

Tactic:
refine iSup_map_single_le.antisymm fun x hx => ?_

Premises used: Submodule.iSup_map_single_le, LE.le.antisymm
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi (φ := φ) Set.univ p
intro :
  Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i))
    (∑ i : ι, Pi.single (M := φ) i (x i))
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i)) x

Tactic:
rw [← Finset.univ_sum_single x]

Premises used: Finset.univ_sum_single
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi (φ := φ) Set.univ p
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i))
    (∑ i : ι, Pi.single (M := φ) i (x i))

Tactic:
sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)

Premises used: trivial, Submodule.sum_mem_iSup, Submodule.mem_map_of_mem
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
p : (i : ι) → Submodule R (φ i)
inst_3 : DecidableEq ι
inst_4 : Finite ι
val : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi (φ := φ) Set.univ p
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨆ (i : ι), map (single R φ i) (p i))
    (∑ i : ι, Pi.single (M := φ) i (x i))

Tactic:
exact sum_mem_iSup fun i => mem_map_of_mem (hx i trivial)

Premises used: trivial, Submodule.sum_mem_iSup, Submodule.mem_map_of_mem
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
⊢ (f.compLeft I).ker = Submodule.pi (φ := fun (x : I) ↦ M) Set.univ fun (x : I) ↦ f.ker

Tactic:
Submodule.ext fun _ => ⟨fun (hx : _ = _) i _ => congr_fun hx i,
    fun hx => funext fun i => hx i trivial⟩

Premises used: trivial, funext, Iff.intro, congr_fun, Submodule.ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
x : I → M₂
hx : Membership.mem (γ := Submodule R (I → M₂)) (Submodule.pi (φ := fun (x : I) ↦ M₂) Set.univ fun (x : I) ↦ f.range) x
choose :
  ∀ (y : (i : I) → Membership.mem (γ := Set I) Set.univ i → M)
    (hy : ∀ (i : I) (a : Membership.mem (γ := Set I) Set.univ i), (f : (a : M) → M₂) (y i a) = x i),
    x ∈ (f.compLeft I).range
⊢ x ∈ (f.compLeft I).range

Tactic:
choose y hy using hx
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
x : I → M₂
y : (i : I) → Membership.mem (γ := Set I) Set.univ i → M
hy : ∀ (i : I) (a : Membership.mem (γ := Set I) Set.univ i), (f : (a : M) → M₂) (y i a) = x i
⊢ x ∈ (f.compLeft I).range

Tactic:
⟨fun i => y i trivial, funext fun i => hy i trivial⟩

Premises used: trivial, Set.Mem, setOf, funext, Exists.intro, Set.range
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
x : I → M₂
y : (i : I) → Membership.mem (γ := Set I) Set.univ i → M
hy : ∀ (i : I) (a : Membership.mem (γ := Set I) Set.univ i), (f : (a : M) → M₂) (y i a) = x i
⊢ x ∈ (f.compLeft I).range

Tactic:
exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩
-- 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
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R (χ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
c : R
f : (i : ι) → φ i
h :
  ∀ (x : ι),
    (e x : (a : φ x) → ψ x) ((c • f) x) =
      HSMul.hSMul (α := R) (β := (i : ι) → ψ i) ((RingHom.id R : (a : R) → R) c : R)
        (fun (i : ι) ↦ (e i : (a : φ i) → ψ i) (f i)) x
⊢ (fun (i : ι) ↦ (e i : (a : φ i) → ψ i) ((c • f) i)) =
    HSMul.hSMul (α := R) (β := (i : ι) → ψ i) ((RingHom.id R : (a : R) → R) c : R) fun (i : ι) ↦
      (e i : (a : φ i) → ψ i) (f i)

Tactic:
ext
-- 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
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R (χ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
c : R
f : (i : ι) → φ i
x : ι
⊢ (e x : (a : φ x) → ψ x) ((c • f) x) =
    HSMul.hSMul (α := R) (β := (i : ι) → ψ i) ((RingHom.id R : (a : R) → R) c : R)
      (fun (i : ι) ↦ (e i : (a : φ i) → ψ i) (f i)) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
f : (i : ι) → φ i
i : ι
⊢ Eq.{u_2 + 1} (α := ψ i) ((piCongrRight (φ := φ) (ψ := ψ) e : (a : (i : ι) → φ i) → (i : ι) → ψ i) f i : ψ i)
    ((e i : (a : φ i) → ψ i) (f i) : ψ i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
⊢ Eq (α := ((i : ι) → φ i) ≃ₗ[R] (i : ι) → φ i) (piCongrRight (φ := φ) (ψ := φ) fun (j : ι) ↦ refl R (φ j))
    (refl R ((i : ι) → φ i))

Tactic:
rfl

Premises used: LinearEquiv.piCongrRight, LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
⊢ (piCongrRight (φ := φ) (ψ := ψ) e).symm = piCongrRight (φ := ψ) (ψ := φ) fun (i : ι) ↦ (e i).symm

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.piCongrRight, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R (χ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
f : (i : ι) → LinearEquiv.{u, u, u_2, u_3} (RingHom.id R) (ψ i) (χ i)
⊢ piCongrRight (φ := φ) (ψ := ψ) e ≪≫ₗ piCongrRight (φ := ψ) (ψ := χ) f =
    piCongrRight (φ := φ) (ψ := χ) fun (i : ι) ↦ e i ≪≫ₗ f i

Tactic:
rfl

Premises used: LinearEquiv.piCongrRight, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type u_4
κ : ι → Type u_5
α : (i : ι) → κ i → Type u_6
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (α i k)
inst_2 : (i : ι) → (k : κ i) → Module.{u, u_6} R (α i k)
f : (x : (i : ι) × κ i) → α (x.fst (β := fun (i : ι) ↦ κ i)) (x.snd (β := fun (i : ι) ↦ κ i))
⊢ (piCurry R (κ := κ) α : (a : (i : Sigma κ) → α i.fst i.snd) → (i : ι) → (j : κ i) → α i j) f =
    Sigma.curry (β := fun (i : ι) ↦ κ i) (γ := α) f

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type u_4
κ : ι → Type u_5
α : (i : ι) → κ i → Type u_6
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (α i k)
inst_2 : (i : ι) → (k : κ i) → Module.{u, u_6} R (α i k)
f : (a : ι) → (b : κ a) → α a b
⊢ (symm (piCurry R (κ := κ) α) : (a : (i : ι) → (j : κ i) → α i j) → (i : Sigma κ) → α i.fst i.snd) f =
    Sigma.uncurry (β := κ) (γ := α) f

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι_1 : Type x
ι' : Type x'
inst : Semiring R
φ : ι_1 → Type u_1
ψ : ι_1 → Type u_2
χ : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommMonoid (φ i)
inst_2 : (i : ι_1) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι_1) → AddCommMonoid (ψ i)
inst_4 : (i : ι_1) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι_1) → AddCommMonoid (χ i)
inst_6 : (i : ι_1) → Module.{u, u_3} R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst_7 : (i : Option ι) → AddCommMonoid (M i)
inst_8 : (i : Option ι) → Module.{u, u_5} R (M i)
⊢ ∀ (x y : (i : Option ι) → M i),
    Equiv.toFun (Equiv.piOptionEquivProd (β := M)) (x + y) =
      Equiv.toFun (Equiv.piOptionEquivProd (β := M)) x + Equiv.toFun (Equiv.piOptionEquivProd (β := M)) y

Tactic:
simp [funext_iff]

Premises used: funext_iff