mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : isCardinalPresentable C κ X
⊢ isCardinalPresentable C κ' X

Tactic:
isCardinalPresentable_iff

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable X κ
⊢ IsCardinalPresentable X κ'
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
X Y : C
e✝ : X ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : isCardinalPresentable C κ X✝
⊢ isCardinalPresentable C κ Y✝

Tactic:
isCardinalPresentable_iff

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
e✝ : X ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X✝ Y✝ : C
e : X✝ ≅ Y✝
hX : IsCardinalPresentable X✝ κ
⊢ IsCardinalPresentable Y✝ κ
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i : J
f g : D.obj i ⟶ X
h : c.π.app i ≫ f = c.π.app i ≫ g
⊢ ∃ j a, D.map a ≫ f = D.map a ≫ g

Tactic:
obtain ⟨j, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (yoneda.obj X) hc.op) f g).mp h
  exact ⟨j.unop, a.unop, ha⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ (uliftCoyoneda.{t, v₁, u₁}.obj (op X)).IsCardinalAccessible κ

Tactic:
by
  change _ ↔ (coyoneda.obj (op X) ⋙ uliftFunctor.{t}).IsCardinalAccessible κ
  refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun J _ _ ↦ ?_⟩⟩
  have := Functor.preservesColimitsOfShape_of_isCardinalAccessible
    (coyoneda.obj (op X) ⋙ uliftFunctor.{t}) κ J
  exact preservesColimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{t, v₁}

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

Goal state before:
pp: case refine_1
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j : ι → J₂
hι : HasCardinalLT ι κ
a : ι → J₁
ha : ∀ (i : ι), Nonempty (j i ⟶ F.obj (a i))
⊢ ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)

Tactic:
exact ⟨F.obj (IsCardinalFiltered.max a hι),
      fun i ↦ ⟨(ha i).some ≫ F.map (toMax a hι i)⟩⟩

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

Goal state before:
pp: 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 π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
H : (ConcreteCategory.hom (g' ≫ c.ι.app i)) ↑r = 0
⊢ ∃ i' hi', (ConcreteCategory.hom (F.map hi')) ((ConcreteCategory.hom g') ↑r) = 0

Tactic:
by
      obtain ⟨k, f, g, e⟩ := this.mp (by simpa using! H)
      exact ⟨k, f, by simpa using! e⟩

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

Goal state before:
pp: case refine_1
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 π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ ker (CommRingCat.Hom.hom π) ≤ ker (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)))

Tactic:
rw [← hs, Ideal.span_le]
    intro r hr
    rw [← c'.w (.init ⟨r, hr⟩)]
    simp [hi'']

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
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom)

Tactic:
apply P.comp_mem _ _ (P.of_isPullback h.flip ?_) (hpres _)

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
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
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan

Tactic:
· exact CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g) =
    ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype).range

Tactic:
by
  rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]
  rw [← map_sub, ker_lTensor_eq]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ (algebraMap K L).fieldRange
⊢ x ∈ Set.range ⇑(algebraMap K L)

Tactic:
rwa [Set.mem_range, ← RingHom.mem_fieldRange]

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

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
injection h with h'
    rw [← h']
    obtain ⟨f, al⟩ := s
    apply Subtype.ext
    dsimp [think, tail]
    rw [← f0]
    exact (Stream'.eta f).symm

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s

Tactic:
rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]

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

Goal state before:
pp: case zero.think
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
⊢ s.think = (pure a).thinkN 0

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

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

Tactic:
· obtain ⟨n, h⟩ := of_results_think h
    cases h
    contradiction

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

case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ ∃ a, s.get? n = some a

Tactic:
← Option.isSome_iff_exists

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ (s.get? n).isSome = true
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
destruct_eq_cons h

Goal state after:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then (cons x r).get? n else none
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partNums.get? n = none

Tactic:
terminatedAt_iff_s_none,

Goal state after:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.s.get? n = none ↔ g.partNums.get? n = none
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partDens.get? n = none

Tactic:
terminatedAt_iff_s_none,

Goal state after:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.s.get? n = none ↔ g.partDens.get? n = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ : Computation β
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) c₂.destruct c₂.destruct

Tactic:
rcases destruct c₂ with b | cb

Goal state after:
case inl
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ : Computation β
b : β
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (Sum.inl b) (Sum.inl b)

case inr
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ cb : Computation β
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (Sum.inr cb) (Sum.inr cb)
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' 0 = g.h

Tactic:
by simp [convs']

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂✝ = s.bind fun x ↦ (f x).bind g
c₂ : Computation γ
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g) c₂.destruct c₂.destruct

Tactic:
rcases destruct c₂ with b | cb

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂✝ = s.bind fun x ↦ (f x).bind g
c₂ : Computation γ
b : γ
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g) (Sum.inl b) (Sum.inl b)

case inr
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂✝ = s.bind fun x ↦ (f x).bind g
c₂ cb : Computation γ
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g) (Sum.inr cb)
    (Sum.inr cb)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]

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

Goal state before:
pp: α : Type u
p : α → Prop
s : Seq α
h : ∀ x ∈ s, p x
n : ℕ
x : α
hx : s.get? n = some x
⊢ p x

Tactic:
exact h _ (get?_mem hx)

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

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

Tactic:
rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
  have : fib n ≤ 2 * fib (n + 1) :=
    le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
  zify [this]
  ring

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

Goal state before:
pp: case succ.some.inr
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 : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
this : (↑fr)⁻¹ = ↑fr⁻¹
coe_of_fr : mapFr Rat.cast (IntFractPair.of fr⁻¹) = IntFractPair.of (↑fr)⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
simpa [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_ne_zero]

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

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : g.TerminatedAt n :=
      terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)
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
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup

Tactic:
have ⟨x, y, z, h3⟩ := (splits_iff_roots_eq_three ha).mp hP
  rw [discr_ne_zero_iff_roots_ne ha h3, h3]
  change _ ↔ (x ::ₘ y ::ₘ {z}).Nodup
  rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
  simp only [nodup_singleton]
  tauto

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
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
let a := e₁ - e₁ * e₂

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₂
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0
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 : M
⊢ x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ ((f - μ • 1) ^ k).ker

Tactic:
rw [mem_genEigenspace]
  constructor
  · rintro ⟨l, hl, hx⟩
    simp only [Nat.cast_le] at hl
    exact (f - μ • 1).iterateKer.monotone hl hx
  · intro hx
    exact ⟨k, le_rfl, hx⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ f.HasUnifEigenvalue μ 1 ↔ ¬IsUnit (f - (algebraMap K (End K V)) μ)

Tactic:
LinearMap.isUnit_iff_ker_eq_bot,

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ f.HasUnifEigenvalue μ 1 ↔ ¬LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥
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
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

Tactic:
use N p p

Goal state after:
case h
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
⊢ N p p * y * M p q + N p p - 1 ∈ I
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst✝³ : Semigroup G₁
inst✝² : Semigroup G₂
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i : ι), DecompositionMonoid (G i)
a b c : (i : ι) → G i
h : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
by
    simp_rw [pi_dvd_iff] at h ⊢
    choose a₁ a₂ h₁ h₂ eq using fun i ↦ DecompositionMonoid.primal _ (h i)
    exact ⟨a₁, a₂, h₁, h₂, funext eq⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
⊢ Field α

Tactic:
by
  let add_group_with_one := e.addGroupWithOne
  let neg := e.Neg
  let inv := e.Inv
  let div := e.div
  let mul := e.mul
  let npow := e.pow ℕ
  let zpow := e.pow ℤ
  let nnratCast := e.nnratCast
  let ratCast := e.ratCast
  let nnqsmul := e.smul ℚ≥0
  let qsmul := e.smul ℚ
  apply e.injective.field _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree + ∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
replace hx := eq_neg_of_add_eq_zero_left hx

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) A (T * S)

Tactic:
left_eq_inter.mpr h

Goal state after:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) (A ∩ fun a ↦ B (f a)) (T * S)
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < comap φ (map φ K) → map φ K = ⊤
hK : comap φ M < K
⊢ K = ⊤

Tactic:
← (comap_injective hφ).eq_iff

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
K : Subgroup G
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
hK : comap φ M < K
⊢ K = ⊤
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : G₀
hx : x ≠ 0
⊢ (snd G₀ H₀) ((inl G₀ H₀) x) = 1

Tactic:
rw [← comp_apply, snd_comp_inl, one_apply_of_ne_zero hx]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Torsion

Goal state before:
pp: case pos
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
h : x ≠ 0 ∧ y ≠ 0
⊢ x = y

pp: case neg
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
h : ¬(x ≠ 0 ∧ y ≠ 0)
⊢ x = y

Tactic:
· exact ih x h.1 y h.2 n hn hxy

Goal state after:
case neg
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsReduced M
ih : ∀ (x : M), x ≠ 0 → ∀ (y : M), y ≠ 0 → ∀ (n : ℕ), n ≠ 0 → x ^ n = y ^ n → x = y
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
h : ¬(x ≠ 0 ∧ y ≠ 0)
⊢ x = y