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 β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Functor.Comp.mk ((fun x ↦ (fun x1 x2 ↦ x1 * x2) <$> x) <$> traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y))

Tactic:
]

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Functor.Comp.mk ((fun x ↦ (fun x1 x2 ↦ x1 * x2) <$> x) <$> traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y))
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = reduce (reduce L₁ ++ reduce L₂)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = x * y

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ Red L (reduce L)

Tactic:
]

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ Red L (reduce L)
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ i₃ (f₂ x) = 1

Tactic:
]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ i₃ (f₂ x) = 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ ∀ ⦃a b : α × Bool⦄ ⦃l₁ l₂ : List (α × Bool)⦄, L = l₁ ++ a :: b :: l₂ → a.1 = b.1 → a.2 = b.2

Tactic:
]

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ ∀ ⦃a b : α × Bool⦄ ⦃l₁ l₂ : List (α × Bool)⦄, L = l₁ ++ a :: b :: l₂ → a.1 = b.1 → a.2 = b.2
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (pure ∘ f) (of x) = pure (f <$> of x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ pure ((fun x2 ↦ f <$> of x * x2) (f <$> y)) = pure (f <$> of x * f <$> y)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2

Tactic:
]

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
x₁ : α
x₂ y₂ : Bool
l₁ l₂ : List (α × Bool)
hl : L = l₁ ++ (x₁, x₂) :: ((x₁, x₂).1, y₂) :: l₂
⊢ ((x₁, x₂).1, y₂).2 ≠ !(x₁, x₂).2
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).norm = (x * y).norm

Tactic:
]

Goal state after:
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.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ n = n

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
a : M₁
hy : i₂ (f₁ a) = i₂ x
⊢ f₂ x = 1

Tactic:
]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
a : M₁
hy : i₂ (f₁ a) = i₂ x
⊢ f₂ x = 1
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α = #α

pp: α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α

Tactic:
]

Goal state after:
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = max #α ℵ₀

Tactic:
]

Goal state after:
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = max #α ℵ₀
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀) =
    max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
a : M₁
hm : i₃ (f₂ (f₁ a)) = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X : Type u
⊢ #(FreeAlgebra R X) ≤ max (max #R #X) ℵ₀

Tactic:
by
  simpa using cardinalMk_le_max_lift R X

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
]

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0) =
    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then 1 else 0) = if p x then 1 else 0

Tactic:
]

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (if decide (p x) = true then 1 else 0) = if p x then 1 else 0
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥((FreeAlgebra.lift R) Subtype.val).range ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥((FreeAlgebra.lift R) Subtype.val).range ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ s.lcm f = s.prod f

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
h : (↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ s.lcm f = s.prod f
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (f a✝ + ∑ x ∈ s✝, f x).den ∣ GCDMonoid.lcm (f a✝).den (s✝.lcm fun i ↦ (f i).den)

Tactic:
]

Goal state after:
case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (f a✝ + ∑ x ∈ s✝, f x).den ∣ GCDMonoid.lcm (f a✝).den (s✝.lcm fun i ↦ (f i).den)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ map (algebraMap R K) g ∣ map (algebraMap R K) f

pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ IsUnit (C ((algebraMap R K) f.leadingCoeff))

Tactic:
]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ map (algebraMap R K) g ∣ map (algebraMap R K) f

R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ IsUnit (C ((algebraMap R K) f.leadingCoeff))
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✝ : AddCommGroupWithOne R
n : ℕ
⊢ -↑↑(n + 1) = -↑↑(n + 1)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
this : C ((algebraMap R K) g.leadingCoeff) = ↑u
⊢ map (algebraMap R K) r = 0

Tactic:
by
      simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ φ (f.coeff n✝) ∈ Ideal.map φ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
n✝ : ℕ
hn : n✝ < (Polynomial.map φ f).natDegree
⊢ φ (f.coeff n✝) ∈ Ideal.map φ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
⊢ ∀ {n : ℕ}, n < (f * f').natDegree → (f * f').coeff n ∈ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
⊢ ∀ {n : ℕ}, n < (f * f').natDegree → (f * f').coeff n ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C a = C a

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * f'.coeff x.2 ∈ 𝓟
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g

Tactic:
]

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g

Tactic:
hm,

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ 0 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False