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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
by_cases hi : σ i ∈ s

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∈ s
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

case neg
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ e i * (r₁ * e i * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)

Tactic:
conv in (r₁ * _ * r₂) => rw [← (he.idem i).eq]

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ e i * (r₁ * (e i * e i) * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (((f - μ • 1) ^ finrank K V) ∘ₗ (f - μ • 1) ^ finrank K V).ker =
    ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V).ker

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ((f - μ • 1) ^ (finrank K V + finrank K V)).ker

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
⊢ 0 < finrank R S

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ∑ x, (-1) ^ ↑x • ↑(finrank k (V x)) = 0

Tactic:
refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_

Goal state after:
case refine_1
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V 0)) = ↑(finrank k ↥(f 0).range)

case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)

case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h1
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst
      ({ re := TrivSqZeroExt.fst (x✝ * y✝).re, imI := TrivSqZeroExt.fst (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.fst (x✝ * y✝).imJ, imK := TrivSqZeroExt.fst (x✝ * y✝).imK },
        { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK }) =
    TrivSqZeroExt.fst
      (({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK },
          { re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK }) *
        ({ re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK },
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ ({ re := TrivSqZeroExt.fst (x✝ + y✝).re, imI := TrivSqZeroExt.fst (x✝ + y✝).imI,
        imJ := TrivSqZeroExt.fst (x✝ + y✝).imJ, imK := TrivSqZeroExt.fst (x✝ + y✝).imK },
      { re := TrivSqZeroExt.snd (x✝ + y✝).re, imI := TrivSqZeroExt.snd (x✝ + y✝).imI,
        imJ := TrivSqZeroExt.snd (x✝ + y✝).imJ, imK := TrivSqZeroExt.snd (x✝ + y✝).imK }) =
    ({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
          imK := TrivSqZeroExt.fst x✝.imK },
        { re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
          imK := TrivSqZeroExt.snd x✝.imK }) +
      ({ re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
          imK := TrivSqZeroExt.fst y✝.imK },
        { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
          imK := TrivSqZeroExt.snd y✝.imK })

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
h : [(x, b)] = L2 ++ (x', b') :: (x', !b') :: L3
this : [(x, b)].length = (L2 ++ (x', b') :: (x', !b') :: L3).length
⊢ False

Tactic:
grind

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
r : reduce L1 = []
⊢ List.rec [(x, b)] (fun head tail tail_ih ↦ if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail) [] =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
dsimp; intro h
      exfalso
      have := congr_arg List.length h
      grind

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))

Tactic:
← quot_mk_assoc c d,

Goal state after:
case refine_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))

Tactic:
← quot_mk_assoc c d,

Goal state after:
case refine_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * f * b))
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

Tactic:
rfl

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₄
m : M₃
hm : i₃ m = 1
h : i₄ (f₃ m) = 1
⊢ f₃ m = 1

Tactic:
rwa [map_eq_one_iff _ hi₄] at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (reduce (invRev w)) (invRev (reduce w))

Tactic:
rw [← red_invRev_iff, invRev_invRev]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

Tactic:
exact reduce.not (h.trans hl)

Goal state after:
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:
rfl

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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ Nonempty (CommRing α)

Tactic:
by
  obtain hR | hR := finite_or_infinite α
  · obtain ⟨x⟩ := nonempty_fintype α
    have : NeZero (Fintype.card α) := ⟨by simp⟩
    classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩
  · have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
    exact ⟨e.commRing⟩

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 3, ⋯⟩ =
    x✝ ⟨0 + 3, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 2, ⋯⟩ =
    x✝ ⟨0 + 2, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0 + 1, ⋯⟩ =
    x✝ ⟨0 + 1, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case step.step.step.refl
R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) ⟨0, ⋯⟩ =
    x✝ ⟨0, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zero
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✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case add
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✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ + y✝) = (equivProd c₁ c₂ c₃) x✝ + (equivProd c₁ c₂ c₃) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case neg
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✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (-x✝) = -(equivProd c₁ c₂ c₃) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case sub
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✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ - y✝) = (equivProd c₁ c₂ c₃) x✝ - (equivProd c₁ c₂ c₃) y✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case nsmul
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✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℕ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case zsmul
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✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℤ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

Tactic:
rfl

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 : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False

Tactic:
replace hn := hn.trans_le natDegree_mul_le

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 : ℕ
x : ℕ × ℕ
hx : x.1 + x.2 = n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
hn : n < f.natDegree + f'.natDegree
⊢ False
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 : 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
P : Ideal R := ⋯
hP : P.IsPrime
m : ℕ
hm✝ : m ≤ p
hm : m = 0
a : R
hg_div : C a ∣ f
hgP : (C a).leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) (C a) ∣ map (algebraMap R K) q ^ p
hf : Associated (map (algebraMap R K) (C a)) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : C a = C (C a).leadingCoeff + r
hr : map (algebraMap R K) r = 0
this : (C a).natDegree = 0
⊢ C a ∣ f

Tactic:
rwa [leadingCoeff_C] at hgP

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ IsIntegrallyClosedIn R A →
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

pp: case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x) →
    IsIntegrallyClosedIn R A

Tactic:
· rintro ⟨_, cl⟩
    simp_all

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x) →
    IsIntegrallyClosedIn R A
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟

Tactic:
rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one,
    Finset.sum_insert Finset.notMem_range_self, Finset.sum_range, hmo.coeff_natDegree, one_mul] at
    *

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : x ^ f.natDegree + ∑ i, f.coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟
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:
rfl

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case e'_2.e'_8
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ y' * x = ↑⟨y, hy⟩ * x'

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f

Tactic:
by
  apply toPartialEquiv_injective
  rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: case inl
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : α
⊢ (a • inl val✝).swap = a • (inl val✝).swap

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: case inr
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
val✝ : β
⊢ (a • inr val✝).swap = a • (inr val✝).swap

Tactic:
rfl

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 ⧸ P) (FractionRing (R ⧸ P))).comp (algebraMap R (R ⧸ P))) = P

Tactic:
ker_comp_of_injective

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.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:
rfl

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

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

Tactic:
rw [← SetLike.mem_coe, coe_closure']
  simp [mem_mul]

Goal state after:
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
m : M
n : ℕ
y : M
⊢ Δ_[h]^[n] (fun r ↦ f (r + m)) y = Δ_[h]^[n] f (y + m)

Tactic:
simp [fwdDiff_iter_eq_sum_shift, add_right_comm]

Goal state after:
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 * (-1) ^ 1 * a * b = (-1) ^ k * (-1) ^ 1 * (a * b)

Tactic:
npow_one,

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 * -1 * a * b = (-1) ^ k * -1 * (a * b)
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 ^ 1) = ↑n ^ m * ↑n ^ 1

Tactic:
npow_one,

Goal state after:
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 ^ 1
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 ^ 1) = ↑n ^ (m + 1)

Tactic:
npow_one,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑(n ^ m * n) = ↑n ^ (m + 1)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: n : ℕ
m : ℤ
⊢ (∃ x, ↑n * x = m) ↔ ∃ c, m = ↑n * c

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
x : G₀ˣ × H₀ˣ
⊢ (fst G₀ H₀) ↑x = ↑x.1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
x : G₀ˣ × H₀ˣ
⊢ (snd G₀ H₀) ↑x = ↑x.2

Tactic:
rfl

Goal state after: