mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [fastFibAux, binaryRec_eq]

Goal state after:
n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)
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:
rw [fastFibAux, binaryRec_eq]

Goal state after:
n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).2 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).1 +
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p ↦
                if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
              n).1 *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p ↦
                    if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                    else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                  n).2 -
            (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1),
        (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).2 ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p ↦
                  if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
                  else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
                n).1 ^
            2)) =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases SS with

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminatedAt_n

Goal state after:
case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ g.convs (n + 1) = g'.convs' n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
⊢ (∀ n > 3, P.toPoly.coeff n = 0) ∧
    P.toPoly.coeff 3 = P.a ∧ P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d

Tactic:
simp only [Cubic.toPoly, Polynomial.coeff_add, Polynomial.coeff_C, Polynomial.coeff_C_mul_X,
    Polynomial.coeff_C_mul_X_pow]
  grind [zero_add]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
suffices g.convs (n + 1) = g'.convs n by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
⊢ (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
s_nth_eq

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : (↑↑c).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      n =
    (↑f).coeff n

Tactic:
rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
      simpa using hn

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

Tactic:
refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _

Goal state after:
case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.range n
⊢ Commute (1 - x ^ n) x
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
i j : n
⊢ (matrix n c) (single i j x) (single i j y)

Tactic:
matrix_apply_single

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 j : n
⊢ c x y
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (1 - e a) * x = x
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
⊢ matrix n c.ofMatrix = c

Tactic:
by
  ext x y
  constructor
  · intro h
    rw [matrix_eq_sum_single x, matrix_eq_sum_single y]
    refine c.finsetSum _ fun i _ ↦ c.finsetSum _ fun j _ ↦ h i j i j
  · intro h i' j' i j
    simpa using c.mul (c.mul (c.refl <| single i i' 1) h) (c.refl <| single j' j 1)

Goal state after:
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: case mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).1 ∣ y.1 ∧ (fst✝, snd✝).2 ∣ y.2

Tactic:
cases y

Goal state after:
case mk.mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ∣ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 ∣ (fst✝, snd✝).2
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) id = ↑(finrank R M)

Tactic:
rw [← Module.End.one_eq_id, trace_one]

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
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = p.subtype.range ⊓ (f.genEigenspace μ) k

Tactic:
Submodule.range_subtype

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = p ⊓ (f.genEigenspace μ) k
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - (t * μ) • 1) ^ l) m = 0

Tactic:
mul_smul,

Goal state after:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - t • μ • 1) ^ l) m = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
hg : IsNilpotent (g - (algebraMap R (End R M)) μ)
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
by
  set n := g - algebraMap R _ μ
  replace hg : trace R M (f ∘ₗ n) = 0 := by
    rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]
    refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)
    exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)
  have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl
  have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp -- TODO Surely exists?
  rw [hμ, comp_add, map_add, hg, add_zero, this, map_smul, smul_eq_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)

Tactic:
let b := Module.Free.chooseBasis R M

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = (algebraMap R A) ((trace R M) f)
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)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1

Tactic:
inv_mul_cancel,

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)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * (1 * a⁻¹)) = 1
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 * (a⁻¹ * a) = a

Tactic:
inv_mul_cancel,

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 * 1 = a
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

Tactic:
obtain ⟨y, c⟩ := hd

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ (lift f) (of x) * (lift f) y = f x * (lift f) y

Tactic:
lift_of

Goal state after:
α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ f x * (lift f) y = f x * (lift f) y
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
b✝ c✝ : List (α × Bool)
a✝ : Relation.ReflTransGen Red.Step (reduce L₁) b✝
H1 : Red.Step b✝ c✝
H2 : reduce L₁ = b✝
⊢ reduce L₁ = c✝

Tactic:
| tail _ H1 H2 =>

Goal state after:
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
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
exact congr(∀ _ _, _ ∈ $Subtype.range_val)

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

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

Tactic:
exact congr(∀ _ _, _ ∈ $Subtype.range_val)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R ≃+* S
h : IsIntegrallyClosed R
x✝ : Algebra S R := f✝.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv ⋯
⊢ IsIntegrallyClosed S

Tactic:
let g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R ≃+* S
h : IsIntegrallyClosed R
x✝ : Algebra S R := f✝.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv ⋯
g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
⊢ IsIntegrallyClosed S
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: case right
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ (g ∘ f) a✝ = (δ * γ) • a✝

Tactic:
mul_smul,

Goal state after:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ (g ∘ f) a✝ = δ • γ • a✝
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
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : G
⊢ (Δ_[h] fun y ↦ f y • g) = Δ_[h] f • fun x ↦ g

Tactic:
by
  ext y
  simp only [fwdDiff, Pi.smul_apply', sub_smul]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
j n : ℕ
h : j < n
⊢ (Δ_[1]^[n] fun r ↦ r ^ j) = 0

Tactic:
induction n generalizing j with
  | zero => aesop
  | succ n ih =>
    have : (Δ_[1] fun (r : R) ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]
    exact sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
b : ↑Y.toLinOrd
⊢ (LinOrd.Hom.hom (ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f).hom) b = (LinOrd.Hom.hom (𝟙 Y).hom) b

Tactic:
apply hφ

Goal state after:
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ ((normalizedMooreComplex C).obj X).d (n + 1) n = objD X n

Tactic:
simp [-objD, -obj_X]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
by
  ext k
  dsimp [δ, Fin.succAbove]
  rcases i with ⟨i, _⟩
  rcases j with ⟨j, _⟩
  rcases k with ⟨k, _⟩
  split_ifs <;> · simp at * <;> lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
dsimp; rwa [← mono_iff_injective]

Goal state after: