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

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
⊢ (RingHom.pi fun i ↦ algebraMap R (A i)) a * f = f * (RingHom.pi fun i ↦ algebraMap R (A i)) a

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝ = (f * (RingHom.pi fun i ↦ algebraMap R (A i)) a) x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
⊢ a • f = (RingHom.pi fun i ↦ algebraMap R (A i)) a * f

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ (a • f) x✝ = ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A i)
inst✝² : (i : ι) → Algebra R (A i)
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
g : (i : ι) → B →ₐ[R] A i
r : R
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) = (algebraMap R ((i : ι) → A i)) r

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A i)
inst✝² : (i : ι) → Algebra R (A i)
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
g : (i : ι) → B →ₐ[R] A i
r : R
x✝ : ι
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) x✝ = (algebraMap R ((i : ι) → A i)) r x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
ι : Type u_4
c : R
⊢ ⇑f ∘ (algebraMap R (ι → A)) c = (algebraMap R (ι → B)) c

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
ι : Type u_4
c : R
x✝ : ι
⊢ (⇑f ∘ (algebraMap R (ι → A)) c) x✝ = (algebraMap R (ι → B)) c x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝ : R
⊢ (RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝) = (algebraMap R ((α → S) × (β → S))) x✝

Tactic:
ext

Goal state after:
case fst
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : α
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).1 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).1 x✝

case snd
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : β
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).2 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).2 x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
t : R
v : ι → R
⊢ ⇑(algebraMap R A) ∘ (t • v) = (RingHom.id R) t • ⇑(algebraMap R A) ∘ v

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
t : R
v : ι → R
x✝ : ι
⊢ (⇑(algebraMap R A) ∘ (t • v)) x✝ = ((RingHom.id R) t • ⇑(algebraMap R A) ∘ v) x✝
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
⊢ toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)

Tactic:
ext

Goal state after:
X : Type u_1
x✝ a✝ : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x✝)) 1) a✝ =
    (((AddMonoidHom.id (X →₀ ℤ)).comp (singleAddHom x✝)) 1) a✝
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
⊢ toFreeAbelianGroup.comp toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)

Tactic:
ext

Goal state after:
X : Type u_1
x✝ : X
⊢ (toFreeAbelianGroup.comp toFinsupp) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } = 0

Tactic:
ext

Goal state after:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝ : AddChar A M
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } x✝ = 0 x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝¹ x✝ : A
⊢ { toFun := fun ψ ↦ ψ (x✝¹ + x✝), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } =
    { toFun := fun ψ ↦ ψ x✝¹, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } +
      { toFun := fun ψ ↦ ψ x✝, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

Tactic:
ext

Goal state after:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝² x✝¹ : A
x✝ : AddChar A M
⊢ { toFun := fun ψ ↦ ψ (x✝² + x✝¹), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } x✝ =
    ({ toFun := fun ψ ↦ ψ x✝², map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } +
        { toFun := fun ψ ↦ ψ x✝¹, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ })
      x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ - χ) a = ψ a / χ a

Tactic:
rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ⁻¹ = ψ.mulShift (-1)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s : R
⊢ ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = (ψ.mulShift (r + s)) x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s : R
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ ((ψ.mulShift r).mulShift s) x✝ = (ψ.mulShift (r * s)) x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 0 = 1

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 0) x✝ = 1 x✝
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 0 = 1

Tactic:
ext; rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 1 = ψ

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 1) x✝ = ψ x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∈ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

pp: case neg
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

Tactic:
· simp [insert_eq_of_mem has, has]

Goal state after:
case neg
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)
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
s : Set ι
a : ι
f : ι → V
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

Tactic:
by
  by_cases has : a ∈ s
  · simp [insert_eq_of_mem has, has]
  simp [linearIndepOn_insert has, has]

Goal state after:
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
inst✝² : Monoid S
inst✝¹ : Semiring R
inst✝ : DistribMulAction S R
f : M → N
s : S
x : R[M]
⊢ mapDomain f (s • x) = s • mapDomain f x

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝² : Monoid S
inst✝¹ : Semiring R
inst✝ : DistribMulAction S R
f : M → N
s : S
x : R[M]
a✝ : N
⊢ (mapDomain f (s • x)).coeff a✝ = (s • mapDomain f x).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
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
f : M → N
g : N → O
⊢ mapDomainLinearMap R S (g ∘ f) = mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
f : M → N
g : N → O
x✝ : S[M]
a✝ : O
⊢ ((mapDomainLinearMap R S (g ∘ f)) x✝).coeff a✝ = ((mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f) x✝).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
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
e₁ : M ≃ N
e₂ : N ≃ O
⊢ mapDomainLinearEquiv R S (e₁.trans e₂) = mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
e₁ : M ≃ N
e₂ : N ≃ O
x✝ : S[M]
a✝ : O
⊢ ((mapDomainLinearEquiv R S (e₁.trans e₂)) x✝).coeff a✝ =
    ((mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂) x✝).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
⊢ (liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m✝ : M
x✝ : S
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c)).comp (singleAddHom m✝)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom m✝)) x✝
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]
⊢ (t • a) • b = t • a • b

Tactic:
ext

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]
⊢ t • a • b = a • t • b

Tactic:
ext

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.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : AddZeroClass M
f : S →+* R
g : Multiplicative M →* R
c : S
φ : S[M]
⊢ (liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : AddZeroClass M
f : S →+* R
g : Multiplicative M →* R
c : S
φ : S[M]
m✝ : M
x✝ : S
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c)).comp (singleAddHom m✝)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom m✝)) x✝
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a) ↔ ∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

Tactic:
constructor

Goal state after:
case h.mp
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a) → ∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f

case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) → ∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_3
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
exact subset_sUnion_of_mem

Goal state after:
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, ⋯⟩
⊢ Subtype.val ∘ f' = v ∘ Subtype.val

Tactic:
ext

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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective fun a ↦ f a b
⊢ #(image₂ f s {b}) = #s

Tactic:
image₂_singleton_right,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective fun a ↦ f a b
⊢ #(image (fun a ↦ f a b) s) = #s
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
b : β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
hf : Injective fun a ↦ f a b
⊢ image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}

Tactic:
image₂_singleton_right,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
b : β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
hf : Injective fun a ↦ f a b
⊢ image (fun a ↦ f a b) (s₁ ∩ s₂) = image (fun a ↦ f a b) s₁ ∩ image (fun a ↦ f a b) s₂
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
⊢ mapDomain f 0 = 0

Tactic:
ext

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]
⊢ mapDomain f (x + y) = mapDomain f x + mapDomain f y

Tactic:
ext

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 β
⊢ image₂ Prod.mk s t = s ×ˢ t

Tactic:
ext

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.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]
⊢ mapDomain f (x.coeff.sum v) = x.coeff.sum fun a b ↦ mapDomain f (v a b)

Tactic:
ext

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.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
⊢ mapDomain f (single a r) = single (f a) r

Tactic:
ext

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
⊢ map f 0 = 0

Tactic:
ext

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]
⊢ map f (x + y) = map f x + map f y

Tactic:
ext

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]
⊢ map f (∑ i ∈ s, x i) = ∑ i ∈ s, map f (x i)

Tactic:
ext

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 : M
⊢ map f (single m r) = single m (f r)

Tactic:
ext

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]
⊢ map (AddMonoidHom.id R) x = x

Tactic:
ext

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]
⊢ map f (map g x) = map (f.comp g) x

Tactic:
ext

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
⊢ map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv

Tactic:
ext

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
⊢ map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv

Tactic:
ext

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.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:
image₂_singleton_right,

Goal state after:
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image (fun a ↦ f a b) s = s
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:
ext

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]
⊢ comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

Tactic:
ext

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
⊢ comapDomain f hf (single n r) = 0

Tactic:
ext

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✝