mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (c.ι.app i ≫ hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)))

Tactic:
hc.fac

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app i))
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s) ≫ c.π.app i))

Tactic:
hc.fac

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app i))
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
e : F✝ ≅ G✝
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsCardinalAccessible κ
inst✝ : G.IsCardinalAccessible κ
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     []
     ":="
     (Term.app `F.preservesColimitsOfShape_of_isCardinalAccessible [`κ]))))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     []
     ":="
     (Term.app `G.preservesColimitsOfShape_of_isCardinalAccessible [`κ]))))
  []
  (Tactic.exact
   "exact"
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x✝ : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x✝ i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
x : ↑R
⊢ (CommRingCat.Hom.hom
        (iP ≫
          CommRingCat.ofHom
            (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x ↦
              (ConcreteCategory.hom (F.map (hi x))) (x✝ x))))
      x =
    (CommRingCat.Hom.hom (α.app i)) x

Tactic:
simp [P, iP]

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

Goal state before:
pp: case inst
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
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
· apply Under.closedUnderColimitsOfShape_pushout

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
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.IsClosedUnderFiniteProducts

Tactic:
refine .of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩

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
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (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
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
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ S)

Tactic:
rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]

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
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R ⋙
      CategoryTheory.Under.pushout f)
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)

Tactic:
rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this✝ :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ S)

Tactic:
rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this✝ :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R ⋙
      CategoryTheory.Under.pushout f)
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
r_dvd_a : ringChar K ∣ a
⊢ False

Tactic:
exact absurd r_dvd_a r_ne_dvd_a

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
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L
x : L
hx : x ∈ ↑S.toSubsemiring
⊢ (↑f x)⁻¹ ∈ (Subalgebra.map f S.toSubalgebra).carrier

Tactic:
exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ corec' (Corec.f f) o (n + 1) = none → corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none →
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (m + n) s

Tactic:
ext; simp [Nat.add_assoc]

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o (n + 1) = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ [] = take 0 s

Tactic:
take_zero

Goal state after:
α : Type u
s : Stream' α
n : ℕ
⊢ [] = []
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs

Tactic:
rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

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

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
⊢ a ∈ s

Tactic:
obtain ⟨a', h⟩ := h
  rw [p h]
  exact h

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.b = b

Tactic:
by
  simpa [partDens, Stream'.Seq.map_get?] using nth_partDen_eq

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab'⟩ := l ma
    rw [mem_unique mb mb']; exact ab'

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (lift G f P g✝ Hg) ((of G f i✝) g) = 0
⊢ (of G f i✝) g = 0

Tactic:
| ih _ g =>

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * Int.fract a = b * a + c

Tactic:
Int.fract

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases s with
    | nil =>
      cases SS with
      | nil => simp
      | cons S SS =>
        obtain ⟨⟨x, s⟩, S⟩ := S
        cases s with
        | nil => simpa using ⟨_, _, rfl, rfl⟩
        | cons x s => simpa using ⟨Seq.cons x (append s (Seq.join S)), SS, by simp, by simp⟩
    | cons _ s => simpa using ⟨s, SS, rfl, rfl⟩

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

Goal state before:
pp: case refl
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num

Tactic:
obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq

Goal state after:
case refl
q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
stream_nth_eq' : IntFractPair.stream q n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
zero_le_ifp_n_fract : 0 ≤ ifp_n.fr
right✝ : ifp_n.fr < 1
⊢ (IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

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

Tactic:
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n :=
      stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq

Goal state after:
case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
⊢ ∃ n, IntFractPair.stream q n = none
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
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.discr = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
simp only [discr, RingHom.map_add, map_sub, map_mul, map_pow, map_ofNat]
  rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
  ring1

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

Goal state before:
pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
have : 0 ≤ pB := (Nat.cast_nonneg _).trans pB_ineq

Goal state after:
case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this : 0 ≤ pB
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
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)
w : W
⊢ ∃ a, T a = w

Tactic:
by
    obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
    exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin (n + 1) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e
i : Fin (n + 1)
this : ∀ (i : Fin (n + 1)), f (e' i) = e i
⊢ (⇑f ∘ (fun x ↦ x.elim (1 - ∑ i, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) i = e i

Tactic:
cases i using Fin.cases with

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
⊢ IsNilpotent μ

Tactic:
by
  obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector
  obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
  exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

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

Tactic:
by simp_rw [mul_zero, zero_mul]

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
⊢ (f.genEigenspace μ₁) ↑↑⟨k, property✝¹⟩ ⊓ (f.genEigenspace μ₂) ↑↑⟨l, property✝⟩ = ⊥

Tactic:
set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
⊢ p = ⊥
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i

Tactic:
simpa only [Submodule.map_iSup] using iSup₂_mono <| fun i _ ↦ hf i

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) f).trace = ((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace

Tactic:
by
        rw [LinearMap.id_comp, LinearMap.comp_id]

Goal state after: