mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
⊢ Function.Bijective
    (⇑((pushforward φ).obj M).unitHomEquiv ∘
      ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)

Tactic:
convert! (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
⊢ (⇑((pushforward φ).obj M).unitHomEquiv ∘
      ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x) =
    pushforwardSections φ ∘ ⇑M.unitHomEquiv
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
⊢ IsIso (pullbackObjUnitToUnit φ)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]
  intro M
  rw [← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',
    ← (unitHomEquiv _).bijective.of_comp_iff']
  convert! (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective
  ext f : 1
  dsimp
  rw [pushforwardSections_unitHomEquiv, EmbeddingLike.apply_eq_iff_eq,
    Adjunction.homEquiv_naturality_right,
    pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (toPushforwardOfIso H₁ H₂).app U = ℱ.map (eqToHom ⋯) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [toPushforwardOfIso, Adjunction.homEquiv_unit]

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) = U

Tactic:
by
  apply le_antisymm
  · refine iSup_le ?_
    intro f
    exact f.2.1.le
  intro x hxU
  rw [Opens.mem_iSup]
  obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
  exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩

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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
overS : SheafOfModules S ⥤ SheafOfModules (S.over i.fst) := SheafOfModules.pushforward (𝟙 (S.over i.fst))
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation

Tactic:
letI G' := Over.post (X := i.1) G ⋙ Over.map i.2.2

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
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
i : (X : D) × (i : P.I) × (G.obj X ⟶ P.X i)
overS : SheafOfModules S ⥤ SheafOfModules (S.over i.fst) := SheafOfModules.pushforward (𝟙 (S.over i.fst))
G' : Over i.fst ⥤ Over (P.X i.snd.fst) := Over.post G ⋙ Over.map i.snd.snd
⊢ (((SheafOfModules.pushforward φ).obj M).over i.fst).Presentation
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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
⊢ ∃ U, ∃ (m : x ∈ U) (_ : U ∈ B), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
obtain ⟨U, hxU, s, rfl⟩ := F.exists_germ_eq t
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := hB.exists_subset_of_mem_open hxU U.2
  exact ⟨V, hxV, hV, F.map (homOfLE hVU).op s, by rw [← ConcreteCategory.comp_apply, F.germ_res']⟩

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

Goal state before:
pp: case mp
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

pp: case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe

Tactic:
· rintro ⟨f, rfl⟩
    exact ⟨f.continuous, f, rfl⟩

Goal state after:
case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
a : WithOne α
⊢ id a = a

Tactic:
id

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ HasCardinalFilteredColimits C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasCardinalFilteredColimits C ℵ₀
H : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape J C
⊢ ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C

case refine_2
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape J C
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
have iso : coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅
    e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
    NatIso.ofComponents (fun Z ↦
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) (by
        intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit])

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
iso :
  coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅ e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
H : (ConcreteCategory.hom (g' ≫ c.ι.app i)) ↑r = 0
⊢ (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0

Tactic:
simpa using! H

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
h : Function.Injective ⇑f
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x

Tactic:
rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]

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

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ ringChar K = ringChar L

Tactic:
rw [ringChar.eq_iff, Algebra.charP_iff K L]

Goal state after:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : CommSemiring L
inst✝¹ : Nontrivial L
inst✝ : Algebra K L
⊢ CharP L (ringChar L)

Tactic:
apply ringChar.charP

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Module S M
inst✝⁷ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
f✝ g : N →ₗ[R] P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ ↥(lTensor A f).ker ≃ₗ[R] A ⊗[R] ↥f.ker

Tactic:
refine .ofEq _ _ ?_ ≪≫ₗ (LinearEquiv.ofInjective _ (LinearMap.lTensor_injective_of_exact_of_flat
    f hf _ (LinearMap.ker f).subtype_injective (LinearMap.exact_subtype_ker_map _) _)).symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Module S M
inst✝⁷ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
f✝ g : N →ₗ[R] P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ (lTensor A f).ker = (lTensor A f.ker.subtype).range
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
constructor
  · intro g
    rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
    -- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
    rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
    use M
    constructor
    · exact hM_max
    · cases CharP.exists (R ⧸ M) with
      | intro r hr =>
        convert! hr
        have r_dvd_p : r ∣ p := by
          rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
          convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
        symm
        apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
        exact CharP.char_ne_one (R ⧸ M) r
  · intro ⟨I, hI_max, h_charP⟩
    use I
    exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
⊢ corec f b = cons x (corec f s)

Tactic:
apply destruct_eq_cons

Goal state after:
α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
⊢ (corec f b).destruct = some (x, corec f s)
Module: Mathlib.Data.Stream.Init

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

Tactic:
apply Stream'.ext

Goal state after:
α : Type u
a : α
⊢ ∀ (n : ℕ), (const a).get n = (a :: const a).get n
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : some x ∈ ↑s
⊢ ∃ i, some x = s.get? i

Tactic:
Stream'.mem_iff_exists_get_eq

Goal state after:
α : Type u
s : Seq α
x : α
h : ∃ n, some x = (↑s).get n
⊢ ∃ i, some x = s.get? i
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s = cons a s.tail

Tactic:
apply destruct_eq_cons

Goal state after:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s.destruct = some (a, s.tail)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : 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' : Computation α
⊢ R s s' → BisimO R s.destruct s'.destruct → s.head = s'.head ∧ R s.tail s'.tail

Tactic:
refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_

Goal state after:
case refine_1.refine_1
α : 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' : Computation α
r' : α
⊢ ∀ (a : α),
    R (pure r') (pure a) →
      BisimO R (pure r').destruct (pure a).destruct → (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail

case refine_1.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' : Computation α
r' : α
⊢ ∀ (s : Computation α),
    R (pure r') s.think →
      BisimO R (pure r').destruct s.think.destruct → (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail

case refine_2.refine_1
α : 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' : Computation α
⊢ ∀ (a : α),
    R r'.think (pure a) →
      BisimO R r'.think.destruct (pure a).destruct → r'.think.head = (pure a).head ∧ R r'.think.tail (pure a).tail

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' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ s.head :: (take n s.tail ++ [s.tail.get n]) = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
← List.cons_append,

Goal state after:
α : Type u
s : Stream' α
n : ℕ
⊢ s.head :: take n s.tail ++ [s.tail.get n] = take (n + 1) s ++ [s.get (n + 1)]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ s.inits = [s.head] :: map (List.cons s.head) s.tail.inits

Tactic:
apply Stream'.ext

Goal state after:
α : Type u
s : Stream' α
⊢ ∀ (n : ℕ), s.inits.get n = ([s.head] :: map (List.cons s.head) s.tail.inits).get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: ⊢ nats = 0 :: map succ nats

Tactic:
apply Stream'.ext

Goal state after:
⊢ ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : (map f s).Terminates
⊢ (map f s).length' = s.length'

Tactic:
rw [terminates_map_iff] at h'

Goal state after:
case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h h' : ¬(map f s).Terminates
⊢ (map f s).length' = s.length'

Tactic:
rw [terminates_map_iff] at h'

Goal state after:
case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b, b ∈ cb ∧ R a b

Tactic:
by
  induction cb using recOn with
  | pure b =>
    exact
      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
  | think cb =>
    rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩

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:
simp [IntFractPair.stream, ite_eq_iff, Option.bind_eq_some_iff]

Goal state after:
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✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : (ringEquiv G f') ((of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) x) = (ringEquiv G f') 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')

Tactic:
ext1 n
  cases n <;> simp

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
hy : y ∈ (Seq.cons hd tl).get? j
⊢ R x y

Tactic:
cases j with
  | zero => simp at h_ij
  | succ k =>
    simp only [get?_cons_succ] at hy
    cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

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

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

Tactic:
fib_add,

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