mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₂
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
x : ↑S
hx : x ∈ hf.finset
⊢ (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))) x =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))) x

Tactic:
rw [← c'.w (.fst (by exact ⟨x, hx⟩)), ← c'.w (.snd (by exact ⟨x, hx⟩))]

Goal state after:
case h₂
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
x : ↑S
hx : x ∈ hf.finset
⊢ (CommRingCat.Hom.hom
        (a ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.fst ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x =
    (CommRingCat.Hom.hom
        (b ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.snd ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ IsFinitelyPresentable S

Tactic:
isFinitelyPresentable_iff_preservesFilteredColimits

Goal state after:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ PreservesFilteredColimits (coyoneda.obj (Opposite.op S))
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ (((Functor.const (WidePullbackShape J)).obj c.pt.left).map f ≫
      Option.casesOn Y c.pt.hom fun j ↦ Hom.left (c.π.app { as := j })) =
    (Option.casesOn X c.pt.hom fun j ↦ Hom.left (c.π.app { as := j })) ≫ (widePullbackDiagramOfDiagramOver B F).map f

Tactic:
dsimp; cases X <;> cases Y <;> cases f
        · rw [Category.id_comp, Category.comp_id]
        · rw [Over.w, Category.id_comp]
        · rw [Category.id_comp, Category.comp_id]

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

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

Tactic:
have hp : p.Prime := Fact.out

Goal state after:
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
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
Module: Mathlib.Algebra.CharZero.AddMonoidHom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : AddCommMonoidWithOne M
inst✝¹ : AddCommMonoidWithOne N
inst✝ : CharZero M
e : M →+ N
he : e 1 = 1
he' : Function.Injective ⇑e
n m : ℕ
h : ↑n = ↑m
⊢ n = m

Tactic:
by
    rwa [← map_natCast' _ he, ← map_natCast' _ he, he'.eq_iff, Nat.cast_inj] at h

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
F E✝ E'✝ : Subfield L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤
      { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E' ↔
    E ≤ E'

Tactic:
simp only [Equiv.coe_fn_mk]

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
F E✝ E'✝ : Subfield L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E✝ E'✝ : IntermediateField K L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤
      { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
        E' ↔
    E ≤ E'

Tactic:
simp only [Equiv.coe_fn_mk]

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E✝ E'✝ : IntermediateField K L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
Module: Mathlib.Algebra.CharP.MixedCharZero

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

Tactic:
intro h_alg
    have h_alg' : Algebra ℚ R := h_alg.some
    apply of_algebraRat

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r

Tactic:
simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
| ∃ k k_1, ↑z * (k_1 • p + ↑k • p * (↑z)⁻¹) = ↑z * r
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case a
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'

Tactic:
exact ⟨s₁, s₂, rfl, rfl, r⟩

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

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
· rintro rfl
    simp [TerminatedAt]

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

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ s₁'.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail

Tactic:
by
      rw [h₁]
      constructor
      · rfl
      · exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩

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

Goal state before:
pp: case a
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', s.val = s₁.val ∧ s'.val = s₂.val ∧ R s s'

Tactic:
exact ⟨s₁, s₂, rfl, rfl, r⟩

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

Goal state before:
pp: α : Type u
a : α
l : List α
s : Stream' α
⊢ drop (a :: l).length (a :: l ++ₛ s) = s

Tactic:
rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
a : α
ha : s.get? m = some a
⊢ ¬s.get? m = none

Tactic:
simp [ha]

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

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

Tactic:
ext k
  simp only [toList, getElem?_take, Nat.lt_find_iff, length,
    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]
  intro h m hmn
  let ⟨a, ha⟩ := ge_stable s hmn h
  simp [ha]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (∏ x ∈ Finset.range n, -(g.partNums.get? x).getD 0) * -(g.partNums.get? n).getD 0

Tactic:
← this,

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -(g.partNums.get? n).getD 0
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
simp [fib, Function.iterate_succ_apply']

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

Goal state before:
pp: case succ.inl.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n' : ℕ
IH : IntFractPair.stream v (n' + 1) = none → v = (of v).convs (n' + 1 - 1)
nth_stream_eq_none✝ : IntFractPair.stream v (n' + 1 + 1) = none
nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none
⊢ v = g.convs (n' + 1)

Tactic:
have : g.TerminatedAt n' :=
          of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.2
            nth_stream_eq_none

Goal state after:
case succ.inl.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n' : ℕ
IH : IntFractPair.stream v (n' + 1) = none → v = (of v).convs (n' + 1 - 1)
nth_stream_eq_none✝ : IntFractPair.stream v (n' + 1 + 1) = none
nth_stream_eq_none : IntFractPair.stream v (n' + 1) = none
this : g.TerminatedAt n'
⊢ v = g.convs (n' + 1)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (n + 1) = ∑ k ∈ Finset.range n, fib k + 1

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]

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

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : s.get? n = some gp_n
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }

Tactic:
by
  simp [*, squashSeq]

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
⊢ g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')

Tactic:
have : g'.s.get? n' = some ⟨pa, pb + a / b⟩ :=
          squashSeq_nth_of_not_terminated s_n'th_eq s_nth_eq

Goal state after:
K : Type u_1
g : GenContFract K
inst✝ : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_eq : ppred_conts = g.contsAux n'
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
pred_conts' : Pair K := g'.contsAux (n' + 1)
succ_n'th_contsAux_eq' : pred_conts' = g'.contsAux (n' + 1)
ppred_conts' : Pair K := g'.contsAux n'
n'th_contsAux_eq' : ppred_conts' = g'.contsAux n'
pA' : K := pred_conts'.a
pB' : K := pred_conts'.b
ppA' : K := ppred_conts'.a
ppB' : K := ppred_conts'.b
this : g'.s.get? n' = some { a := pa, b := pb + a / b }
⊢ g'.convs (n' + 1) = ((pb + a / b) * pA' + pa * ppA') / ((pb + a / b) * pB' + pa * ppB')
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
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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
this : 1 * ↑(fib (n + 1)) ≤ gp.b * pconts.b
⊢ ↑(fib (n + 1)) ≤ gp.b * pconts.b

Tactic:
by rwa [one_mul] at this

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ { a := a, b := b, c := c, d := d }.toPoly.leadingCoeff = a

Tactic:
simp [ha]

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

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

Tactic:
smul_eq_mul,

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

Goal state before:
pp: R : Type u_1
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ { a := a, b := b, c := c, d := d }.toPoly.degree = 3

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ { a := a, b := b, c := c, d := d }.toPoly.natDegree = 3

Tactic:
simp [ha]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

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

Tactic:
by
    classical
    rcases i with - | i <;> rcases j with - | j
    · cases ne rfl
    · simpa only [mul_assoc, Finset.sum_mul, he.mul_eq, Finset.sum_ite_eq', Finset.mem_univ,
        ↓reduceIte, zero_mul] using! congr_arg (· * e j) hx₁
    · simpa only [Option.elim_some, Option.elim_none, ← mul_assoc, Finset.mul_sum, he.mul_eq,
        Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, mul_zero] using! congr_arg (e i * ·) hx₂
    · exact he.ortho (Option.some_inj.ne.mp ne)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1

Tactic:
rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]

Goal state after:
R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ x * y = 0 ∧ x + y = 1 → y * x = 0
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
w : V
⊢ (f ((smulRightₗ v) x)) (T w) = (f ((smulRightₗ v) y)) (T w)

Tactic:
← this,

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
w : V
⊢ T (((smulRightₗ v) x) w) = T (((smulRightₗ v) y) w)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2
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
k : Rᵐᵒᵖ
hk : 1 ^ n - MulOpposite.op (1 - a ^ n) ^ n = (1 - MulOpposite.op (1 - a ^ n)) * k
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
apply_fun MulOpposite.unop at hk

Goal state after:
case inr.refine_2
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
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ (M • N) i j ∈ ↑I.toAddSubmonoid

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ (M * N) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
⊢ M • N ∈ I.matrix.carrier

Tactic:
intro i j
    rw [smul_eq_mul, mul_apply]
    apply sum_mem
    intro k _
    apply I.mul_mem_left _ (hN k j)

Goal state after:
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
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
refine ⟨?_, he.1.surjective_pi⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Injective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : M ∈ (matrix n I).jacobson
p q : n
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
replace Mmem := mul_mem_right _ _ (single q p 1) 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
Mmem : M * single q p 1 ∈ (matrix n I).jacobson
⊢ ∀ (y : R), ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx : x ∈ (f.genEigenspace μ) ↑k
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
mem_genEigenspace_nat

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)