mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
| ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
enter [

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
| ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩

Goal state after:
case refine_2.refine_1
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ (↑t).pi V

case refine_2.refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ ↑(⨆ i, map (LinearMap.single R M i) (s i))
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
by
    -- Since `F` is a sheaf, we can glue all the local preimages together to get a global preimage.
    obtain ⟨s, s_spec, -⟩ := F.existsUnique_gluing' V U iVU V_cover sf this
    · use s
      apply G.eq_of_locally_eq' V U iVU V_cover
      intro x
      rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝¹⁰ : Ring R
inst✝⁹ : Ring S
A : Type u_3
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module R A
inst✝⁶ : TopologicalSpace A
B' : Type u_5
inst✝⁵ : AddCommGroup B'
inst✝⁴ : Module S B'
inst✝³ : TopologicalSpace B'
inst✝² : IsModuleTopology S B'
inst✝¹ : ContinuousAdd A
inst✝ : ContinuousSMul R A
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
⊢ IsOpenMap ⇑φ

Tactic:
have hOpenMap :=
    letI : TopologicalSpace A := moduleTopology R A
    have : IsModuleTopology R A := ⟨rfl⟩
    isOpenQuotientMap_of_surjectiveₛₗ hσ φ hφ |>.isOpenMap
  intro U hU
  exact hOpenMap U <| moduleTopology_le R A U hU

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ ((Shrink.equivalence C).functor.mapArrow.obj ((Shrink.equivalence C).inverse.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
simp; rfl

Goal state after:
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
⊢ Continuous (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun

Tactic:
rw [continuous_iff_le_induced]

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
⊢ instTopologicalSpaceCarrier R (ofCocone c).pt ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun
      s.1.topologicalSpace
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)

Tactic:
have := h ι

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this : IsIso (F.map ι)
⊢ IsIso (F.map φ)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j

Tactic:
let i := IsFiltered.max i₀ j'

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j

Tactic:
rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, assoc]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ Continuous ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun

Tactic:
rw [continuous_iff_le_induced]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat ⋙ free R).obj X).topologicalSpace ≤
    TopologicalSpace.induced ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace
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 → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A✝
f : i ⟶ j
⊢ F.map f ≫ (c₁.ι.app j, c₂.ι.app j) = (c₁.ι.app i, c₂.ι.app i) ≫ ((Functor.const A✝).obj (c₁.pt, c₂.pt)).map f

Tactic:
ext
          · simpa using c₁.w f
          · simpa using c₂.w f

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
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')
x : ↑P
this :
  (ConcreteCategory.hom (π ≫ g)) x =
    (ConcreteCategory.hom
        (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app (((Functor.const (WidePushoutShape ↥s)).obj c'.pt).obj none)))
      x
⊢ (CommRingCat.Hom.hom g) ((ConcreteCategory.hom π) x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) ≫
          c.ι.app c'.pt))
      ((ConcreteCategory.hom π) x)

Tactic:
simpa only [CommRingCat.hom_comp, CommRingCat.hom_ofHom,
        RingHom.liftOfRightInverse_comp_apply, coe_comp, Function.comp_apply] using! this

Goal state after:
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
⊢ PreservesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
refine ⟨fun {K} ↦ ?_⟩

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
⊢ PreservesLimit K (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f)
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ (Ideal.Quotient.mk (Ideal.span {↑↑n})) ↑↑n = 0

Tactic:
Ideal.Quotient.eq_zero_iff_mem

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n ∈ Ideal.span {↑↑n}
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:
Set.mem_range,

Goal state after:
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
⊢ ∃ y, (algebraMap K L) y = x
Module: Mathlib.Algebra.CharZero.Quotient

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

Tactic:
← mul_smul_comm,

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
c : Computation α
n : ℕ
a : α
h : Stream'.cons none c.val n = some a
⊢ Stream'.cons none c.val (n + 1) = some a

Tactic:
by
    rcases n with - | n
    · contradiction
    · exact c.2 h

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

Goal state before:
pp: α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ unfolds g f a = g a :: unfolds g f (f a)

Tactic:
unfold unfolds

Goal state after:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ (of G f (Classical.arbitrary ι)) (-1) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (-1)

Tactic:
simp; rfl

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none

Tactic:
intro h hn
    exact h n hn n le_rfl hn

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

Goal state before:
pp: α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail

Tactic:
rwa [cycle_eq, const_eq]

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

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
exact Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
s : Computation α
⊢ s.bind pure = s

Tactic:
simpa using bind_pure id s

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

Goal state before:
pp: case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g

Tactic:
exact Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_num_eq : g.nums (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
      ∃ conts, g.conts (n + 1) = conts ∧ conts.a = predA :=
    exists_conts_a_of_num succ_nth_num_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]

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

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

Tactic:
rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]

Goal state after:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
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
⊢ R x y

Tactic:
obtain ⟨k, hj⟩ := Nat.exists_eq_add_of_lt h_ij

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

Goal state before:
pp: case pos
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
this : motive (a.drop (a.length ha)) (b.drop (a.length ha))
hb : ¬b.TerminatedAt (a.length ha)
hb_cons : b.drop (a.length ha) ≠ nil
⊢ False

Tactic:
generalize b.drop (a.length ha) = b' at *

Goal state after:
case pos
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b' : Seq β
this : motive (a.drop (a.length ha)) b'
hb_cons : b' ≠ nil
⊢ False
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
⊢ P.toPoly.degree ≤ 1

Tactic:
by
  simpa only [of_b_eq_zero ha hb] using degree_linear_le

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
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
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
suffices v - g.convs n = 0 by simpa [ifp_fr_eq_zero]
    replace g_finite_correctness : v = g.convs n := by
      simpa [GenContFract.compExactValue, ifp_fr_eq_zero] using! g_finite_correctness
    exact sub_eq_zero.2 g_finite_correctness

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.roots.toFinset.card ≤ 3

Tactic:
apply (toFinset_card_le P.toPoly.roots).trans

Goal state after:
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.toPoly.roots.card ≤ 3
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case pos
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

pp: case neg
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3

Tactic:
· simp [hP]

Goal state after:
case neg
R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬P.toPoly = 0
⊢ P.toPoly.roots.card ≤ 3