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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ (match { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) =
    F.obj.map (a ≫ g).op

Tactic:
apply map_eq_of_eq K G

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map (Exists.choose ha) = G.map (a ≫ g)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝⁴ : Category.{v_4, u_4} A
inst✝³ : IsDenseSubsite J K G
inst✝² : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
⊢ PreservesFiniteLimits (presheafToSheaf J A ⋙ (G.sheafPushforwardContinuous A J K).inv)

Tactic:
apply comp_preservesFiniteLimits

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝⁴ : Category.{v_4, u_4} A
inst✝³ : IsDenseSubsite J K G
inst✝² : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
this : PreservesFiniteLimits (presheafToSheaf J A ⋙ (G.sheafPushforwardContinuous A J K).inv)
⊢ PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A)

Tactic:
apply comp_preservesFiniteLimits

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
apply +allowSynthFailures createsLimitsOfShapeLeftOp
    exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ Function.Bijective ((fun g ↦ G.op.whiskerLeft f ≫ g) ∘ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map) ↔
    Function.Bijective fun g ↦ f ≫ g

Tactic:
exact Function.Bijective.of_comp_iff'
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.obj R.property)
        (fun g ↦ f ≫ g)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y},
    { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
Equiv.coe_fn_mk

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y}, functorPushforward (Over.forget X) a ≤ functorPushforward (Over.forget X) b ↔ a ≤ b
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
⊢ ↑s₁ Y = ↑s₂ Y

Tactic:
let X : CostructuredArrow F Y := Classical.arbitrary _

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
⊢ ↑s₁ Y = ↑s₂ Y
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx

Goal state after:
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
V : Opens ↑Y
i : V ⟶ U
hi : S.arrows i
hxV : (ConcreteCategory.hom f) x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))

Tactic:
← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone (coveringOfPresieve Y S.arrows)).op))
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := ⋯
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ gl = t

Tactic:
· symm
    apply gl_uniq
    intro i
    rw [← h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x : M
⊢ (𝓝[≠] x).NeBot

Tactic:
rcases exists_ne (0 : M) with ⟨y, hy⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ (𝓝[≠] x).NeBot
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
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      s.1.topologicalSpace ≤
    instTopologicalSpaceCarrier R (ofCone c).pt

Tactic:
refine le_iInf fun i ↦ ?_

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
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      s.1.topologicalSpace ≤
    TopologicalSpace.induced (⇑(hom (c.π.app i))) (F.obj i).topologicalSpace
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case hf
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ Q ?f

Tactic:
exact Q.pushout_inl _ _ hQf

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
a✝ : R
⊢ z • ⟦a✝⟧ = z • θ ↔ ∃ k, ⟦a✝⟧ = θ + ↑(↑k • (p / ↑z))

Tactic:
induction θ using Quotient.inductionOn

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
⊢ corec id id a = const a

Tactic:
by
  rw [corec_def, map_id, iterate_id]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
simpa using h.length_le

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

Goal state before:
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:
rw [IH (results_think_iff.1 h)]
    rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
⊢ C s

Tactic:
by
  haveI T := terminates_of_mem M
  rw [eq_thinkN' s, get_eq_of_mem s M]
  generalize length s = n
  induction n with | zero => exact h1 | succ n IH => exact h2 _ IH

Goal state after:
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
s : Computation α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (s.bind (pure ∘ f)).destruct
    (map f s).destruct

Tactic:
induction s using recOn with
      | pure s => simp
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: case inl.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inl b)

Tactic:
simp only [LiftRelAux]

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

Goal state before:
pp: case inl.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inr cb)

Tactic:
simp only [LiftRelAux]

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

Goal state before:
pp: case inr.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inl b)

Tactic:
simp only [LiftRelAux]

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

Goal state before:
pp: case inr.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inr cb)

Tactic:
simp only [LiftRelAux]

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

Goal state before:
pp: α β : Type u
f : α → β
p : β → Prop
s : Seq α
⊢ (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x

Tactic:
refine ⟨fun _ _ hx ↦ ?_, fun _ _ hx ↦ ?_⟩
  · solve_by_elim [mem_map f hx]
  · obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx
    rw [← hx']
    solve_by_elim

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

Goal state before:
pp: α : 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 : α
hx : x ∈ s.get? i
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
⊢ R x y

Tactic:
rw [← head_dropn] at hx

Goal state after:
α : 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 : α
hx : x ∈ (s.drop i).head
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
⊢ R x y
Module: Mathlib.Data.Seq.Basic

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

Tactic:
rw [← head_dropn] at hx

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

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

Tactic:
induction k generalizing y with

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))

Tactic:
ring_nf

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret nil).join.destruct nil.destruct

Tactic:
simp [ret]

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

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

Tactic:
simp [ret]

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

Goal state before:
pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
simp only [g, a_eq_one, b_eq_z,
            contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]

Goal state after:
case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
⊢ ∃ conts,
    { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast ppred_conts).a,
        b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast ppred_conts).b } =
      Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case zero
q : ℚ
n : ℕ
ifp_zero : IntFractPair ℚ
stream_zero_eq : IntFractPair.stream q 0 = some ifp_zero
this : IntFractPair.of q = ifp_zero
⊢ ifp_zero.fr.num ≤ (IntFractPair.of q).fr.num - ↑0

Tactic:
simp [this.symm]

Goal state after:
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:
· -- arrive at a contradiction since the numerator decreased num + 1 times but every fractional
    -- value is nonnegative.
    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
    have : fract_q_num - n = -1 := by
      have : 0 ≤ fract_q_num := Rat.num_nonneg.mpr (Int.fract_nonneg q)
      simp only [n, Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one,
        sub_add_eq_sub_sub_swap, sub_right_comm, sub_self, zero_sub]
    have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
    have : 0 ≤ ifp.fr.num := Rat.num_nonneg.mpr this
    lia

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✝ : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Tactic:
suffices (⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹ by
    obtain ⟨_, ifp_n_fr⟩ := ifp_n
    have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
    have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
    rwa [← this]
  exact floor_le ifp_n.fr⁻¹

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«0»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0

Tactic:
ring_nf

Goal state after:
case inl.«0»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«1»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1

Tactic:
ring_nf

Goal state after:
case inl.«1»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«2»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2

Tactic:
ring_nf

Goal state after:
case inl.«2»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«3»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3

Tactic:
ring_nf

Goal state after:
case inl.«3»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : R
i j : n
⊢ c.ofMatrix x y ↔ c (single i j x) (single i j y)

Tactic:
refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : R
i j : n
h : c (single i j x) (single i j y)
i' j' : n
⊢ c (single i' j' x) (single i' j' y)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_4
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
⊢ IsIdempotentElem (Option.rec e₀ ((1 - e₀) • e') (some i))

Tactic:
dsimp [IsIdempotentElem]
    linear_combination congr($(he₀.eq) * ((e' i) ^ 2 - k i) + (1 - e₀) * $(hk i))

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalRing R
a : R
⊢ -(e * a) * e = -(e * a * e)

Tactic:
neg_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
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ Commute f₂ f₁

Tactic:
ext; simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]

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
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis (↥s) R M)
⊢ traceAux R ⋯.some = traceAux R b

Tactic:
apply traceAux_eq

Goal state after: