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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
p q : ℕ
a : R
inst✝ : Fact True
hR : ¬p * q = 0
hch : ↑(p * q) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
hq : ringChar R = p * q
ha : a * ↑p = 1
h₃ : ¬p * q ∣ q
⊢ False

Tactic:
grind [ringChar.dvd]

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
x y : M
⊢ { toFun := fun a ↦ ⟨(x + y) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun a ↦ ⟨y ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp [add_tmul]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ), ↑(x + y).num /ₚ ↑(x + y).pnatDen = ↑x.num /ₚ ↑x.pnatDen + ↑y.num /ₚ ↑y.pnatDen

Tactic:
by
      intro a b
      simp only [Units.add_divp, pnatCast_eq_natCast, Rat.coe_pnatDen, divp_mul_eq_mul_divp,
        Units.divp_add, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq, Units.val_mul]
      trans (↑((a + b).num * a.den * b.den) : R)
      · simp_rw [Int.cast_mul, Int.cast_natCast]
        ring
      rw [Rat.add_num_den' a b]
      simp

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ Prod.fst <$> (cons a s).destruct = some a

Tactic:
destruct_cons,

Goal state after:
α : Type u
a : α
s : Seq α
⊢ Prod.fst <$> some (a, s) = some a
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.head = none ↔ s = nil

Tactic:
constructor
  · apply head_eq_none
  · intro h
    simp [h]

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

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ s₁ = s₂

Tactic:
apply eq_of_bisim motive _ base

Goal state after:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ IsBisimulation motive
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case nil
α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ ([] ++ₛ a).get ([].length + n) = a.get n

Tactic:
simp [Nat.succ_add, *, cons_append_stream]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons
α : Type u
n : ℕ
x : List α
a : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : (tail✝ ++ₛ a).get (tail✝.length + n) = a.get n
⊢ (head✝ :: tail✝ ++ₛ a).get ((head✝ :: tail✝).length + n) = a.get n

Tactic:
simp [Nat.succ_add, *, cons_append_stream]

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

Goal state before:
pp: α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results a s.length

Tactic:
rw [← get_eq_of_mem _ h]

Goal state after:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length + 1 ≤ n + 1

Tactic:
apply Nat.succ_le_succ
      apply Nat.find_min'
      apply this

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

Goal state before:
pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (cons x✝ (s✝.append nil)).destruct (cons x✝ s✝).destruct

Tactic:
destruct_cons,

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (some (x✝, s✝.append nil)) (cons x✝ s✝).destruct
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rcases eq_or_ne (fract v) 0 with h | h

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v = 0
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rcases eq_or_ne (fract v) 0 with h | h

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v = 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
p : α → Prop
hd : α
tl : Seq α
h_hd : p hd
h_tl : ∀ x ∈ tl, p x
⊢ ∀ x ∈ cons hd tl, p x

Tactic:
by
  simp only [mem_cons_iff, forall_eq_or_imp] at *
  exact ⟨h_hd, h_tl⟩

Goal state after:
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: f : ℕ → ℕ
hf : IsStrongDvdSequence f
⊢ IsDvdSequence f

Tactic:
intro a b hab

Goal state after:
f : ℕ → ℕ
hf : IsStrongDvdSequence f
a b : ℕ
hab : a ∣ b
⊢ f a ∣ f b
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
⊢ False

Tactic:
rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
j : ι
hij : ?m.64 ≤ j
hf : (f' ?m.64 j hij) 1 = 0
⊢ False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
⊢ b.drop (a.length ha) ≠ nil

Tactic:
intro hb'

Goal state after:
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb' : b.drop (a.length ha) = nil
⊢ False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
ha' : (a.drop (a.length ha)).length' = (cons a_hd a_tl).length'
⊢ False

Tactic:
simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'

Goal state after:
case pos.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
ha' : 0 = a_tl.length' + 1
⊢ False
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
conv_rhs => rw [← mod_add_div' n m]

Goal state after:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib (n % m + n / m * m))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case H1
m n : ℕ
a✝ : 0 < m
h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
| H1 m n _ h' =>

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly

Tactic:
by
  simp only [toPoly, C_neg, C_add, C_mul]
  ring1

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.b = Q.b

Tactic:
by rw [← coeff_eq_b, h, coeff_eq_b]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d ≠ 0
⊢ P.toPoly.degree = 0

Tactic:
by
  rw [of_c_eq_zero ha hb hc, degree_C hd]

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
inst✝ : Fintype I
ortho : Pairwise fun x1 x2 ↦ e x1 * e x2 = 0
complete : ∑ i, e i = 1
⊢ ∀ (i : I), IsIdempotentElem (e i)

Tactic:
i

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
complete : ∑ i, e i = 1
i : I
⊢ IsIdempotentElem (e i)
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c (f.sum fun x ↦ ⇑(h x)) (g.sum fun x ↦ ⇑(h' x))

Tactic:
exact c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H

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

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker) → x ∈ ((f - μ • 1) ^ k).ker

Tactic:
rintro ⟨l, hl, hx⟩
    simp only [Nat.cast_le] at hl
    exact (f - μ • 1).iterateKer.monotone hl hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
⊢ (matrix n c).ofMatrix x y

Tactic:
i

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i : n
⊢ ∀ (j : n), (matrix n c) (single i j x) (single i j y)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : c x y
i' j' : n
⊢ c.ofMatrix (x i' j') (y i' j')

Tactic:
i

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : c x y
i' j' i : n
⊢ ∀ (j : n), c (single i j (x i' j')) (single i j (y i' j'))
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ {x | ∃ N ∈ I, N i j = x} → r ∈ ↑(equivMatrix.symm I)

Tactic:
· rintro ⟨n, hn, rfl⟩
    rw [SetLike.mem_coe, mem_iff, equivMatrix_symm_apply_ringCon,
      RingCon.coe_ofMatrix_eq_relationMap i j]
    exact ⟨n, 0, (I.mem_iff n).mp hn, rfl, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
MI : M ∈ matrix n I
⊢ M ∈ matrix n J

Tactic:
i

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
MI : M ∈ matrix n I
i : n
⊢ ∀ (j : n), J.ringCon (M i j) (0 i j)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ True ∧ True

Tactic:
true_and

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Tactic:
by
  replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)
  suffices (⨆ i ∈ s, N i).map f ≤ ⨆ i ∈ s, N i from Submodule.map_le_iff_le_comap.mp this
  simpa only [Submodule.map_iSup] using iSup₂_mono <| fun i _ ↦ hf i

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Goal state after:
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x : FreeMagma α
⊢ ∀ (x y : FreeMagma α), f x = g x → f y = g y → f (x * y) = g (x * y)

Tactic:
by intros; simp only [map_mul, *]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : N₂
⊢ ∃ a, i₃ a = g₂ y

Tactic:
obtain ⟨y, rfl⟩ := hi₂.2 y

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : M₂
⊢ ∃ a, i₃ a = g₂ (i₂ y)
Module: Mathlib.Algebra.FreeMonoid.Count

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

Tactic:
rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]

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.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : N₂
⊢ ∃ a, i₃ a = g₂ y

Tactic:
obtain ⟨y, rfl⟩ := hi₂.2 y

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : M₂
⊢ ∃ a, i₃ a = g₂ (i₂ y)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -((algebraMap R S) p * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
neg_eq_neg_one_mul,

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = -1 * ((algebraMap R S) p * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(normSq a) ↔ a = ↑a.re

Tactic:
← star_eq_self,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = ↑(normSq a) ↔ star a = a
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

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

Tactic:
· rw [f.coeff_eq_zero_of_natDegree_lt]
        · exact P.zero_mem
        · simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]

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:
by
  simp [fwdDiff_iter_eq_sum_shift, add_right_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Finset β
h : s.Nonempty
⊢ ↑(0 • s) = ↑0

Tactic:
by simpa using @Set.zero_smul_set α _ _ _ _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • s = univ ↔ s = univ

Tactic:
exact_mod_cast smul_finset_eq_univ (α := Units α) (a := Units.mk0 a ha)

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
⊢ f (v i) ≠ 1

Tactic:
suffices v i ≠ 1 → 1 < f (v i) from (this hv_one).ne'

Goal state after:
ι✝ : Type u_1
G✝ : Type u_3
S✝ : Type u_4
inst✝⁶ : CommGroup G✝
inst✝⁵ : LinearOrder S✝
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
hi : v i ∈ closure (v '' s)
⊢ v i ≠ 1 → 1 < f (v i)
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasKernel (𝟙 X - p)
⊢ HasEqualizer (𝟙 X) p

Tactic:
apply Preadditive.hasEqualizer_of_hasKernel

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ P.p ≫ P.p ≫ P.p = P.p

Tactic:
by repeat' rw [P.idem]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom

Tactic:
by
        slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp]

Goal state after: