mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s.tail.val = s.val.tail

Tactic:
cases s

Goal state after:
case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s' : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R ⟨val✝, property✝⟩ s'
this : head ⟨val✝, property✝⟩ = s'.head ∧ R (tail ⟨val✝, property✝⟩) s'.tail
r : R (tail ⟨val✝, property✝⟩) s'.tail
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
· rw [IH (results_think_iff.1 h)]
    rfl

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' = 0 ↔ s = nil

Tactic:
cases s

Goal state after:
case nil
α : Type u
⊢ nil.length' = 0 ↔ nil = nil

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' = 0 ↔ cons x✝ s✝ = nil
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' ≠ 0 ↔ ∃ x s', s = cons x s'

Tactic:
cases s

Goal state after:
case nil
α : Type u
⊢ nil.length' ≠ 0 ↔ ∃ x s', nil = cons x s'

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ (cons x✝ s✝).length' ≠ 0 ↔ ∃ x s', cons x✝ s✝ = cons x s'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ take 0 s = []

Tactic:
cases s

Goal state after:
case nil
α : Type u
⊢ take 0 nil = []

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ take 0 (cons x✝ s✝) = []
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h h✝ : s.Terminates
⊢ s.length h ≤ s.length h✝

Tactic:
exact le_rfl

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

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ match
    match
      match s.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
cases s

Goal state after:
case nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    nil.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    (cons x✝ s✝).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases s

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

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
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ s =>

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

Goal state before:
pp: case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ b, b ∈ cb.think ∧ R a b

Tactic:
rw [destruct_think]

Goal state after:
case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ b, b ∈ cb.think ∧ R a b
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ s =>

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)

Tactic:
intro s1

Goal state after:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 : Seq α
⊢ ∀ ⦃s₂ : Seq α⦄,
    (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1 s₂ →
      BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
        s₂.destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
s : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s.destruct
    s.destruct

Tactic:
cases s

Goal state after:
case nil
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) nil.destruct
    nil.destruct

case cons
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons x✝ s✝).destruct (cons x✝ s✝).destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, s) S).join.destruct (cons a (s.append S.join)).destruct

Tactic:
cases s

Goal state after:
case nil
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, nil) S).join.destruct (cons a (nil.append S.join)).destruct

case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x✝ s✝) S).join.destruct (cons a ((cons x✝ s✝).append S.join)).destruct
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome

Goal state after:
case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ s =>

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

Goal state before:
pp: α : Type u
s : Seq α
n m : ℕ
⊢ List.drop m (take n s) = take (n - m) (s.drop m)

Tactic:
by
  ext
  grind

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: 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

Tactic:
rcases eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ | h₁

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Monoid α
inst✝⁴ : Monoid β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a b : α
c d : β
hab : a ∣ b
hcd : c ∣ d
⊢ a • c ∣ b • d

Tactic:
by
  obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hab, hcd
  exact ⟨x • y, mul_smul_mul_comm a x c y⟩

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
⊢ Pairwise R s.tail

Tactic:
cases s

Goal state after:
case nil
α : Type u
R : α → α → Prop
h : Pairwise R nil
⊢ Pairwise R nil.tail

case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
cases s

Goal state after:
case nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret nil).join.destruct nil.destruct

case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret (Seq.cons x✝ s✝)).join.destruct
    (Seq.cons x✝ s✝).destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)

Tactic:
cases s

Goal state after:
case nil
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
⊢ join ((a, nil), nil) = (a, nil)

case cons
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a x✝ : β
s✝ : Seq β
⊢ join ((a, Seq.cons x✝ s✝), nil) = (a, Seq.cons x✝ s✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
x✝ : β
s : Seq β
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    ((Seq.cons x✝ s).append (Seq.map f S.join)).destruct ((Seq.cons x✝ s).append (Seq.map (map f) S).join).destruct

Tactic:
| cons _ s =>

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join

Tactic:
cases s

Goal state after:
case nil
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
⊢ map f (join ((a, nil), S)) = (map (map f) ((a, nil), S)).join

case cons
α : Type u
β : Type v
f : α → β
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ map f (join ((a, Seq.cons x✝ s✝), S)) = (map (map f) ((a, Seq.cons x✝ s✝), S)).join
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ s =>

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

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.squashGCF n = g

Tactic:
cases n with
  | zero =>
    change g.s.get? 0 = none at terminatedAt_n
    simp only [squashGCF, terminatedAt_n]
  | succ =>
    cases g
    simp only [squashGCF, mk.injEq, true_and]
    exact squashSeq_eq_self_of_terminated terminatedAt_n

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
⊢ P.toPoly.natDegree = 2

Tactic:
rw [of_a_eq_zero ha, natDegree_quadratic hb]

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
i : I
complete : e i * ∑ i, e i = e i * 1
⊢ IsIdempotentElem (e i)

Tactic:
rwa [Finset.mul_sum, Finset.sum_eq_single i (fun _ _ ne ↦ ortho ne.symm) (by simp at ·), mul_one]
    at complete

Goal state after:
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✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
have hf' : ∀ i, MapsTo (restrict f hp') (N' i) (N' i) := fun i x hx' ↦ by simpa using! hf i hx'

Goal state after:
ι : 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✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
⊢ (trace R ↥p) (restrict f hp') = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) i) =
      (contractLeft R M) ((b.dualBasis.tensorProduct b) i)

Tactic:
rintro ⟨i, j⟩

Goal state after:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) (i, j)) =
    (contractLeft R M) ((b.dualBasis.tensorProduct b) (i, j))
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_6
inst✝⁷ : CommRing R
inst✝⁶ : CharZero R
M : Type u_7
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
e : M →ₗ[R] M
he : IsIdempotentElem e
inst✝³ : Free R ↥e.range
inst✝² : Module.Finite R ↥e.range
inst✝¹ : Free R ↥e.ker
inst✝ : Module.Finite R ↥e.ker
⊢ (trace R M) e = 0 ↔ e = 0

Tactic:
rw [he.isProj_range.trace, Nat.cast_eq_zero, finrank_eq_zero_iff_of_free,
    Submodule.subsingleton_iff_eq_bot, range_eq_bot]

Goal state after:
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 - μ • 1)) ^ l) m = 0

Tactic:
smul_pow,

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 ^ l • (f - μ • 1) ^ l) m = 0
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x ↦ f (x * a)) (c / a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const a

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
  apply coe_mul_inv_eq_one
  apply Nat.Coprime.symm
  rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]

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

Goal state before:
pp: case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
⊢ Red tl1 TL →
    Red (hd1 :: tl1)
      (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
        TL)

Tactic:
intro ih

Goal state after:
case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail) TL)
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
cases isEmpty_or_nonempty α <;> simp [FreeCommRing]

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

Goal state before:
pp: case neg
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_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ False

Tactic:
apply hfmodP2

Goal state after:
case neg
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_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑(↑x✝.num / ↑x✝.den) = ↑x✝.num / ↑x✝.den

Tactic:
coe_div,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ≥0
⊢ ↑↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑(↑x✝.num / ↑x✝.den) = ↑x✝.num / ↑x✝.den

Tactic:
coe_div,

Goal state after:
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑↑x✝.num / ↑↑x✝.den = ↑x✝.num / ↑x✝.den
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:
by
  rw [← SetLike.mem_coe, coe_closure']
  simp [mem_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Submonoid M
p : (x : M) → x ∈ s.saturation → Prop
mem : ∀ (x : M) (hx : x ∈ s), p x ⋯
mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯
of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯
x : M
hx : x ∈ s.saturation
s' : SaturatedSubmonoid M :=
  { carrier := {x | ∃ (hx : x ∈ s.saturation), p x hx}, mul_mem' := ⋯, one_mem' := ⋯, mulSaturated := ⋯ }
⊢ p x hx

Tactic:
exact SaturatedSubmonoid.mem_sInf.mp hx s' (fun _ h ↦ ⟨_, mem _ h⟩) |>.2

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i i' : Fin (l + 1)
hii' : i ≤ i'
⊢ (fun i ↦ ⟨↑i + j, ⋯⟩) i ≤ (fun i ↦ ⟨↑i + j, ⋯⟩) i'

Tactic:
simpa only [Fin.mk_le_mk, add_le_add_iff_right] using! hii'

Goal state after: