mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ 0 ∈ P

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ f.natDegree < n

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ 0 ∈ P

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ f.natDegree < n
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
hq0 : a ≠ 0
⊢ star a = -a ↔ star a = -a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a • s ↔ b ∈ a • s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a • b ∈ s ↔ a • b ∈ s

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfmodP2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ f.coeff 0 ∉ ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2

Tactic:
]

Goal state after:
case hfmodP2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ f.coeff 0 ∉ ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑x✝.num / ↑x✝.den = ↑x✝.num / ↑x✝.den

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker ((algebraMap (R ⧸ P) (FractionRing (R ⧸ P))).comp (algebraMap R (R ⧸ P))) = P

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker ((algebraMap (R ⧸ P) (FractionRing (R ⧸ P))).comp (algebraMap R (R ⧸ P))) = P
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ s = univ ↔ s = univ

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker (algebraMap R (R ⧸ P)) = P

pp: case hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ Function.Injective ⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ ker (algebraMap R (R ⧸ P)) = P

case hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ Function.Injective ⇑(algebraMap (R ⧸ P) (FractionRing (R ⧸ P)))
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑x✝.num / ↑x✝.den = ↑x✝.num / ↑x✝.den

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
q : ℚ
⊢ ↑↑q ^ 2 = ↑↑q ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
⊢ #(R × R × R × R) = #R ^ 4

Tactic:
]

Goal state after:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #(R × R × R × R) = #R ^ 4
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #R = #R

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
⊢ #R ^ 4 = #R ^ 4

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ ↑I = s ∪ univ * s

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ ↑I = s ∪ univ * s
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ s ∪ univ * s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ⊆ univ * s

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ⊆ univ * s
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ univ * s ↔ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ univ * s ↔ ∃ y, ∃ z ∈ s, y * z = x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ Δ_[h]^[n] x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝

Tactic:
]

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

Goal state before:
pp: case one
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m : ℕ+
⊢ x ^ m = x ^ m

Tactic:
]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ (x ^ m) ^ k * x ^ m = (x ^ m) ^ k * x ^ m

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
]

Goal state after:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
]

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = shiftₗ M G h - 1
⊢ ((shiftₗ M G h - 1) ^ n) f y = ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ k * x = x ^ k * x

Tactic:
]

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

Goal state before:
pp: case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y

Tactic:
]

Goal state after:
case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    ∑ c ∈ range (n + 1), (shiftₗ M G h ^ c * (-1) ^ (n - c) * ↑(n.choose c)) f y
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h)

Tactic:
]

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

Goal state before:
pp: case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
⊢ ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) =
    (∑ m ∈ range (n + 1), shiftₗ M G h ^ m * (-1) ^ (n - m) * ↑(n.choose m)) f y

Tactic:
· rw [LinearMap.sum_apply, sum_apply]
    congr 1 with k
    have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G))
              = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast
    rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]

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

Goal state before:
pp: case zero
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m : ℕ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
⊢ (x ^ m) ^ n * x ^ m = (x ^ m) ^ n * x ^ m

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
]

Goal state after:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ -(-1) ^ k * a * b = -(-1) ^ k * (a * b)

Tactic:
]

Goal state after:
case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ -(-1) ^ k * a * b = -(-1) ^ k * (a * b)
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ((fwdDiffₗ M G h + 1) ^ n) f y = ((fwdDiffₗ M G h + 1) ^ n) f y

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n m : ℕ
ih : ↑(n ^ m) = ↑n ^ m
⊢ ↑n ^ m * ↑n = ↑n ^ m * ↑n

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑n ^ m * ↑n = ↑n ^ m * ↑n

Tactic:
]

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

Goal state before:
pp: m k : ℕ
hmn : m < m + k + 1
⊢ m + k + 1 = k + 1 + m

Tactic:
by ring

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

Goal state before:
pp: case inr.inr
n k : ℕ
hnm : n < n + k + 1
⊢ Δ_[1]^[n] (fun x ↦ ↑(x.choose (n + k + 1))) 0 = if n = n + k + 1 then 1 else 0

Tactic:
simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]

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

Goal state before:
pp: case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * (φ (x + h) - φ x)

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range j, Δ_[1]^[n] (j.choose k • fun r ↦ r ^ k) = 0

Tactic:
]

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range j, Δ_[1]^[n] (j.choose k • fun r ↦ r ^ k) = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ (j.choose i • Δ_[1]^[n] fun r ↦ r ^ i) = 0

Tactic:
ih (by have := mem_range.1 hi; lia),

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ j.choose i • 0 = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ P.coeff P.natDegree • ↑P.natDegree ! x = P.coeff P.natDegree • ↑P.natDegree ! x

pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0

Tactic:
]

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(image2 (fun x1 x2 ↦ x1 * x2) s t) ≤ #↑s * #↑t

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(image2 (fun x1 x2 ↦ x1 * x2) s t) ≤ #↑s * #↑t
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] fun i ↦ P.leadingCoeff • ↑P.natDegree ! i) x = 0 x

Tactic:
]

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] fun i ↦ P.leadingCoeff • ↑P.natDegree ! i) x = 0 x
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s = #↑s

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(image2 (fun x1 x2 ↦ x1 / x2) s t) ≤ #↑s * #↑t

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(image2 (fun x1 x2 ↦ x1 / x2) s t) ≤ #↑s * #↑t
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Small

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑((fun x ↦ -x) '' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑((fun x ↦ -x) '' s)
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ((v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2) =
    (v.prod fun x1 x2 ↦ f x1 ^ x2) * w.prod fun x1 x2 ↦ f x1 ^ x2

pp: case h.h_zero
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

pp: case h.h_add
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
]

Goal state after:
case h.h_zero
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

case h.h_add
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℤ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℤ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℤ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a.prod fun a b ↦ f a ^ (-b)

pp: case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∀ (a : ι), f a ^ 0 = 1

Tactic:
]

Goal state after:
case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 ↦ f x1 ^ x2)⁻¹ = a.prod fun a b ↦ f a ^ (-b)

case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∀ (a : ι), f a ^ 0 = 1
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Goal state after:
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) → x ∈ closure (Set.range f)
Module: Mathlib.Algebra.Group.Subgroup.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
]

Goal state after:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z