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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
⊢ CharP A p

Tactic:
have := f.domain_nontrivial

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this : Nontrivial R
⊢ CharP A p
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q * 1
this : k = 1
⊢ CharP A p

Tactic:
mul_one

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
this✝ : Nontrivial R
H : Nat.Prime p
q : ℕ
hq : CharP A q
k : ℕ
e : p = q
this : k = 1
⊢ CharP A p
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)

Tactic:
apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed
  exact hQe.isClosedUnderLimitsOfShape hQi _

Goal state after:
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
⊢ RingHom.ker (algebraMap ℤ R) = Ideal.span {↑p}

Tactic:
by
  ext a
  simp [CharP.intCast_eq_zero_iff R p, Ideal.mem_span_singleton]

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
intro I hI
  constructor
  intro a b h_ab
  contrapose! hI
  -- `↑a - ↑b` is a unit contained in `I`, which contradicts `I ≠ ⊤`.
  refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))
  · simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]
  simpa only [Ne, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ ↑n • ψ = ↑n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz),

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑↑n))) ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
⊢ s.get? m = none → s.get? n = none

Tactic:
obtain ⟨f, al⟩ := s

Goal state after:
α : Type u
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ n = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none

Tactic:
· exact s.2 h

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n✝ : ℕ
n' : (↑s).tail n✝ = none
⊢ (↑s).tail (n✝ + 1) = none

Tactic:
obtain ⟨f, al⟩ := s

Goal state after:
α : Type u
β : Type v
γ : Type w
n✝ : ℕ
f : Stream' (Option α)
al : f.IsSeq
n' : (↑⟨f, al⟩).tail n✝ = none
⊢ (↑⟨f, al⟩).tail (n✝ + 1) = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
obtain ⟨f, al⟩ := s

Goal state after:
case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h : (fun a' ↦ (a', tail ⟨f, al⟩)) <$> some a' = some (a, s')
⊢ ⟨f, al⟩ = cons a s'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h' : s.tail = s'
⊢ s = s.tail.think

Tactic:
obtain ⟨f, al⟩ := s

Goal state after:
case none
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ⟨f, al⟩.val 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = (tail ⟨f, al⟩).think
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match f b with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x ↦ none) (f b)

Tactic:
match (f b) with
    | Sum.inl x => rfl
    | Sum.inr x => rfl

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ s.val m = some a → s.val n = some a

Tactic:
obtain ⟨f, al⟩ := s

Goal state after:
α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ⟨f, al⟩.val m = some a → ⟨f, al⟩.val n = some a
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s

Tactic:
Nat.min_zero,

Goal state after:
α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take 0 s
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
simp [length'_of_terminates h, length'_of_terminates h', length_cons h']

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
x' y' : FreeCommRing ((i : ι) × G i)
i : ι
x : G i
hx :
  (of G f i) x =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      x'
j : ι
y : G j
hy :
  (of G f j) y =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      y'
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ ∃ i x,
    (of G f i) x =
      (Ideal.Quotient.mk
          (Ideal.span
            {a |
              (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
                (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                  (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                    ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
        (x' * y')

Tactic:
· exact ⟨k, f i k hik x * f j k hjk y, by rw [map_mul, of_f, of_f, hx, hy]; rfl⟩

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
⊢ Function.Injective ⇑(lift G f P g Hg)

Tactic:
simp_rw [injective_iff_map_eq_zero] at injective ⊢
  intro z hz
  induction z using DirectLimit.induction_on with
  | ih _ g => rw [lift_of] at hz; rw [injective _ g hz, map_zero]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (bit false n).fastFibAux =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
by
  rw [fastFibAux, binaryRec_eq]
  · rfl
  · simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (bit true n).fastFibAux =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

Tactic:
by
  rw [fastFibAux, binaryRec_eq]
  · rfl
  · simp

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
⊢ P.toPoly ≠ 0

Tactic:
contrapose! h0
  rw [(toPoly_eq_zero_iff P).mp h0]
  exact ⟨rfl, rfl, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑(((decompose V) (x * 1)) i)

Tactic:
mul_one

Goal state after:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = ↑(((decompose V) x) i)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b = φ P.a * -(x + y + z)

Tactic:
by
  injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.c = φ P.a * (x * y + x * z + y * z)

Tactic:
by
  injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.d = φ P.a * -(x * y * z)

Tactic:
by
  injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : Option I
ne : i ≠ j
⊢ (fun x1 x2 ↦ x1.elim x e * x2.elim x e = 0) i j

Tactic:
rcases i with - | i <;> rcases j with - | j

Goal state after:
case none.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
ne : none ≠ none
⊢ none.elim x e * none.elim x e = 0

case none.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
j : I
ne : none ≠ some j
⊢ none.elim x e * (some j).elim x e = 0

case some.none
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i : I
ne : some i ≠ none
⊢ (some i).elim x e * none.elim x e = 0

case some.some
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
inst✝ : Fintype I
x : R
hx : IsIdempotentElem x
hx₁ : x * ∑ i, e i = 0
hx₂ : (∑ i, e i) * x = 0
i j : I
ne : some i ≠ some j
⊢ (some i).elim x e * (some j).elim x e = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
ortho : Pairwise fun x1 x2 ↦ e x1 * e x2 = 0
i : I
complete : e i * e i = e i * 1
⊢ IsIdempotentElem (e i)

Tactic:
mul_one

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : Fintype I
ortho : Pairwise fun x1 x2 ↦ e x1 * e x2 = 0
i : I
complete : e i * e i = e i
⊢ IsIdempotentElem (e i)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
intro M

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
⊢ M ∈ matrix n I.jacobson → M ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson

Tactic:
intro M

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
⊢ M ∈ (matrix n I).jacobson → M ∈ matrix n I.jacobson
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 = ⊥
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag = 0

Tactic:
by
  ext ⟨i, k⟩
  simp only [Matrix.diag_apply, Pi.zero_apply, toMatrix_apply, IsInternal.collectedBasis_coe]
  by_cases hi : σ i ∈ s
  · let j : s := ⟨σ i, hi⟩
    replace hσ : j ≠ i := fun hij ↦ hσ i <| Subtype.ext_iff.mp hij
    exact h.collectedBasis_repr_of_mem_ne b hσ <| hf _ <| Subtype.mem (b i k)
  · suffices f (b i k) = 0 by simp [this]
    simpa [hN _ hi] using hf i <| Subtype.mem (b i k)

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

Goal state before:
pp: R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ⊤) ↑((f.genEigenspace μ) ⊤)
⊢ IsNilpotent (LinearMap.restrict (f - μ • 1) h)

Tactic:
by
  apply isNilpotent_restrict_of_le
  on_goal 2 => apply isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ)
  rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ r ∈ corner e → e * r = r ∧ r * e = r

Tactic:
rintro ⟨r, rfl⟩; simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]

Goal state after:
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 * 1 = r

Tactic:
mul_one

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R[ε] R' := f.toAlgebra
⊢ Algebra R R'

Tactic:
exact Algebra.compHom _ (algebraMap R R[ε])

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).2 (x * 1) = (↑fg).2 x

Tactic:
mul_one

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).2 x = (↑fg).2 x
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
⊢ InjOn (fun x ↦ (f.genEigenspace x) k) {μ | (f.genEigenspace μ) k ≠ ⊥}

Tactic:
rintro μ₁ _ μ₂ hμ₂ hμ₁₂

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
a✝ : μ₁ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
μ₂ : R
hμ₂ : μ₂ ∈ {μ | (f.genEigenspace μ) k ≠ ⊥}
hμ₁₂ : (fun x ↦ (f.genEigenspace x) k) μ₁ = (fun x ↦ (f.genEigenspace x) k) μ₂
⊢ μ₁ = μ₂
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
⊢ Disjoint (f.genEigenrange μ ↑(finrank K V)) ((f.genEigenspace μ) ↑(finrank K V))

Tactic:
by
  have h :=
    calc
      Submodule.comap ((f - μ • 1) ^ finrank K V)
        (f.genEigenspace μ (finrank K V)) =
          LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
            (f - algebraMap K (End K V) μ) ^ finrank K V) := by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
      _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
              simp_rw [← pow_add, genEigenspace_nat]; rfl
      _ = f.genEigenspace μ (finrank K V) := by
              rw [genEigenspace_eq_genEigenspace_finrank_of_le]; lia
  rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map,
    Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h, genEigenspace_nat]
  apply Submodule.map_comap_le

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a

Tactic:
mul_one

Goal state after:
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a = a
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ toFreeMonoid { head := x, tail := xs } = ofList (x :: xs)

Tactic:
by
  suffices ∀ x : FreeMonoid α, (xs.map FreeMonoid.of).foldl (· * ·) x = x * ofList xs by
    simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)
  induction xs with grind [ofList_nil, ofList_cons]

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)
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
have hP : P.IsPrime := ker_isPrime (algebraMap R K)

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
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (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 * 1 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g

Tactic:
mul_one

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 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g
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
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
set P := ker (algebraMap R K)
  have hP : P.IsPrime := ker_isPrime (algebraMap R K)
  have hgP : g.leadingCoeff ∉ P := by
    simp only [mem_ker, P]
    obtain ⟨h, rfl⟩ := hg_div
    simp only [leadingCoeff_mul, map_mul, ne_eq, mul_eq_zero, not_or] at hf_lC
    exact hf_lC.1
  have map_dvd_pow_q :
      g.map (algebraMap R K) ∣ q.map (algebraMap R K) ^ p := by
    rw [← IsUnit.dvd_mul_left _, ← hfmodP]
    · exact Polynomial.map_dvd _ hg_div
    · simp_all
  obtain ⟨m, hm, hf⟩ := (dvd_prime_pow hq_irr.prime _).mp map_dvd_pow_q
  set r := g - C g.leadingCoeff * q ^ m
  have hg : g = C g.leadingCoeff * q ^ m + r := by ring
  have hr : r.map (algebraMap R K) = 0 := by
    obtain ⟨u, hu⟩ := hf.symm
    obtain ⟨a, ha, ha'⟩ := Polynomial.isUnit_iff.mp u.isUnit
    suffices C (algebraMap R K g.leadingCoeff) = u by
      simp [r, ← this, Polynomial.map_sub, ← hu, Polynomial.map_mul, map_C,
        Polynomial.map_pow, mul_comm]
    rw [← leadingCoeff_map_of_leadingCoeff_ne_zero _ hgP, ← hu, ← ha',
      leadingCoeff_mul, leadingCoeff_C, (hq_monic.map _).pow m, one_mul]
  use m, r, hg, hr
  intro hm
  rw [isPrimitive_iff_isUnit_of_C_dvd] at hf_prim
  rw [hm, pow_zero, mul_one] at hg
  suffices g.natDegree = 0 by
    obtain ⟨a, rfl⟩ := Polynomial.natDegree_eq_zero.mp this
    apply IsUnit.map
    apply hf_prim
    rwa [leadingCoeff_C] at hgP
  by_contra hg'
  apply hgP
  rw [hg, leadingCoeff, coeff_add, ← hg, coeff_C, if_neg hg', zero_add,
    mem_ker, ← coeff_map, hr, coeff_zero]

Goal state after: