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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : IsScalarTower R S S
t : R
a b : S[M]
a✝ : M
⊢ ((t • a) • b).coeff a✝ = (t • a • b).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : IsScalarTower R S S
t : R
a b : S[M]
a✝ : M
⊢ ((t • a) • b).coeff a✝ = (t • a • b).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : SMulCommClass R S S
t : R
a b : S[M]
a✝ : M
⊢ (t • a • b).coeff a✝ = (a • t • b).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝³ : Semiring S
inst✝² : DistribSMul R S
inst✝¹ : Mul M
inst✝ : SMulCommClass R S S
t : R
a b : S[M]
a✝ : M
⊢ (t • a • b).coeff a✝ = (a • t • b).coeff a✝
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
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)

Tactic:
;

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)
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 β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
a : ↑t
⊢ v ((fun a ↦ f ⋯) a) ∈ t

Tactic:
;

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
a : ↑t
⊢ v ((fun a ↦ f ⋯) a) ∈ t
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ range (v ∘ Subtype.val) = t

Tactic:
;

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ range (v ∘ Subtype.val) = t
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
x✝ : ↑s
⊢ (Subtype.val ∘ f') x✝ = (v ∘ Subtype.val) x✝

Tactic:
;

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
x✝ : ↑s
⊢ (Subtype.val ∘ f') x✝ = (v ∘ Subtype.val) x✝
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
a✝ : N
⊢ (mapDomain f 0).coeff a✝ = (coeff 0) a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
a✝ : N
⊢ (mapDomain f 0).coeff a✝ = (coeff 0) a✝
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 y : R[M]
a✝ : N
⊢ (mapDomain f (x + y)).coeff a✝ = (mapDomain f x + mapDomain f y).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x y : R[M]
a✝ : N
⊢ (mapDomain f (x + y)).coeff a✝ = (mapDomain f x + mapDomain f y).coeff a✝
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a✝ : α × β
⊢ a✝ ∈ image₂ Prod.mk s t ↔ a✝ ∈ s ×ˢ t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset β
⊢ image₂ Prod.mk s t = s ×ˢ t

Tactic:
by ext; simp [Prod.ext_iff]

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
f : M → N
x : S[M]
v : M → S → R[M]
a✝ : N
⊢ (mapDomain f (x.coeff.sum v)).coeff a✝ = (x.coeff.sum fun a b ↦ mapDomain f (v a b)).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
N : Type u_7
inst✝¹ : Semiring R
inst✝ : Semiring S
f : M → N
x : S[M]
v : M → S → R[M]
a✝ : N
⊢ (mapDomain f (x.coeff.sum v)).coeff a✝ = (x.coeff.sum fun a b ↦ mapDomain f (v a b)).coeff a✝
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 β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image₂ (fun a b ↦ f b a) t s = image₂ g t s

Tactic:
by simp_rw [h_comm]

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
a : M
r : R
a✝ : N
⊢ (mapDomain f (single a r)).coeff a✝ = (single (f a) r).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
a : M
r : R
a✝ : N
⊢ (mapDomain f (single a r)).coeff a✝ = (single (f a) r).coeff a✝
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
a✝ : M
⊢ (map f 0).coeff a✝ = (coeff 0) a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
a✝ : M
⊢ (map f 0).coeff a✝ = (coeff 0) a✝
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
x y : R[M]
a✝ : M
⊢ (map f (x + y)).coeff a✝ = (map f x + map f y).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
x y : R[M]
a✝ : M
⊢ (map f (x + y)).coeff a✝ = (map f x + map f y).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
s : Finset ι
x : ι → R[M]
a✝ : M
⊢ (map f (∑ i ∈ s, x i)).coeff a✝ = (∑ i ∈ s, map f (x i)).coeff a✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
s : Finset ι
x : ι → R[M]
a✝ : M
⊢ (map f (∑ i ∈ s, x i)).coeff a✝ = (∑ i ∈ s, map f (x i)).coeff a✝
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
r : R
m a✝ : M
⊢ (map f (single m r)).coeff a✝ = (single m (f r)).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
r : R
m a✝ : M
⊢ (map f (single m r)).coeff a✝ = (single m (f r)).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝ : Semiring R
x : R[M]
a✝ : M
⊢ (map (AddMonoidHom.id R) x).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
inst✝ : Semiring R
x : R[M]
a✝ : M
⊢ (map (AddMonoidHom.id R) x).coeff a✝ = x.coeff a✝
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
f : S →+ T
g : R →+ S
x : R[M]
a✝ : M
⊢ (map f (map g x)).coeff a✝ = (map (f.comp g) x).coeff a✝

Tactic:
;

Goal state after:
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
f : S →+ T
g : R →+ S
x : R[M]
a✝ : M
⊢ (map f (map g x)).coeff a✝ = (map (f.comp g) x).coeff a✝
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
x✝ : R[M]
a✝ : M
⊢ (map f x✝).coeff a✝ = ((⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
x✝ : R[M]
a✝ : M
⊢ (map f x✝).coeff a✝ = ((⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv) x✝).coeff a✝
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
x✝ : R[M]
a✝ : M
⊢ (map f x✝).coeff a✝ = ((⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
x✝ : R[M]
a✝ : M
⊢ (map f x✝).coeff a✝ = ((⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv) x✝).coeff a✝
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
a✝ : M
⊢ (comapDomain f hf 0).coeff a✝ = (coeff 0) a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
a✝ : M
⊢ (comapDomain f hf 0).coeff a✝ = (coeff 0) a✝
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]
a✝ : M
⊢ (comapDomain f hf (x + y)).coeff a✝ = (comapDomain f hf x + comapDomain f hf y).coeff a✝

Tactic:
;

Goal state after:
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]
a✝ : M
⊢ (comapDomain f hf (x + y)).coeff a✝ = (comapDomain f hf x + comapDomain f hf y).coeff a✝
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
a✝ : M
⊢ (comapDomain f hf (single n r)).coeff a✝ = (coeff 0) a✝

Tactic:
;

Goal state after:
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
a✝ : M
⊢ (comapDomain f hf (single n r)).coeff a✝ = (coeff 0) a✝
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
a✝ : M
⊢ (comapDomain f hf (single (f m) r)).coeff a✝ = (single m r).coeff a✝

Tactic:
;

Goal state after:
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
a✝ : M
⊢ (comapDomain f hf (single (f m) r)).coeff a✝ = (single m r).coeff a✝
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)).coeff = x.coeff

Tactic:
;

Goal state after:
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)).coeff = x.coeff
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
x✝ : R[M]
a✝ : M
⊢ ((mapDomainNonUnitalRingHom R (MulHom.id M)) x✝).coeff a✝ = ((NonUnitalRingHom.id R[M]) x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
x✝ : R[M]
a✝ : M
⊢ ((mapDomainNonUnitalRingHom R (MulHom.id M)) x✝).coeff a✝ = ((NonUnitalRingHom.id R[M]) x✝).coeff a✝
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
x✝ : R[M]
a✝ : O
⊢ ((mapDomainNonUnitalRingHom R (f.comp g)) x✝).coeff a✝ =
    (((mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)) x✝).coeff a✝

Tactic:
;

Goal state after:
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
x✝ : R[M]
a✝ : O
⊢ ((mapDomainNonUnitalRingHom R (f.comp g)) x✝).coeff a✝ =
    (((mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)) x✝).coeff a✝
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]
a✝ : M
⊢ ((fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x)).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
ι : 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]
a✝ : M
⊢ ((fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x)).coeff a✝ = x.coeff a✝
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:
have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]

Goal state after:
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))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
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]
a✝ : N
⊢ ((fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x)).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
ι : 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]
a✝ : N
⊢ ((fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x)).coeff a✝ = x.coeff a✝
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]
a✝ : N
⊢ (mapDomain (⇑e) (x + y)).coeff a✝ = (mapDomain (⇑e) x + mapDomain (⇑e) y).coeff a✝

Tactic:
;

Goal state after:
ι : 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]
a✝ : N
⊢ (mapDomain (⇑e) (x + y)).coeff a✝ = (mapDomain (⇑e) x + mapDomain (⇑e) y).coeff a✝
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]
a✝ : N
⊢ ((mapDomainAddEquiv R e) x).coeff a✝ = (equivMapDomain e x.coeff) a✝

Tactic:
;

Goal state after:
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]
a✝ : N
⊢ ((mapDomainAddEquiv R e) x).coeff a✝ = (equivMapDomain e x.coeff) a✝
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
x✝ : R[M]
a✝ : O
⊢ ((mapDomainAddEquiv R (e₁.trans e₂)) x✝).coeff a✝ =
    (((mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)) x✝).coeff a✝

Tactic:
;

Goal state after:
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
x✝ : R[M]
a✝ : O
⊢ ((mapDomainAddEquiv R (e₁.trans e₂)) x✝).coeff a✝ =
    (((mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)) x✝).coeff a✝
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]
a✝ : M
⊢ (map (↑e.symm) (map (↑e) x)).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
ι : 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]
a✝ : M
⊢ (map (↑e.symm) (map (↑e) x)).coeff a✝ = x.coeff a✝
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]
a✝ : M
⊢ (map (↑e) (map (↑e.symm) x)).coeff a✝ = x.coeff a✝

Tactic:
;

Goal state after:
ι : 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]
a✝ : M
⊢ (map (↑e) (map (↑e.symm) x)).coeff a✝ = x.coeff a✝
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
x✝ : R[M]
a✝ : M
⊢ ((mapAddEquiv M (e₁.trans e₂)) x✝).coeff a✝ = (((mapAddEquiv M e₁).trans (mapAddEquiv M e₂)) x✝).coeff a✝

Tactic:
;

Goal state after:
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
x✝ : R[M]
a✝ : M
⊢ ((mapAddEquiv M (e₁.trans e₂)) x✝).coeff a✝ = (((mapAddEquiv M e₁).trans (mapAddEquiv M e₂)) x✝).coeff a✝
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
⊢ (map (↑f) 1).coeff a✝ = (coeff 1) a✝

Tactic:
;

Goal state after:
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
⊢ (map (↑f) 1).coeff a✝ = (coeff 1) a✝
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₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

Tactic:
;

Goal state after:
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₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))