mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ (fun x x_1 h ↦
      ((fun x f x_2 ↦
            Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2))))
          x x_1 h).arrows)
    (pullback p ((E.inter F).toPullback k)) (pullback.fst p ((E.inter F).toPullback k)) ⋯ (pullback.lift f a ⋯)

Tactic:
exact ⟨k.2, a ≫ pullback.snd _ _, by simp [reassoc_of% h₁], by simp [reassoc_of% h₂]⟩

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

Goal state before:
pp: case refine_2.refine_1
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.functorPullback F (Sieve.functorPushforward F T) ≤ T

Tactic:
Sieve.functorPullback_functorPushforward_eq

Goal state after:
case refine_2.refine_1
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ T ≤ T
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id
  simpa using hh i

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
e : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : IsDenseSubsite K J e.inverse
X : Sheaf J A
⊢ (sheafCongr.functor J K e A).map ((sheafCongr.unitIso J K e A).hom.app X) ≫
      (sheafCongr.counitIso J K e A).hom.app ((sheafCongr.functor J K e A).obj X) =
    𝟙 ((sheafCongr.functor J K e A).obj X)

Tactic:
ext
    simp [← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
c : WalkingMulticospan E.multicospanShape
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app c) ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj c) =
    𝟙 ((Hom.mapMulticospan f.hom).obj c)

Tactic:
cases c <;> rw [eqToIso.hom, eqToHom_app, eqToHom_map]

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))

case right
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J
F : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
⊢ PreservesFiniteLimits colim

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v}

Goal state after:
J : Type u₁
K : Type u₂
inst✝¹² : SmallCategory J
inst✝¹¹ : Category.{v₂, u₂} K
inst✝¹⁰ : Small.{v, u₂} K
inst✝⁹ : FinCategory J
F : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
⊢ ∀ (J : Type v) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J colim
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
i₀ : E.I₀
⊢ m ≫ F.obj.map (E.f i₀).op = multiforkLift c ≫ F.obj.map (E.f i₀).op

Tactic:
multiforkLift_map

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
i₀ : E.I₀
⊢ m ≫ F.obj.map (E.f i₀).op = c.ι i₀
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.obj X)

Tactic:
rw [← F.asEquivalence_functor]
  have := F.asEquivalence.counitIso.app (F.asEquivalence.functor.obj X)
  rw [Functor.comp_obj, Functor.id_obj] at this
  have := Simple.of_iso <| Functor.preimageIso _ this
  exact Functor.simple_of_simple_obj F.asEquivalence.inverse _

Goal state after:
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
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
use s

Goal state after:
case h
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
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ (ConcreteCategory.hom (f.hom.app (op U))) s = t
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    1 •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel a =
      Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
        a

Tactic:
rintro ⟨V, b⟩
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ (𝟙 _) (rightToMax _ _) ?_
    dsimp
    simp only [map_one, ← ConcreteCategory.comp_apply, ← Functor.map_comp, one_smul,
      Category.comp_id]

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
r : R
m : A
⊢ (↑φ).toFun (r • m) = (RingHom.id R) r • (↑φ).toFun m

Tactic:
simp [Algebra.smul_def]; 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
i : J
⊢ (F.obj i).topologicalSpace ≤
    TopologicalSpace.induced
      ((ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun ∘ ⇑(hom (c.ι.app i)))
      s.1.topologicalSpace

Tactic:
← 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
i : J
⊢ Continuous
    ((ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun ∘ ⇑(hom (c.ι.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
⊢ s.1.topologicalSpace ≤
    TopologicalSpace.induced
      (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)
      (F.obj i).topologicalSpace

Tactic:
← 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) → 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
    (⇑(hom (c.π.app i)) ∘ (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun)
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)

Tactic:
· simp_all

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

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

Tactic:
CharP.cast_eq_zero_iff R n,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ n ∣ x
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ ↑(tail ⟨some a :: ↑⟨f, al⟩, ⋯⟩) = ↑⟨f, al⟩

Tactic:
dsimp [tail]

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

Goal state before:
pp: case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ (corec' (Corec.f f) (some b)).tail = corec' (Corec.f f) (some b')

Tactic:
Stream'.corec'_eq,

Goal state after:
case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ ((Corec.f f (some b)).fst :: corec' (Corec.f f) (Corec.f f (some b)).snd).tail = corec' (Corec.f f) (some b')
Module: Mathlib.Data.Seq.Computation

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

Tactic:
injection h with h'; rwa [h'] at f0

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (Stream'.corec' (Corec.f f) (Sum.inr b)).tail = Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
Stream'.corec'_eq,

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd)).tail =
    Stream'.corec' (Corec.f f) (Sum.inr b')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ s₁'.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail

Tactic:
rw [h₁]

Goal state after:
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
· simp_all

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

Goal state before:
pp: α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.val.get n)
⊢ (s.val n).isSome = true

Tactic:
dsimp [Stream'.get] at h
      rw [← h]
      exact rfl

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ s.Results a n

Tactic:
injection e with h'

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: (initsCore [s.tail.head] s.tail.tail).get n

Tactic:
cons_get_inits_core

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ (initsCore [s.head, s.tail.head] s.tail.tail).get n = (initsCore [s.head, s.tail.head] s.tail.tail).get n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ map id ⟨s, al⟩ = ⟨s, al⟩

Tactic:
by
    apply Subtype.ext; dsimp [map]
    rw [Option.map_id, Stream'.map_id]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Tactic:
by
  simp [IntFractPair.stream, ite_eq_iff, Option.bind_eq_some_iff]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (IntFractPair.seq1 v).2.get? n = none ↔ IntFractPair.stream v (n + 1) = none

Tactic:
IntFractPair.get?_seq1_eq_succ_get?_stream

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔ IntFractPair.stream v (n + 1) = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop (k + 1)).get? m = s.get? (k + 1 + m)

Tactic:
simp only [drop, get?_tail]
    convert! ih using 2
    lia

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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ IntFractPair.stream (fract v)⁻¹ (n + 1) = none

Tactic:
←
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none,

Goal state after:
case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of (fract v)⁻¹).TerminatedAt n
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
· obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁
    obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
    have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
    rw [← stream_succ h] at hp'₁
    rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]

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

Goal state before:
pp: case succ
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
ih : motive (s.drop m)
⊢ motive (s.drop m).tail

Tactic:
generalize s.drop m = t at *

Goal state after:
case succ
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
t : Seq α
ih : motive t
⊢ motive t.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
⊢ Pairwise R Seq.nil

Tactic:
simp [Pairwise]

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

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

Tactic:
dsimp [join]

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

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)

pp: case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)

Tactic:
· obtain ⟨x, t⟩ := x_1
    cases t <;> simp

Goal state after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ C 0 = 0

Tactic:
C_0

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ 0 = 0