mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : Algebra R S
inst✝⁶ : Module R M₁
inst✝⁵ : Module S M₁
inst✝⁴ : IsScalarTower R S M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module S M₂
inst✝ : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ ∀ (x y : (M₁ × M₂) ⊗[R] M₃),
    (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
              (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
          (c • x) =
        c •
          (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            x →
      (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            (c • y) =
          c •
            (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                  (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
              y →
        (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            (c • (x + y)) =
          c •
            (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                  (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
              (x + y)

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

Tactic:
simp only [AlgHom.toUnder_right, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        Pi.evalAlgHom_apply, Under.comp_right, comp_apply, AlgEquiv.toUnder_hom_right_apply,
        Algebra.TensorProduct.piRight_tmul]

Goal state after:
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
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
let e : A ≅
      CommRingCat.mkUnder R
        (AlgHom.equalizer (R := R)
          (CommRingCat.toAlgHom (pres.diag.map .left))
          (CommRingCat.toAlgHom (pres.diag.map .right))) :=
    (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
      HasLimit.isoOfNatIso (diagramIsoParallelPair _) ≪≫ limit.isoLimitCone
        ⟨CommRingCat.Under.equalizerFork (pres.diag.map .left) (pres.diag.map .right),
          CommRingCat.Under.equalizerForkIsLimit
            (pres.diag.map .left) (pres.diag.map .right)⟩

Goal state after:
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
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥((CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left)).equalizer
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag) ≪≫
      limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ ¬p ∣ ringChar R → IsUnit ↑p

Tactic:
intro h
    rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩
    apply_fun ((↑) : ℤ → R) at hab
    push_cast at hab
    rw [hch, mul_zero, add_zero, mul_comm] at hab
    exact .of_mul_eq_one a hab

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
g : X ⟶ Y
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.IsStableUnderBaseChange
h : f = g
A : P.Over Q Y
⊢ ((pullbackCongr h).hom.app A).left ≫ pullback.fst A.hom g = pullback.fst A.hom f

Tactic:
by
  subst h
  simp [pullbackCongr]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ∃ p > 0, MixedCharZero R p
⊢ P

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P

Tactic:
· rcases h with ⟨p, ⟨H, hp⟩⟩
    rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
    exact h_mixed p H hp

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a

Tactic:
← const_eq

Goal state after:
α : Type u
a : α
this : (const a).tail = const a
⊢ (const a).tail = const a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1
α : 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 α
⊢ ∀ (a : α), R (pure a) s' → BisimO R (pure a).destruct s'.destruct → (pure a).head = s'.head ∧ R (pure a).tail s'.tail

Tactic:
intro r'

Goal state after:
case refine_1
α : 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 (pure r') s' → BisimO R (pure r').destruct s'.destruct → (pure r').head = s'.head ∧ R (pure r').tail s'.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2
α : 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 α
⊢ ∀ (s : Computation α),
    R s.think s' → BisimO R s.think.destruct s'.destruct → s.think.head = s'.head ∧ R s.think.tail s'.tail

Tactic:
intro r'

Goal state after:
case refine_2
α : 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' r' : Computation α
⊢ R r'.think s' → BisimO R r'.think.destruct s'.destruct → r'.think.head = s'.head ∧ R r'.think.tail s'.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ n < x.length

Tactic:
by simpa using h

Goal state after:
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:
rw [Nat.min_zero, List.take_zero, take_zero]

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

Goal state before:
pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ s.Terminates

Tactic:
exact ⟨⟨_, _, h.symm⟩⟩

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

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', a₁ :: l₁, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
Stream'.cycle_g_cons,

Goal state after:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: corec Stream'.cycleF Stream'.cycleG (a₁, l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ (s.toList h)[n]? = some k ↔ s.get? n = some k

Tactic:
simp only [toList, getElem?_take, Nat.lt_find_iff, length,
    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ s.get? n = some k → ∀ m ≤ n, ¬s.get? m = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
rw [← bind_pure] at h

Goal state after:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b
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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (Polynomial.map (f' i₁ i h1) p₁ + Polynomial.map (f' i₂ i h2) p₂) =
    q₁ + q₂

Tactic:
rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]
        congr 2 <;> ext x <;> simp_rw [RingHom.comp_apply, of_f]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ map f (cons a ⟨s, al⟩) = cons (f a) (map f ⟨s, al⟩)

Tactic:
by apply Subtype.ext; dsimp [cons, map]; rw [Stream'.map_cons]; rfl

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R (cons hd nil)

Tactic:
apply Pairwise.cons

Goal state after:
case h_hd
α : Type u
R : α → α → Prop
hd : α
⊢ ∀ x ∈ nil, R hd x

case h_tl
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R nil
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
rw [two_mul, fib_add]

Goal state after:
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i : ℕ
x : α
hx : x ∈ s.get? i
y : α
k : ℕ
h_ij : i < i + k + 1
hy : y ∈ s.get? (i + k + 1)
⊢ R x y

Tactic:
clear h_ij

Goal state after:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i : ℕ
x : α
hx : x ∈ s.get? i
y : α
k : ℕ
hy : y ∈ s.get? (i + k + 1)
⊢ R x y
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ n.fastFibAux = (fib n, fib (n + 1))

Tactic:
refine Nat.binaryRec ?_ ?_ n

Goal state after:
case refine_1
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))

case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ n.fastFib = fib n

Tactic:
by rw [fastFib, fastFibAux_eq]

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

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

Tactic:
by
  dsimp [join]; rw [destruct_cons]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))

Tactic:
rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
    simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

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

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
simp only [Nat.add_assoc, Nat.reduceAdd]

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 2)) ≤ ((of v).contsAux (n + 2)).b
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
rw [(toPoly_eq_zero_iff P).mp h0]

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ a 0 = 0 ∧ b 0 = 0 ∧ c 0 = 0 ∧ d 0 = 0
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
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup

Tactic:
rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
J : Type u_4
i : J ≃ I
⊢ OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e

Tactic:
by
  classical
  simp [iff_mul_eq, i.forall_congr_left]

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ |v - (of v).convs n| ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
have not_terminatedAt_n : ¬(of v).TerminatedAt n := by
    simp [terminatedAt_iff_partDen_none, nth_partDen_eq]
  refine (abs_sub_convs_le not_terminatedAt_n).trans ?_
  -- One can show that `0 < (GenContFract.of v).dens n` but it's easier
  -- to consider the case `(GenContFract.of v).dens n = 0`.
  rcases (zero_le_of_den (K := K)).eq_or_lt' with
    ((hB : (GenContFract.of v).dens n = 0) | hB)
  · simp only [hB, mul_zero, zero_mul, div_zero, le_refl]
  · apply one_div_le_one_div_of_le
    · have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
      apply_rules [mul_pos]
    · conv_rhs => rw [mul_comm]
      gcongr
      exact le_of_succ_get?_den nth_partDen_eq

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
obtain ⟨n, hn⟩ := h _ hx'

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
inst✝ : Finite I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
cases nonempty_fintype I
  obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h
    (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _)
  refine ⟨_, h₁.embedding (Fintype.equivFin I).toEmbedding,
    by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩

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
μ : R
k : ℕ∞
x y : { l // ↑l ≤ k }
h : x ≤ y
⊢ (fun x ↦ ↑↑x) x ≤ (fun x ↦ ↑↑x) y

Tactic:
by simpa using h

Goal state after:
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
⊢ (matrix n c.ofMatrix) x y

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' : n
⊢ ∀ (j : n), c.ofMatrix (x i' j) (y i' j)
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
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • single p p 1 * (M * single q p 1) + z - 1 ∈ matrix n I
⊢ ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
have ⟨N, NxMI⟩ := Mmem

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
p q : n
y : R
Mmem : ∃ z, z * y • single p p 1 * (M * single q p 1) + z - 1 ∈ matrix n I
N : Matrix n n R
NxMI : N * y • single p p 1 * (M * single q p 1) + N - 1 ∈ matrix n I
⊢ ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.Algebra.DirectSum.LinearMap

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

Tactic:
exact h.collectedBasis_repr_of_mem_ne b hσ <| hf _ <| Subtype.mem (b i k)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ ?m.254 ≠ ?m.255

Tactic:
by simpa using h

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
⊢ (trace R (Dual R M)) (Dual.transpose f) = (trace R M) f

Tactic:
rw [← comp_apply, trace_transpose]

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:
intros; simp only [map_mul, *]

Goal state after:
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
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
split_ifs with h <;> intro H

Goal state after:
case pos
α : 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
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

case neg
α : 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
h : ¬(x = y ∧ b = !c)
H : (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p