mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

Goal state after:
α : 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✝
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
x✝ : ι
⊢ (⇑(algebraMap R A) ∘ (t • v)) x✝ = ((RingHom.id R) t • ⇑(algebraMap R A) ∘ v) x✝

Tactic:
;

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.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

pp: case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
;

Goal state after:
case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : d • 1 = 0 ∧ -b • 1 = 0
⊢ b = 0 ∧ d = 0

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : d • 1 = 0 ∧ -b • 1 = 0
⊢ b = 0 ∧ d = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
i : Fin (Nat.succ 0).succ
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] i =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] i

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
i : Fin (Nat.succ 0).succ
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] i =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] i
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Subsingleton S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

pp: case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Nontrivial S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
;

Goal state after:
case inl
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Subsingleton S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
c : S
hS : Nontrivial S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
b : S
hS : Subsingleton S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

pp: case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
b : S
hS : Nontrivial S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Tactic:
;

Goal state after:
case inl
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
b : S
hS : Subsingleton S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

case inr
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
b : S
hS : Nontrivial S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s • x - t • x + (t • x + t • y) = s • x + t • y

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s • x - t • x + (t • x + t • y) = s • x + t • y
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a.support = ∅ ↔ a = 0

Tactic:
;

Goal state after:
X : Type u_1
a : FreeAbelianGroup X
⊢ a.support = ∅ ↔ a = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
x : M
hx : f x = 0
⊢ x ∈ ⊤

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
x : M
hx : f x = 0
⊢ x ∈ ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
hsp : span R (⇑f '' Set.range v) = ⊤
⊢ Surjective ⇑f

Tactic:
← Submodule.map_span,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
hsp : map f (span R (Set.range v)) = ⊤
⊢ Surjective ⇑f
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ✝ ψ : AddChar A M
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h : { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun = ψ.toFun
⊢ { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ } = ψ

Tactic:
;

Goal state after:
case mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ✝ ψ : AddChar A M
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h : { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun = ψ.toFun
⊢ { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ } = ψ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case mk.mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
toFun✝¹ : A → M
map_zero_eq_one'✝¹ : toFun✝¹ 0 = 1
map_add_eq_mul'✝¹ : ∀ (a b : A), toFun✝¹ (a + b) = toFun✝¹ a * toFun✝¹ b
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h :
  { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ }.toFun =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ } =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }

Tactic:
;

Goal state after:
case mk.mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
toFun✝¹ : A → M
map_zero_eq_one'✝¹ : toFun✝¹ 0 = 1
map_add_eq_mul'✝¹ : ∀ (a b : A), toFun✝¹ (a + b) = toFun✝¹ a * toFun✝¹ b
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h :
  { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ }.toFun =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ } =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : (fun f ↦ f.compAddChar ψ) f = (fun f ↦ f.compAddChar ψ) g
⊢ f = g

Tactic:
;

Goal state after:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : (fun f ↦ f.compAddChar ψ) f = (fun f ↦ f.compAddChar ψ) g
⊢ f = g
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : ⇑((fun f ↦ f.compAddChar ψ) f) = ⇑((fun f ↦ f.compAddChar ψ) g)
⊢ ⇑f = ⇑g

Tactic:
;

Goal state after:
A : Type u_1
M : Type u_3
N : Type u_4
inst✝² : AddMonoid A
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
hψ : Surjective ⇑ψ
f g : M →* N
h : ⇑((fun f ↦ f.compAddChar ψ) f) = ⇑((fun f ↦ f.compAddChar ψ) g)
⊢ ⇑f = ⇑g
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ f.compAddChar ψ) ψ = (fun ψ ↦ f.compAddChar ψ) χ
⊢ ψ = χ

Tactic:
;

Goal state after:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ f.compAddChar ψ) ψ = (fun ψ ↦ f.compAddChar ψ) χ
⊢ ψ = χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ ↦ f.compAddChar ψ) ψ) = ⇑((fun ψ ↦ f.compAddChar ψ) χ)
⊢ ⇑ψ = ⇑χ

Tactic:
;

Goal state after:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ ↦ f.compAddChar ψ) ψ) = ⇑((fun ψ ↦ f.compAddChar ψ) χ)
⊢ ⇑ψ = ⇑χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ ψ.compAddMonoidHom f) ψ = (fun ψ ↦ ψ.compAddMonoidHom f) χ
⊢ ψ = χ

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ ψ.compAddMonoidHom f) ψ = (fun ψ ↦ ψ.compAddMonoidHom f) χ
⊢ ψ = χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ ↦ ψ.compAddMonoidHom f) ψ) = ⇑((fun ψ ↦ ψ.compAddMonoidHom f) χ)
⊢ ⇑ψ = ⇑χ

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ ↦ ψ.compAddMonoidHom f) ψ) = ⇑((fun ψ ↦ ψ.compAddMonoidHom f) χ)
⊢ ⇑ψ = ⇑χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : ⇑((fun f ↦ ψ.compAddMonoidHom f) f) = ⇑((fun f ↦ ψ.compAddMonoidHom f) g)
⊢ ⇑f = ⇑g

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : ⇑((fun f ↦ ψ.compAddMonoidHom f) f) = ⇑((fun f ↦ ψ.compAddMonoidHom f) g)
⊢ ⇑f = ⇑g
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✝ : AddChar A M
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } x✝ = 0 x✝

Tactic:
;

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
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✝

Tactic:
;

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
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
⊢ ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0

Tactic:
split_ifs with h
  · simp [h]
  obtain ⟨x, hx⟩ := ne_one_iff.1 h
  refine eq_zero_of_mul_eq_self_left hx ?_
  rw [Finset.mul_sum]
  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

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

Goal state before:
pp: A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0

Tactic:
;

Goal state after:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : CommMonoid M
ψ : AddChar A M
x : A
⊢ (ψ.compAddMonoidHom negAddMonoidHom * ψ) x = 1 x

Tactic:
;

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : CommMonoid M
ψ : AddChar A M
x : A
⊢ (ψ.compAddMonoidHom negAddMonoidHom * ψ) 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
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝) * ψ (s * x✝)

Tactic:
;

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✝ = ψ (r * x✝) * ψ (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
x✝ : R
⊢ (ψ.mulShift 0) x✝ = 1 x✝

Tactic:
;

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
x✝ : R
⊢ (ψ.mulShift 1) x✝ = ψ x✝

Tactic:
;

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.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]
a✝ : N
⊢ (mapDomain f (s • x)).coeff a✝ = (s • mapDomain f x).coeff a✝

Tactic:
;

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
x✝ : S[M]
a✝ : O
⊢ ((mapDomainLinearMap R S (g ∘ f)) x✝).coeff a✝ = ((mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f) x✝).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
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
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✝

Tactic:
;

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.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn K id {y, x}

Tactic:
;

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn K id {y, x}
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s