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

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
;

Goal state after:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ ⇑(toFreeSemigroup.comp (map f)) ∘ of = ⇑((FreeSemigroup.map f).comp toFreeSemigroup) ∘ of

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ ⇑(toFreeSemigroup.comp (map f)) ∘ of = ⇑((FreeSemigroup.map f).comp toFreeSemigroup) ∘ of
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + y.length = (x * y).length

Tactic:
;

Goal state after:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + y.length = (x * y).length
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x✝ : α
⊢ (⇑(((FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)).comp
                (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup)).comp
            Magma.AssocQuotient.of) ∘
        FreeMagma.of)
      x✝ =
    (⇑((MulHom.id (Magma.AssocQuotient (FreeMagma α))).comp Magma.AssocQuotient.of) ∘ FreeMagma.of) x✝

Tactic:
;

Goal state after:
α : Type u
x✝ : α
⊢ (⇑(((FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of)).comp
                (Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup)).comp
            Magma.AssocQuotient.of) ∘
        FreeMagma.of)
      x✝ =
    (⇑((MulHom.id (Magma.AssocQuotient (FreeMagma α))).comp Magma.AssocQuotient.of) ∘ FreeMagma.of) x✝
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
⊢ ⇑((Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).comp
          (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of))) ∘
      FreeSemigroup.of =
    ⇑(MulHom.id (FreeSemigroup α)) ∘ FreeSemigroup.of

Tactic:
;

Goal state after:
α : Type u
⊢ ⇑((Magma.AssocQuotient.lift FreeMagma.toFreeSemigroup).comp
          (FreeSemigroup.lift (⇑Magma.AssocQuotient.of ∘ FreeMagma.of))) ∘
      FreeSemigroup.of =
    ⇑(MulHom.id (FreeSemigroup α)) ∘ FreeSemigroup.of
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
⊢ x ∈ Set.range ⇑toFreeMonoid ↔ x ∈ {1}ᶜ

Tactic:
;

Goal state after:
α : Type u_1
x : FreeMonoid α
⊢ x ∈ Set.range ⇑toFreeMonoid ↔ x ∈ {1}ᶜ
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Function.onFun Nat.Coprime f)
x✝¹ x✝ : ℕ
⊢ x✝¹.Coprime x✝ ↔ IsRelPrime x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Function.onFun Nat.Coprime f)
x✝¹ x✝ : ℕ
⊢ x✝¹.Coprime x✝ ↔ IsRelPrime x✝¹ x✝
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : m = 0
⊢ IsUnit g

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : n = 0
⊢ IsUnit h

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : n = 0
⊢ IsUnit h
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
;

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
inst✝ : IsFractionRing (↥S) A
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ∀ ⦃x : A⦄, x ∈ ofClass S → x ∈ T

Tactic:
;

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ∀ ⦃x : A⦄, x ∈ ofClass S → x ∈ T
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
this : x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
exact mul_mem_right _ _ this

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a✝ b✝ : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re + b.re + c₂ * (a.imI + b.imI) = a.re + c₂ * a.imI + (b.re + c₂ * b.imI)

Tactic:
;

Goal state after:
case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a✝ b✝ : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
a b : ℍ[R,c₁,c₂,c₃]
⊢ a.re + b.re + c₂ * (a.imI + b.imI) = a.re + c₂ * a.imI + (b.re + c₂ * b.imI)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI

Tactic:
;

Goal state after:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (↑(2 * a.re + c₂ * a.imI) - a) * a = a * (↑(2 * a.re + c₂ * a.imI) - a)

Tactic:
;

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ (↑(2 * a.re + c₂ * a.imI) - a) * a = a * (↑(2 * a.re + c₂ * a.imI) - a)
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.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹
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
a : R
⊢ a ∈ ker (algebraMap R (R ⧸ P)) ↔ a ∈ 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
a : R
⊢ a ∈ ker (algebraMap R (R ⧸ P)) ↔ a ∈ P
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ (op a • s)⁻¹ ↔ a✝ ∈ a⁻¹ • s⁻¹
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
a n : ℕ
⊢ (∃ y ∈ s, a + y = n) ↔ a ≤ n ∧ n - a ∈ s

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
a n : ℕ
⊢ (∃ y ∈ s, a + y = n) ↔ a ≤ n ∧ n - a ∈ s
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.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.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
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝

Tactic:
;

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝³ x✝² : ℕ+
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝

Tactic:
;

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝³ x✝² : ℕ+
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝³ x✝² : ℕ
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝

Tactic:
;

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝³ x✝² : ℕ
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 0) x✝ = 1 x✝

Tactic:
;

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 0) x✝ = 1 x✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → MulOneClass (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ
inst✝ : ∀ (i : ι), NatPowAssoc (α i)
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ 1) x✝ = x✝¹ x✝
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
this : i < j
⊢ i < n

Tactic:
;

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
this : i < j
⊢ i < n
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
this : i < n
⊢ i < n

Tactic:
;

Goal state after:
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
this : i < n
⊢ i < n
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 + P.natDegree] (fun x ↦ eval x P) x = 0 x

Tactic:
Function.iterate_add_apply,

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] (Δ_[1]^[P.natDegree] fun x ↦ eval x P) x = 0 x
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.Subgroup.Finsupp

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
;

Goal state after:
case mem
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2
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
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2

Tactic:
;

Goal state after:
case h
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
;

Goal state after:
case mem
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2

Tactic:
;

Goal state after:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 ↦ f x1 ^ x2
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝

Tactic:
;

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
f : G → α
x✝ : G
⊢ τ 0 f x✝ = f x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ a (τ b f) x✝ = τ (a + b) f x✝

Tactic:
;

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ a (τ b f) x✝ = τ (a + b) f x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ (a + b) f x✝ = τ a (τ b f) x✝

Tactic:
;

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
x✝ : G
⊢ τ (a + b) f x✝ = τ a (τ b f) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝

Tactic:
;

Goal state after:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f

Tactic:
;

Goal state after:
G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i