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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
⊢ (pullback C f).map u ≫ (hf.pullbackObjIso 𝒢).hom = (hf.pullbackObjIso ℱ).hom ≫ hf.functor.op.whiskerLeft u

Tactic:
ext U

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
⊢ ((pullback C f).map u ≫ (hf.pullbackObjIso 𝒢).hom).app (op U) =
    ((hf.pullbackObjIso ℱ).hom ≫ hf.functor.op.whiskerLeft u).app (op U)
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible U sf
⊢ ∃! s, F.IsGluing U sf s

Tactic:
by
  simp_rw [isGluing_iff_pairwise]
  exact (Types.isLimit_iff _).mp (h.isSheafPairwiseIntersections U) _ cpt.sectionPairwise.prop

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.QuasicoherentData
X : C
⊢ Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X ∈ J X

Tactic:
refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.QuasicoherentData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
⊢ (Sieve.ofObjects (fun i ↦ q.X (Exists.choose ⋯)) X).arrows hY
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_2
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (eqToHom V_eq_supr_U).op)) ((ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s)

Tactic:
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
      eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_3
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
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map (eqToHom V_eq_supr_U).op)) ((ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t)

Tactic:
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
      eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
W : Opens ↑Y
hW : unop (op ((OpenNhds.inclusion x).obj (unop U))) ≤ (Opens.map f).obj W
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        ((pullback C f).obj F).map (⋯.functor.map i.unop).op ≫ germToPullbackStalk C f F (↑(unop V)) x ⋯ =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        germToPullbackStalk C f F (↑(unop U)) x ⋯ ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
W : Opens ↑Y
hW : unop (op ((OpenNhds.inclusion x).obj (unop U))) ≤ (Opens.map f).obj W
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫
        ((pullback C f).obj F).map (⋯.functor.map i.unop).op ≫ germToPullbackStalk C f F (↑(unop V)) x ⋯ =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map (homOfLE hW).op ≫ germToPullbackStalk C f F (↑(unop U)) x ⋯
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op U) ≫ germToPullbackStalk C f F ((Opens.map f).obj U) x hU =
    F.germ U ((ConcreteCategory.hom f) x) hU ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op U) ≫ germToPullbackStalk C f F ((Opens.map f).obj U) x hU =
    F.germ U ((ConcreteCategory.hom f) x) hU
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
V : Opens ↑X
hV : x ∈ V
V✝ : Opens ↑Y
hV✝ : unop (op V) ≤ (Opens.map f).obj V✝
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op V✝) ≫
      ((pullback C f).obj F).map (homOfLE hV✝).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V✝) ≫
      ((pullback C f).obj F).map (homOfLE hV✝).op ≫
        ((pullback C f).obj F).germ V x hV ≫ 𝟙 (((pullback C f).obj F).stalk x)

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
V : Opens ↑X
hV : x ∈ V
V✝ : Opens ↑Y
hV✝ : unop (op V) ≤ (Opens.map f).obj V✝
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op V✝) ≫
      ((pullback C f).obj F).map (homOfLE hV✝).op ≫ germToPullbackStalk C f F V x hV ≫ stalkPullbackHom C f F x =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V✝) ≫
      ((pullback C f).obj F).map (homOfLE hV✝).op ≫ ((pullback C f).obj F).germ V x hV
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✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : u • x ∈ s
hy' : y ∈ s
⊢ x ∈ s

Tactic:
s.smul_mem_iff' u

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✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
u : Rˣ
hu : x ∈ s
hy' : y ∈ s
⊢ x ∈ s
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(Hom.hom (D₁.π ≫ F ≫ D₂.ι)) = ⇑(Hom.hom (D₁.i ≫ D₂.p))

Tactic:
ShortComplex.π_leftRightHomologyComparison'_ι

Goal state after:
case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(Hom.hom (D₁.i ≫ D₂.p)) = ⇑(Hom.hom (D₁.i ≫ D₂.p))
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : ¬J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + 0).Nodup

pp: case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst b = a
h✝ : J.snd b = a
⊢ (0 + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

pp: case neg
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst b = a
h✝ : ¬J.snd b = a
⊢ (0 + 0).Nodup

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : ¬J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + 0).Nodup

pp: case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : J.snd a = b
⊢ (0 + {Hom.snd a ≫ eqToHom ⋯}).Nodup

pp: case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : ¬J.snd a = b
⊢ (0 + 0).Nodup

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
      if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0).Nodup

Tactic:
split_ifs with h₁ h₂
        · simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMultispan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]
          simp
        all_goals simp

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
intro i j f₁ f₂ e
    obtain ⟨k, hik, hjk, e⟩ := RingHom.EssFiniteType.exists_comp_map_eq_of_isColimit
      R (F ⋙ Under.forget R) { app i := (F.obj i).hom } S.hom ((Under.forget R).mapCocone c)
      (PreservesColimit.preserves hc).some
      (RingHom.FiniteType.of_finitePresentation hS).essFiniteType
      f₁.right (Under.w f₁) f₂.right (Under.w f₂) congr($(e).right)
    exact ⟨k, hik, hjk, Under.UnderMorphism.ext e⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ q ∣ p

Tactic:
by
  refine (CharP.cast_eq_zero_iff A q p).mp ?_
  rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]

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:
exact (Submodule.Quotient.mk_eq_zero I).mpr hx

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

Goal state before:
pp: case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
⊢ R nil (cons x✝ s✝) →
    BisimO R nil.destruct (cons x✝ s✝).destruct → nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail

Tactic:
intro _ this
        rw [destruct_nil, destruct_cons] at this
        exact False.elim this

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

Goal state before:
pp: case cons.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
⊢ R (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

Tactic:
intro _ this
        rw [destruct_nil, destruct_cons] at this
        exact False.elim this

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

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ Stream'.corec' (Corec.f f) (Sum.inr b) 0 = Sum.rec some (fun x ↦ none) (f b)

Tactic:
dsimp [Corec.f, Stream'.corec', Stream'.corec, Stream'.map, Stream'.get, Stream'.iterate]

Goal state after:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match f b with
    | Sum.inl a => some a
    | Sum.inr val => none) =
    Sum.rec some (fun x ↦ none) (f b)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ↑(a :: l) = cons a ↑l

Tactic:
ext1 (_ | n) <;> simp

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

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

Tactic:
| pure a'  => 

Goal state after:
case zero.pure
α : Type u
a a' : α
h : (pure a').Results a 0
⊢ pure a' = (pure a).thinkN 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
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)

Tactic:
| pure a'  => 

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)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ ↦ (empty α <|> c₂) = c₁

Tactic:
intro s' s h

Goal state after:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁

Tactic:
intro s' s h

Goal state after:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b'

Tactic:
by rw [mem_unique mb' mb]; exact ab

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

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

Tactic:
obtain ⟨a, s⟩ := s
        simpa using ⟨s, S, T, rfl, rfl⟩

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
h : fract v ≠ 0
⊢ (of v).s.get? 0 = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
rw [of_s_head_aux, stream_succ_of_some (stream_zero v) h, Option.bind]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some ∘ fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ (have f := fun x ↦
      match x with
      | (acc, x) =>
        match x.destruct with
        | none => none
        | some (x, s) => some (f acc x, f acc x, s);
    cons init (corec f (init, cons x s))) =
    cons init
      (have f_1 := fun x ↦
        match x with
        | (acc, x) =>
          match x.destruct with
          | none => none
          | some (x, s) => some (f acc x, f acc x, s);
      cons (f init x) (corec f_1 (f init x, s)))

Tactic:
dsimp only

Goal state after:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ cons init
      (corec
        (fun x ↦
          match x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (init, cons x s)) =
    cons init
      (cons (f init x)
        (corec
          (fun x ↦
            match x.2.destruct with
            | none => none
            | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
          (f init x, s)))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ (of ↑a).h + convs'Aux (of ↑a).s (n✝ + 1) = ↑a

Tactic:
of_h_eq_floor,

Goal state after:
case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ ↑⌊↑a⌋ + convs'Aux (of ↑a).s (n✝ + 1) = ↑a
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ (of v).h + convs'Aux (of v).s (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
of_h_eq_floor,

Goal state after:
case inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ ↑⌊v⌋ + convs'Aux (of v).s (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ ifp_n = ifp_n'

Tactic:
injection Eq.trans nth_stream_eq.symm nth_stream_eq'

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 : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).h + convs'Aux (of (fract v)⁻¹).s n

Tactic:
of_h_eq_floor,

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = ↑⌊(fract v)⁻¹⌋ + convs'Aux (of (fract v)⁻¹).s n
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
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
⊢ (map (fun x ↦ ↑(e x)) he).comp (map (fun i ↦ ↑(e i).symm) ⋯) = RingHom.id (DirectLimit G' fun x x_1 h ↦ ⇑(f' x x_1 h))

Tactic:
by simp [map_comp]

Goal state after: