mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ (f ∘SL ↑e).IsInvertible → f.IsInvertible

pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible

Tactic:
· rintro ⟨A, hA⟩
    have : f = (f ∘L (e : M₃ →L[R] M)) ∘L e.symm := by ext; simp
    rw [this, ← hA]
    simp

Goal state after:
case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible
Module: Mathlib.Algebra.Category.Ring.EqualizerPushout

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
algebraize [f.hom]
  let fork : Fork (pushoutCocone R S S).inl (pushoutCocone R S S).inr :=
    Fork.ofι (ofHom (algebraMap R S)) (by rw [(PushoutCocone.condition _)])
  let isPushout : IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R S))
      (pushoutCocone R S S).inl (pushoutCocone R S S).inr :=
    ⟨⟨PushoutCocone.condition (pushoutCocone R S S)⟩, ⟨pushoutCoconeIsColimit R S S⟩⟩
  let isLimit : IsLimit fork :=
    (Fork.isLimitEquivOfIsos _
      (equalizerFork (pushoutCocone R S S).inl (pushoutCocone R S S).inr) (Iso.refl _) (Iso.refl _)
      (RingEquiv.toCommRingCatIso <| RingEquiv.ofBijective _
        (Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat R S))
      (by cat_disch) (by cat_disch) (by cat_disch)).symm
    (equalizerForkIsLimit (pushoutCocone R S S).inl (pushoutCocone R S S).inr)
  exact Fork.isLimitEquivOfIsos fork (Fork.ofι f pushout.condition) (Iso.refl _)
    (IsPushout.isoPushout isPushout) (Iso.refl _) (IsPushout.inl_isoPushout_hom isPushout).symm
    (IsPushout.inr_isoPushout_hom isPushout).symm rfl isLimit

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : M →L[R] M
x✝ : M
⊢ x✝¹⁻¹ʳ x✝ = x✝¹.inverse x✝

Tactic:
simp [inverse_eq_ringInverse (ContinuousLinearEquiv.refl R M)]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Tactic:
intro
    constructor
    intro A _ F hA
    rw [hasCardinalLT_aleph0_iff] at hA
    have := ((Arrow.finite_iff A).1 hA).some
    exact ⟨IsFiltered.cocone F⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
obtain ⟨s, hs, H⟩ := hPQ S hS

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case mp
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (∃ y, f ≫ y = x) → ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0

Tactic:
rintro ⟨g, rfl⟩ a ha; simp [ha]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ (i j • s) • x = (s • (toSpanSingleton R N x).compLeft ι) i j

Tactic:
_root_.Algebra.smul_def,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ ((algebraMap R S) (i j) * s) • x = (s • (toSpanSingleton R N x).compLeft ι) i j
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 : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ (Iso.refl
          (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                      map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                    { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                      map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                X).pt.left).hom ≫
      ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).pt.hom =
    (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).pt.hom

Tactic:
simpa using X.fst.w.symm

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ HasPushouts (P.Under ⊤ X)

Tactic:
by
  apply +allowSynthFailures hasColimitsOfShape_of_closedUnderColimitsOfShape
  · exact inferInstanceAs (HasColimitsOfShape WalkingSpan (Under X))
  · apply Under.closedUnderColimitsOfShape_pushout

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

Goal state before:
pp: case tmul.tmul.zero
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
⊢ e₄'.symm (0 • x ⊗ₜ[R] z ⊗ₜ[S] y) = 0 • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
simp only [zero_smul, LinearEquiv.map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0

Tactic:
refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case intro
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
⊢ P

Tactic:
| intro p p_charP =>

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ ∀ (i : ℕ) (h₁ : i < (take n (x ++ₛ a)).length) (h₂ : i < (List.take n x).length),
    (take n (x ++ₛ a))[i] = (List.take n x)[i]

Tactic:
intro _ _ _

Goal state after:
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n

Tactic:
by
  induction n generalizing s with | zero | succ n IH <;>
  induction s using recOn with | pure a' | think s
  · rw [← eq_of_pure_mem h.mem]
    rfl
  · obtain ⟨n, h⟩ := of_results_think h
    cases h
    contradiction
  · have := h.len_unique (results_pure _)
    contradiction
  · rw [IH (results_think_iff.1 h)]
    rfl

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

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (match
      match (cons a s).destruct with
      | none =>
        match t.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', t) 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)) =
    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))
          (s, t))

Tactic:
rw [destruct_cons]

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

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

Tactic:
rw [destruct_cons]

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match some (x✝, s✝) 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),
    some (x✝, s✝) 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.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb

Tactic:
refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_)

Goal state after:
case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C (pure a) cb → LiftRel R (pure a) cb

case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
⊢ ∀ (cb : Computation β), C ca'.think cb → LiftRel R ca'.think cb
Module: Mathlib.Data.Seq.Basic

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

Tactic:
rw [destruct_cons]

Goal state after:
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)) (some (x✝, s✝))
    (some (x✝, s✝))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
x : α
s : Seq α
⊢ ((cons x s).drop (n + 1)).length' = (cons x s).length' - ↑(n + 1)

Tactic:
simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]

Goal state after:
case succ.cons
α : Type u
n : ℕ
x : α
s : Seq α
⊢ (s.drop n).length' = s.length' + 1 - (↑n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
this : motive (Seq.cons hd tl)
hx : hd = x
hy : tl.get? k = some y
⊢ R x y

Tactic:
exact hx ▸ all_get (step hd tl this).left hy

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n

Tactic:
rw [eventually_atTop]
  obtain ⟨n, terminatedAt_n⟩ : ∃ n, (of v).TerminatedAt n := terminates
  use n
  intro m m_geq_n
  rw [convs_stable_of_terminated m_geq_n terminatedAt_n]
  exact of_correctness_of_terminatedAt terminatedAt_n

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

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match (Seq.cons b s).destruct with
    | none => (a, S.join)
    | some s' => (a, (Seq.cons s' S).join)) =
    (a, (Seq.cons (b, s) S).join)

Tactic:
rw [destruct_cons]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ fib (n + 2 + 1) = ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2

Tactic:
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']

Goal state after:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 +
      ∑
        p ∈
          Finset.cons (n + 1, 0)
            (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯,
        p.1.choose p.2 =
    ∑
      p ∈
        Finset.cons (0, n + 2)
          (Finset.cons (n + 2, 0)
            (Finset.map ({ toFun := succ, inj' := succ_injective }.prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯)
          ⋯,
      p.1.choose p.2
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case none
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
stream_nth_eq : IntFractPair.stream q n = none
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
use n, stream_nth_eq

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
by
  rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]

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
i : I
⊢ IsIdempotentElem (idempotent V i)

Tactic:
by
  rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]

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
⊢ b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
by
  obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
  simp [of_partNum_eq_one (partNum_eq_s_a nth_s_eq), zero_le_of_contsAux_b,
    GenContFract.contsAux_recurrence nth_s_eq rfl rfl]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

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

Tactic:
by
  rw [of_b_eq_zero ha hb, degree_linear hc]

Goal state after:
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✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨_, ((equiv (Fintype.equivFin I)).mpr h₁),
    by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ 1 * (1 - e i) + e i * (1 - e j) = 1

Tactic:
by simp [mul_sub, he.ortho hij]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.none.some
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
j : I
h : none ≠ some j
⊢ Option.rec e₀ ((1 - e₀) • e') none * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

pp: case refine_1.some.none
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 : I
h : some i ≠ none
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') none = 0

pp: case refine_1.some.some
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
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

Tactic:
· dsimp; linear_combination - he₀.eq * e' j

Goal state after:
case refine_1.some.none
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 : I
h : some i ≠ none
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') none = 0

case refine_1.some.some
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
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
a b : R
⊢ (fun x ↦ e * x * e) (a + b) = (fun x ↦ e * x * e) a + (fun x ↦ e * x * e) b

Tactic:
by simp_rw [mul_add, add_mul]

Goal state after: