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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
⊢ ⇑coeffEquiv ⁻¹' Set.range (mapRange ⇑f ⋯ ∘ ⇑coeffEquiv) = {x | ∀ (i : M), x.coeff i ∈ Set.range ⇑f}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g' t) s)

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✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
⊢ map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ ↑(insert b₁ u) ⊆ s ∪ ↑(insert b₁ t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' t (image g' s))

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✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
⊢ Injective (map f)

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✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
⊢ map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv

Tactic:
by

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

Goal state before:
pp: α : Type u_1
γ : Type u_5
inst✝ : DecidableEq γ
f : α → γ → γ
a : α
h : ∀ (b : γ), f a b = b
t : Finset γ
⊢ ↑(image₂ f {a} t) = ↑t

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✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
⊢ Surjective (map f)

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
f : M → N
hf : Injective f
x : R[N]
⊢ (comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯

Tactic:
by

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

Goal state before:
pp: β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image₂ f s {b} = s

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
f : M → N
hf : Injective f
⊢ comapDomain f hf 0 = 0

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
f : M → N
hf : Injective f
x y : R[N]
⊢ comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

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
f : M → N
r : R
n : N
hn : n ∉ Set.range f
hf : Injective f
⊢ comapDomain f hf (single n r) = 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✝¹ : Semiring S
inst✝ : Semiring T
f✝ : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ comapDomain f hf 0 = 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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ ↑u ⊆ ↑(insert b₁ u)

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✝¹ : Semiring S
inst✝ : Semiring T
f✝ : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ ∀ (x y : R[N]), comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

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
f : M → N
hf : Injective f
m : M
r : R
⊢ comapDomain f hf (single (f m) r) = single m r

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
f : M → N
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ mapDomain f (comapDomain f hf x) = x

Tactic:
by

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

Goal state before:
pp: F : Type u_2
R : Type u_3
M : Type u_6
N : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
x y : R[M]
⊢ mapDomain (⇑f) (x * y) = mapDomain (⇑f) x * mapDomain (⇑f) y

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (insert b₁ u).card = (s' ∪ insert b₁ t).card

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
⊢ mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id R[M]

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))

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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
f : N →ₙ* O
g : M →ₙ* N
⊢ mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)

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✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[M]
⊢ (fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x) = 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✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[N]
⊢ (fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x) = 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✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x y : R[M]
⊢ mapDomain (⇑e) (x + y) = mapDomain (⇑e) x + mapDomain (⇑e) y

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✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
x : R[M]
⊢ ((mapDomainAddEquiv R e) x).coeff = equivMapDomain e x.coeff

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✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
r : R
m : M
⊢ (mapDomainAddEquiv R e) (single m r) = single (e m) r

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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
⊢ mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))

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✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : R[M]
⊢ map (↑e.symm) (map (↑e) x) = 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✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : S[M]
⊢ map (↑e) (map (↑e.symm) x) = x

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
e : R ≃+ S
x : R[M]
m : M
⊢ ((mapAddEquiv M e) x).coeff m = e (x.coeff m)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
e : R ≃+ S
r : R
m : M
⊢ (mapAddEquiv M e) (single m r) = single m (e r)

Tactic:
by

Goal state after:
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✝ : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
⊢ mapAddEquiv M (e₁.trans e₂) = (mapAddEquiv M e₁).trans (mapAddEquiv M e₂)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
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: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
⊢ mapDomainRingHom R (MonoidHom.id M) = RingHom.id R[M]

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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
⊢ mapDomainRingHom R (f.comp g) = (mapDomainRingHom R f).comp (mapDomainRingHom R g)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
⊢ map (↑f) 1 = 1

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
x : R[M]
m : M
⊢ ((mapRingHom M f) x).coeff m = f (x.coeff m)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
a : M
b : R
⊢ (mapRingHom M f) (single a b) = single a (f b)

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✝ : Monoid M
⊢ mapRingHom M (RingHom.id R) = RingHom.id R[M]

Tactic:
by

Goal state after:
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
f : S →+* T
g : R →+* S
⊢ mapRingHom M (f.comp g) = (mapRingHom M f).comp (mapRingHom M g)

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
N : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Monoid M
inst✝ : Monoid N
f : R →+* S
g : M →* N
⊢ (mapRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRingHom M f)

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 : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f s 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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

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✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm) = RingHom.id R[N]

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 : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ f s 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✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
⊢ ↑(insert b₂ 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✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ (mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e) = RingHom.id R[M]

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
e : M ≃* N
r : R
m : M
⊢ (mapDomainRingEquiv R e) (single m r) = single (e m) r

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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
⊢ mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : u.card = (insert b₂ s' ∪ t).card
⊢ ↑t ⊆ ↑(insert b₁ t)

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 : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ image2 f s t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

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 s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∩ s') (t ∪ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

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✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ (mapRingHom M ↑e).comp (mapRingHom M ↑e.symm) = RingHom.id S[M]

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 s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∪ s') (t ∩ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∩ t) (s ∪ t)) ⊆ ↑(image₂ f s t)

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✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ (mapRingHom M ↑e.symm).comp (mapRingHom M ↑e) = RingHom.id R[M]

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✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : u.card = (insert b₂ s' ∪ t).card
⊢ u.card = (s' ∪ insert b₁ t).card

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∪ t) (s ∩ t)) ⊆ ↑(image₂ f s t)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
e : R ≃+* S
x : R[M]
m : M
⊢ ((mapRingEquiv M e) x).coeff m = e (x.coeff m)

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✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
e : R ≃+* S
r : R
m : M
⊢ (mapRingEquiv M e) (single m r) = single m (e r)

Tactic:
by

Goal state after: