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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀

Tactic:
PreOneHypercover.sieve₁'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (Sieve.ofArrows (E.refineOneHypercover F).Y fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).sieve₀
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ (overEquiv U) (functorPullback (Over.post F) S) = functorPullback F ((overEquiv ((Over.post F).obj U)) S)

Tactic:
refine le_antisymm ?_ ?_
  · dsimp [Sieve.overEquiv]
    rw [Sieve.functorPushforward_le_iff_le_functorPullback, ← Sieve.functorPullback_comp]
    simp_rw [← CategoryTheory.Over.post_forget_eq_forget_comp, Sieve.functorPullback_comp]
    exact Sieve.functorPullback_monotone _ _ (Sieve.le_functorPushforward_pullback _ _)
  · intro Z g hg
    rw [Sieve.overEquiv_iff]
    dsimp [Presieve.functorPullback]
    convert! (Sieve.overEquiv_iff _ _).mp hg
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
⊢ (Over.forget X).PreservesOneHypercovers (J.over X) J

Tactic:
intro Y E

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ E.IsPreservedBy (Over.forget X) J
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
⊢ (Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))

Tactic:
intro Y E

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
⊢ E.IsPreservedBy (Over.post F) (K.over (F.obj X))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (Sieve.overEquiv ((Over.post F).obj Y)) (Sieve.functorPushforward (Over.post F) E.sieve₀) ∈
    K ((Over.post F).obj Y).left

Tactic:
Sieve.functorPushforward_ofArrows,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (Sieve.overEquiv ((Over.post F).obj Y))
      (Sieve.ofArrows (fun i ↦ (Over.post F).obj (E.X i)) fun i ↦ (Over.post F).map (E.f i)) ∈
    K ((Over.post F).obj Y).left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X

Tactic:
rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
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
K' : GrothendieckTopology D'
K'' : GrothendieckTopology D''
G : D ⥤ D'
R' : Sheaf K' RingCat
inst✝³ : G.IsContinuous K K'
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R'
G' : D' ⥤ D''
R'' : Sheaf K'' RingCat
inst✝² : G'.IsContinuous K' K''
inst✝¹ : (G ⋙ G').IsContinuous K K''
inst✝ : (F ⋙ G).IsContinuous J K'
ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R''
⊢ (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫
      pushforwardComp (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ψ' =
    ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
        pushforwardComp φ (ψ ≫ (G.sheafPushforwardContinuous RingCat K K').map ψ')

Tactic:
by ext; rfl

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

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
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

Tactic:
by ext; rfl

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

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
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor

Tactic:
by ext; rfl

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

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

Tactic:
by
  rcases exists_ne (0 : M) with ⟨y, hy⟩
  suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot
  refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)
  · convert! tendsto_const_nhds.add ((@tendsto_id R _).zero_smul_const y)
    rw [add_zero]
  · intro c hc
    simpa [hy] using hc

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff]

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ (∀ (x : M) (x_1 : ι), (f x_1) x = 0 x x_1) ↔ ∀ (i : ι) (x : M), (f i) x = 0 x
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
α✝ β✝ : Type u_2
a✝¹ : α✝ ≃ β✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : β✝ → Type u_3
inst✝³ : (i : β✝) → AddCommMonoid (A i)
inst✝² : (i : β✝) → Module R (A i)
inst✝¹ : (i : β✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : β✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : β✝) → A i)

Tactic:
case of_equiv X Y e _ _ _ _ _ =>
    exact .iso (ContinuousLinearEquiv.piCongrLeft R A e)

Goal state after:
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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
dsimp [coneπApp]

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = (h.isoMap α ⋯).inv ≫ 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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j

Tactic:
dsimp [coneπApp]

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = s.π.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
hF : IsEventuallyConstant F
inst✝ : IsFiltered J
⊢ HasColimit F

Tactic:
obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantFrom
  exact h.hasColimit

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i : J
f g : D.obj i ⟶ X
h : c.π.app i ≫ f = c.π.app i ≫ g
⊢ ∃ j a, D.map a ≫ f = D.map a ≫ g

Tactic:
obtain ⟨j, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (yoneda.obj X) hc.op) f g).mp h

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i : J
f g : D.obj i ⟶ X
h : c.π.app i ≫ f = c.π.app i ≫ g
j : Jᵒᵖ
a : op i ⟶ j
ha : (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map a)) f = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map a)) g
⊢ ∃ j a, D.map a ≫ f = D.map a ≫ g
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
f : of (MvPolynomial ↑A ↑(⊥_ CommRingCat)) ⟶ A := ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
⊢ IsClosedEmbedding fun f ↦ ⇑(Hom.hom f)

Tactic:
have : Function.Surjective f := Function.LeftInverse.surjective (g := .X) fun x ↦ by simp [f]

Goal state after:
R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
f : of (MvPolynomial ↑A ↑(⊥_ CommRingCat)) ⟶ A := ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsClosedEmbedding fun f ↦ ⇑(Hom.hom f)
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Tactic:
obtain ⟨d, hd⟩ : i₂ (σ (ι₃ x)) ∈ range g₁ := by
    rw [← hg.linearMap_ker_eq, mem_ker, show g₂ (i₂ _) = i₃ (f₂ _) from DFunLike.congr_fun h₂ _,
      ← @comp_apply _ _ _ f₂ σ, hσ, id_eq, ← i₃.comp_apply,
      hι₃.linearMap_comp_eq_zero, zero_apply]
  rw [← hd, ← ρ.comp_apply, hρ, id_eq]

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

Goal state before:
pp: case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∀ ⦃s₁ s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = s₁ ∧ ↑s' = s₂ ∧ R s s') → s₁.head = s₂.head ∧ ∃ s s', ↑s = s₁.tail ∧ ↑s' = s₂.tail ∧ R s s'

Tactic:
intro t₁

Goal state after:
case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ : Stream' (Option α)
⊢ ∀ ⦃s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = t₁ ∧ ↑s' = s₂ ∧ R s s') → t₁.head = s₂.head ∧ ∃ s s', ↑s = t₁.tail ∧ ↑s' = s₂.tail ∧ R s s'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∀ ⦃s₁ s₂ : Stream' (Option α)⦄,
    (∃ s s', s.val = s₁ ∧ s'.val = s₂ ∧ R s s') →
      s₁.head = s₂.head ∧ ∃ s s', s.val = s₁.tail ∧ s'.val = s₂.tail ∧ R s s'

Tactic:
intro t₁

Goal state after:
case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ : Stream' (Option α)
⊢ ∀ ⦃s₂ : Stream' (Option α)⦄,
    (∃ s s', s.val = t₁ ∧ s'.val = s₂ ∧ R s s') →
      t₁.head = s₂.head ∧ ∃ s s', s.val = t₁.tail ∧ s'.val = s₂.tail ∧ R s s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
· exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩

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

Goal state before:
pp: 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' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') a'.think.destruct
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
destruct_think

Goal state after:
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' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: 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 r'.think (pure a')
h : BisimO R r'.think.destruct (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
destruct_think

Goal state after:
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 r'.think (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs

Tactic:
take_succ',

Goal state after:
case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ (take n xs ++ [xs.get n]).dropLast = take (n + 1 - 1) xs
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -(g.partNums.get? n).getD 0

Tactic:
partNum_eq_s_a s_nth_eq,

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -(some gp.a).getD 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2

Tactic:
← lift_eq_iff_equiv

Goal state after:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 ↦ x1 = x2) (map f s1) (map f s2)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
rw [length'_of_not_terminates h, length'_of_not_terminates h']

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

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

Tactic:
destruct_think

Goal state after:
case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ b, b ∈ cb.think ∧ R a b
Module: Mathlib.Data.Seq.Computation

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

Tactic:
rcases a with a | ca <;> rcases b with b | cb <;> simp only [LiftRelAux]

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
h : LiftRelAux R C (pure a).destruct cb.destruct
⊢ LiftRel R (pure a) cb

Tactic:
simp only [destruct_pure, LiftRelAux.ret_left] at h
    simp [h]

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
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)
i j : ι
h : i ≤ j
x : G' i
eq1 : ((e j).toRingHom.comp (f i j h)) ((e i).symm x) = ((f' i j h).comp ↑(e i)) ((e i).symm x)
⊢ ((↑(e j).symm).comp (f' i j h)) x = ((f i j h).comp ↑(e i).symm) x

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
        RingEquiv.apply_symm_apply] at eq1 ⊢

Goal state after:
ι : 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)
i j : ι
h : i ≤ j
x : G' i
eq1 : (e j) ((f i j h) ((e i).symm x)) = (f' i j h) x
⊢ (e j).symm ((f' i j h) x) = (f i j h) ((e i).symm x)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right)

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