mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
⊢ mapRingEquiv M (e₁.trans e₂) = (mapRingEquiv M e₁).trans (mapRingEquiv M e₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ commRingEquiv (single m (single n r)) = single n (single m r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x : R[M]
⊢ map f (-x) = -map f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x y : R[M]
⊢ map f (x - y) = map f x - map f y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff))
      ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff)) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = s.sup' ⋯ fun x ↦ t.sup' ⋯ fun x_1 ↦ g (f x x_1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : MonoidAlgebra R (Multiplicative M)
⊢ (fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff)) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m₁ m₂ : M
⊢ single m₁ r₁ = single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r : R
m₁ m₂ : M
hr : r ≠ 0
⊢ single m₁ r = single m₂ r ↔ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m : M
⊢ single m r₁ = single m r₂ ↔ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m₁ m₂ m₁' m₂' : M
hr₁ : r₁ ≠ 0
hr₂ : r₂ ≠ 0
⊢ single m₁ r₁ + single m₂ r₂ = single m₁' r₁ + single m₂' r₂ ↔
    m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x y : R[M]
⊢ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x * y).coeff) =
    MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) *
      MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ erase m 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x y : R[M]
⊢ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x + y).coeff) =
    MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) +
      MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
⊢ {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
r : R
⊢ erase m (single m r) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Add M
m : M
r : R
⊢ (toMultiplicative R M) (single m r) = MonoidAlgebra.single (Multiplicative.ofAdd m) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
A : Type u_8
inst✝ : SMulZeroClass A R
⊢ SMul.smul = NSMul.nsmul

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
A : Type u_8
inst✝¹ : SMulZeroClass A R
inst✝ : Monoid A
a : Aˣ
x : R[M]
⊢ a • x = ↑a • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff))
      ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff)) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
A : Type u_8
inst✝ : SMulZeroClass A R
a : A
m : M
r : R
⊢ a • single m r = single m (a • r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ single m 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : AddMonoidAlgebra R (Additive M)
⊢ (fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff)) x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
a : δ
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
r₁ r₂ : R
⊢ single m (r₁ + r₂) = single m r₁ + single m r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
⊢ single m (x.coeff m) + erase m x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
⊢ erase m x + single m (x.coeff m) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
⊢ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x * y).coeff) =
    AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) *
      AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ ↑({x ∈ t | x ∈ s}) ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
⊢ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x + y).coeff) =
    AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) +
      AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
m : M
r : R
⊢ (toAdditive R M) (single m r) = AddMonoidAlgebra.single (Additive.ofMul m) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
N : Type u_8
inst✝ : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ ∀ (m : M) (r : R), f (single m r) = g (single m r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid N
m : M
r : R
h : M → R → N
h_zero : h m 0 = 0
⊢ (single m r).coeff.sum h = h m r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ s ∩ ↑({x ∈ t | x ∉ s}) = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = t.sup fun y ↦ s.sup fun x ↦ g (f x y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
f : R[M]
⊢ f.coeff.sum single = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r : R
m : M
⊢ single m r = 0 ↔ r = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
motive : R[M] → Prop
x : R[M]
zero : motive 0
single_add : ∀ (m : M) (r : R) (x : R[M]), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)
⊢ motive (ofCoeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : One M
⊢ (coeff 1) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
⊢ x * y = x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a : R[M]), 0 * a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a : R[M]), a * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Mul M
inst✝ : DecidableEq M
x y : R[M]
m : M
⊢ (x * y).coeff m = x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = m then r₁ * r₂ else 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
⊢ s ⊆ ↑(span K ↑({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeInf δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) =
    ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
h : ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card
⊢ s ∪ ↑({x ∈ t | x ∉ s}) ⊆ s ∪ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ (piFinset fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t
u : Finset V
h : ↑u ⊆ s ∪ ↑({x ∈ t | x ∉ s}) ∧ s ⊆ ↑u ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card
⊢ u.card = t.card

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝³ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(image2 f s t)
⊢ ↑(image2 f s t).toFinset = ↑(image₂ f s.toFinset t.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2 =
    ∑ p ∈ s with p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support, x.coeff p.1 * y.coeff p.2

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K ↑ht.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
hf : (image2 f s t).Finite
⊢ ↑hf.toFinset = ↑(image₂ f hs.toFinset ht.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ ↑this.toFinset ⊆ ↑u

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ ht.toFinset.card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (x y : R[M]ᵐᵒᵖ),
    (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun (x * y) =
      (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun x *
        (opAddEquiv.symm.trans ((mapDomainAddEquiv R opEquiv).trans (mapAddEquiv Mᵐᵒᵖ opAddEquiv))).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
⊢ MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ MonoidAlgebra.opRingEquiv.symm (single x r) = op (single (unop x) (unop r))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
⊢ (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
m₁ m₂ : M
r₁ r₂ : R
⊢ single m₁ r₁ * single m₂ r₂ = single (m₁ * m₂) (r₁ * r₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r₁ r₂ : R
m₁ m₂ : M
inst✝ : Mul M
hm : Commute m₁ m₂
hr : Commute r₁ r₂
⊢ Commute (single m₁ r₁) (single m₂ r₂)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
⊢ AddMonoidHom.mulLeft (single m r) = AddMonoidHom.mulRight (single m r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
⊢ Commute (single m r) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r).coeff m₁ = x.coeff.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0) = x.coeff.sum fun m' r' ↦ if m' = m₂ then r' * r else 0

Tactic:
by

Goal state after: