awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h : (i : ι) → M₁ i
rw :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s ∈ Finset.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (x + h) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
      ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)

Tactic:
rw [add_comm, map_add_univ, ← Finset.powerset_univ,
      ← sum_filter_add_sum_filter_not _ (2 ≤ #·)]

Premises used: LE.le, add_comm, Finset.sum_filter_add_sum_filter_not, Finset.card, OfNat.ofNat, Finset.powerset_univ, MultilinearMap.map_add_univ
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
z z' : M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (z + z') : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((HAdd.hAdd (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z)
            (MultilinearMap.mkPiRing R ι z') :
          (a : (i : ι) → R) → M₂)
        fun (x : ι) ↦ 1 :
      M₂)
⊢ MultilinearMap.mkPiRing R ι (z + z') =
    HAdd.hAdd (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z)
      (MultilinearMap.mkPiRing R ι z')

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
z z' : M₂
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (z + z') : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((HAdd.hAdd (α := MultilinearMap R (fun (x : ι) ↦ R) M₂) (MultilinearMap.mkPiRing R ι z)
            (MultilinearMap.mkPiRing R ι z') :
          (a : (i : ι) → R) → M₂)
        fun (x : ι) ↦ 1 :
      M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
c : R
z : M₂
h :
  Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (c • z) : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((HSMul.hSMul (α := R) (β := MultilinearMap R (fun (x : ι) ↦ R) M₂) ((RingHom.id R : (a : R) → R) c : R)
            (MultilinearMap.mkPiRing R ι z) :
          (a : (i : ι) → R) → M₂)
        fun (x : ι) ↦ 1 :
      M₂)
⊢ MultilinearMap.mkPiRing R ι (c • z) =
    HSMul.hSMul (α := R) (β := MultilinearMap R (fun (x : ι) ↦ R) M₂) ((RingHom.id R : (a : R) → R) c : R)
      (MultilinearMap.mkPiRing R ι z)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
c : R
z : M₂
⊢ Eq.{v₂ + 1} (α := M₂) ((MultilinearMap.mkPiRing R ι (c • z) : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((HSMul.hSMul (α := R) (β := MultilinearMap R (fun (x : ι) ↦ R) M₂) ((RingHom.id R : (a : R) → R) c : R)
            (MultilinearMap.mkPiRing R ι z) :
          (a : (i : ι) → R) → M₂)
        fun (x : ι) ↦ 1 :
      M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Fintype ι
z : M₂
⊢ (fun (f : MultilinearMap R (fun (x : ι) ↦ R) M₂) ↦ ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂))
      ((fun (z : M₂) ↦ (MultilinearMap.mkPiRing R ι z : MultilinearMap R (fun (x : ι) ↦ R) M₂)) z) =
    z

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
let :
  ∀ (i : ι),
    Membership.mem (γ := Set M₂)
      (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
      (c • x_1)
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)

Tactic:
⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩

Premises used: Function.update, Set.Mem, setOf, Eq.rec, dite, And.intro, Exists.intro, Set.image, HSMul.hSMul, Eq
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
refine_1 : ∀ (j : ι) (hij : j = i), update (β := M₁) x i (c • x i) j ∈ p j
refine_2 : ∀ (j : ι) (hij : ¬j = i), update (β := M₁) x i (c • x i) j ∈ p j
refine_3 :
  (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (c • x i)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i})
    (c • x_1)

Tactic:
refine ⟨update x i (c • x i), fun j => if hij : j = i then ?_ else ?_, hf ▸ ?_⟩
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
refine_1 : c • x i ∈ p i
⊢ update (β := M₁) x i (c • x i) j ∈ p j

Tactic:
rw [hij, update_self]

Premises used: Function.update_self
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ c • x i ∈ p i

Tactic:
(p i).smul_mem _ (hx i)

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ c • x i ∈ p i

Tactic:
exact (p i).smul_mem _ (hx i)

Premises used: Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
refine_2 : x j ∈ p j
⊢ update (β := M₁) x i (c • x i) j ∈ p j

Tactic:
rw [update_of_ne hij]

Premises used: Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ x j ∈ p j

Tactic:
hx j
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : ¬j = i
⊢ x j ∈ p j

Tactic:
exact hx j
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M'
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x_1 : M₂
h :
  Membership.mem (γ := Set M₂)
    (Set.image (α := (i : ι) → M₁ i) (⇑f : (a : (i : ι) → M₁ i) → M₂) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i}) x_1
x : (i : ι) → M₁ i
hx : Membership.mem (γ := Set ((i : ι) → M₁ i)) {v : (i : ι) → M₁ i | ∀ (i : ι), v i ∈ p i} x
hf : (f : (a : (i : ι) → M₁ i) → M₂) x = x_1
i : ι
this : DecidableEq ι := Classical.decEq ι
refine_3 :
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (x i)) : M₂) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
refine_3₁ refine_3₂ :
  HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (c • x i)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)

Tactic:
rw [f.map_update_smul, update_eq_self]

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Ring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
⊢ (↑(f.map (M₁ := M₁) p) : Set M₂).Nonempty

Tactic:
⟨f 0, 0, fun i => (p i).zero_mem, rfl⟩

Premises used: Set.Nonempty, Submodule.zero_mem, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
intro : ∀ (val : Fintype ι), f = g
⊢ f = g

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
intro :
  ∀ (m : (i : ι) → M i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
⊢ f = g

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
m : (i : ι) → M i
intro :
  ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
    Eq.{u_4 + 1} (α := N)
      ((f : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
      ((g : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)

Tactic:
rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩

Premises used: LinearEquiv.symm, LinearEquiv.surjective, Module.Basis.repr, Function.Surjective.piMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R
intro :
  Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
    ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
        (fun (i : ι) ↦
            ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
          i (x i) :
      N)
⊢ Eq.{u_4 + 1} (α := N)
    ((f : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)
    ((g : (a : (i : ι) → M i) → N)
        (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
          (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
      N)

Tactic:
unfold Pi.map

Premises used: Pi.map
-- Module: Mathlib.LinearAlgebra.Multilinear.Basis
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
M : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis.{u_5, u_2, u_3} (ιM i) R (M i)
h :
  ∀ (v : (i : ι) → ιM i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦ (e i : (a : ιM i) → M i) (v i) : N)
val : Fintype ι
intro :
  ∀ (m : (i : ι) → M i),
    Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M i) → N) m : N) ((g : (a : (i : ι) → M i) → N) m : N)
intro₁ :
  ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
    Eq.{u_4 + 1} (α := N)
      ((f : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
      ((g : (a : (i : ι) → M i) → N)
          (Pi.map (α := fun (i : ι) ↦ Finsupp.{u_5, u_2} (ιM i) R) (β := M)
            (fun (i : ι) ↦ (⇑(e i).repr.symm : (a : ιM i →₀ R) → M i)) x) :
        N)
intro₂ :
  ∀ (x : (i : ι) → Finsupp.{u_5, u_2} (ιM i) R),
    Eq.{u_4 + 1} (α := N)
      ((f : (a : (i : ι) → M i) → N) fun (i : ι) ↦
          (fun (i : ι) ↦
              ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
            i (x i) :
        N)
      ((g : (a : (i : ι) → M i) → N) fun (i : ι) ↦
          (fun (i : ι) ↦
              ((⇑(e i).repr.symm : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i) : (a : Finsupp.{u_5, u_2} (ιM i) R) → M i))
            i (x i) :
        N)
⊢ f = g

Tactic:
classical
  ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]

Premises used: Finsupp.sum, Pi.map, Finsupp.linearCombination_apply, MultilinearMap.map_sum_finset, MultilinearMap.map_smul_univ, Module.Basis.repr_symm_apply, rfl