awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
⊢ finrank R ↥(⋀[R]^(n + 1) (M × N)) = 1

Tactic:
simp [exteriorPower.finrank_eq, hp]

Premises used: exteriorPower.finrank_eq
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
e : R ≃ₗ[R] ↥(⋀[R]^(n + 1) (M × N)) := Nonempty.some ⋯
bN : Basis (Fin n) R N := finBasis R N
f : R →ₗ[R] M := exteriorPower.cofactorToLeft bN ∘ₗ (↑e : R →ₗ[R] ↥(⋀[R]^(n + 1) (M × N)))
x : M
⊢ (f : (a : R) → M)
      ((e.symm : (a : ↥(⋀[R]^(n + 1) (M × N))) → R)
          (((exteriorPower.ιMulti R (n + 1) (M := M × N) : (M × N) [⋀^Fin (n + 1)]→ₗ[R] ↥(⋀[R]^(n + 1) (M × N))) :
                (a : Fin (n + 1) → M × N) → ↥(⋀[R]^(n + 1) (M × N)))
              (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M × N) (x, 0) fun (i : Fin n) ↦ (0, (bN : (a : Fin n) → N) i)) :
            ↥(⋀[R]^(n + 1) (M × N))) :
        R) =
    x

Tactic:
simp [f, exteriorPower.cofactorToLeft_ιMulti_cons]

Premises used: _private.0.exteriorPower.cofactorToLeft_ιMulti_cons
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
hp : finrank R (M × N) = n + 1
e : R ≃ₗ[R] ↥(⋀[R]^(n + 1) (M × N)) := Nonempty.some ⋯
bN : Basis (Fin n) R N := finBasis R N
f : R →ₗ[R] M := exteriorPower.cofactorToLeft bN ∘ₗ (↑e : R →ₗ[R] ↥(⋀[R]^(n + 1) (M × N)))
⊢ Free R M

Tactic:
exact Module.Free.of_equiv <| LinearEquiv.ofBijective f <| Invertible.bijective_of_surjective <|
    fun x ↦ ⟨e.symm (exteriorPower.ιMulti R (n + 1) (Fin.cons (x, 0) fun i ↦ (0, bN i))), by
      simp [f, exteriorPower.cofactorToLeft_ιMulti_cons]⟩

Premises used: Module.Invertible.bijective_of_surjective, Module.Free.of_equiv, LinearEquiv.ofBijective
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ StrictMono.{v, v} (α := Submodule R M) toAddSubmonoid

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
⊢ p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Monotone.{v, v} (α := Submodule R M) toAddSubmonoid

Tactic:
toAddSubmonoid_strictMono.monotone

Premises used: StrictMono.monotone, Submodule.toAddSubmonoid_strictMono
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ StrictMono.{v, v} (α := Submodule R M) toSubMulAction

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Monotone.{v, v} (α := Submodule R M) toSubMulAction

Tactic:
toSubMulAction_strictMono.monotone

Premises used: StrictMono.monotone, Submodule.toSubMulAction_strictMono
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
t : Finset ι
f : ι → M
⊢ (∀ c ∈ t, f c ∈ p) → ∑ i ∈ t, f i ∈ p

Tactic:
sum_mem

Premises used: sum_mem
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
t : Finset ι
f : ι → M
r : ι → R
hyp : ∀ c ∈ t, f c ∈ p
⊢ ∑ i ∈ t, r i • f i ∈ p

Tactic:
sum_mem fun i hi => smul_mem _ _ (hyp i hi)

Premises used: sum_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : IsScalarTower S R M
inst_5 : SMul.{u', u} Sᵐᵒᵖ R
inst_6 : SMul.{u', v} Sᵐᵒᵖ M
inst_7 : IsScalarTower.{u', u, v} Sᵐᵒᵖ R M
inst_8 : IsCentralScalar S M
⊢ IsCentralScalar.{u', v} S ↥p

Tactic:
p.toSubMulAction.isCentralScalar

Premises used: Set.Mem, Submodule.toSubMulAction, SubMulAction.isCentralScalar
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Module.IsTorsionFree R M
⊢ ∀ (r : R) (m : ↥p), (↑(r • m) : M) = r • (↑m : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
α : Type u_1
β : Type u_2
inst_2 : VAdd M β
inst_3 : VAdd α β
inst_4 : VAddCommClass M α β
⊢ VAddCommClass.{v, u_1, u_2} (↥p) α β

Tactic:
⟨fun a => vadd_comm (a : M)⟩

Premises used: VAddCommClass.vadd_comm, VAddCommClass.mk, Subtype.val
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
α : Type u_1
β : Type u_2
inst_2 : VAdd M α
inst_3 : FaithfulVAdd M α
⊢ FaithfulVAdd.{v, u_1} (↥p) α

Tactic:
⟨fun h => Subtype.ext <| eq_of_vadd_eq_vadd h⟩

Premises used: FaithfulVAdd.mk, FaithfulVAdd.eq_of_vadd_eq_vadd, Subtype.ext
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
α : Type u_1
inst_2 : VAdd M α
g : ↥p
m : α
⊢ g +ᵥ m = (↑g : M) +ᵥ m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
⊢ StrictMono.{v, v} (α := Submodule R M) toAddSubgroup

Tactic:
fun _ _ => id

Premises used: StrictMono, id
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
⊢ p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
⊢ Monotone.{v, v} (α := Submodule R M) toAddSubgroup

Tactic:
toAddSubgroup_strictMono.monotone

Premises used: StrictMono.monotone, Submodule.toAddSubgroup_strictMono
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
⊢ p.toAddSubgroup.toAddSubmonoid = p.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
⊢ -(↑p : Set M) = (↑p : Set M)

Tactic:
Set.ext fun _ => p.neg_mem_iff

Premises used: Set.ext, Submodule.neg_mem_iff
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
x : M
N : Submodule R M
ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False

Tactic:
simpa using ortho (-1) x hx

Premises used: OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
x : M
N : Submodule R M
ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ x ≠ 0

Tactic:
mt (fun h => show x ∈ N from h.symm ▸ N.zero_mem) (notMem_of_ortho ortho)

Premises used: mt, Eq.rec, Submodule.zero_mem, Submodule.notMem_of_ortho, Eq.symm
-- Module: Mathlib.Algebra.Module.Submodule.Basic
Goal:
S : Type u'
R : Type u
M : Type v
inst : DivisionSemiring S
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
p : Submodule R M
s : S
x : M
s0 : s ≠ 0
⊢ s • x ∈ p ↔ x ∈ p

Tactic:
p.toSubMulAction.smul_mem_iff s0

Premises used: Set.Mem, Submodule.toSubMulAction, SubMulAction.smul_mem_iff
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
p : Submodule R M
q : Submodule R N
hm : m ∈ p
hn : n ∈ q
⊢ Eq.{u_4 + 1} (α := P)
    ((((f : (a : M) → N →ₗ[R] P) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) m hm) : M) : N →ₗ[R] P) : (a : N) → P) n : P)
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
r : Submodule R P
⊢ map₂ f p q ≤ r ↔
    ∀ m ∈ p, ∀ n ∈ q, Membership.mem (α := P) r ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
⟨fun H _m hm _n hn => H <| apply_mem_map₂ _ hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

Premises used: Iff.mpr, _private.0.Submodule.map₂_le.match_1, Submodule.apply_mem_map₂, LE.le, Iff.intro, iSup_le, Submodule.map, Submodule.map_le_iff_le_comap, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  map₂ f (span R s) (span R t) ≤
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
a₁ :
  span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t) ≤
    map₂ f (span R s) (span R t)
⊢ map₂ f (span R s) (span R t) =
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  ∀ (m : M),
    Membership.mem (γ := Submodule R M) (span R s) m →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
⊢ map₂ f (span R s) (span R t) ≤
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)

Tactic:
rw [map₂_le]

Premises used: Submodule.map₂_le
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
a₁ :
  ∀ (x : N) (h : x ∈ t),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
      ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P)
a₂ :
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) 0 : P)
a₃ :
  ∀ (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P) →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) y : P) →
        Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (x + y) : P)
a₄ :
  ∀ (a_1 : R) (x : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P) →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (a_1 • x) : P)
⊢ ∀ (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
apply @span_induction R N _ _ _ t

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
b : N
hb : b ∈ t
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) b : P)

Tactic:
subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩

Premises used: And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
b : N
hb : b ∈ t
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) b : P)

Tactic:
exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  ∀ (a : M) (ha : a ∈ s),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
      ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) 0 : P)
a₁ :
  ∀ (a : M) (ha : a ∈ s) (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P) →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) y : P) →
        Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (x + y) : P)
a₂ :
  ∀ (a : M) (ha : a ∈ s) (a_1 : R) (x : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P) →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (a_1 • x) : P)
⊢ ∀ (x : M) (h : x ∈ s) (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) 0 : P)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
x y : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
h :
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P)
h_1 :
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) y : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (x + y) : P)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
a_1 : R
x : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
h :
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) (a_1 • x) : P)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
n : N
h : Membership.mem (γ := Submodule R N) (span R t) n
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul