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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ { l //
    l ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
      l ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
          m ≫ (F.interUnionPullbackCone U V).fst = s.fst → m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = l }

Tactic:
use interUnionPullbackConeLift F U V s

Goal state after:
case property
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
    F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
        m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
          m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

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

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

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ g s ⊗ₜ[R] (AlgHom.id R S) 1 = 1 ⊗ₜ[R] s

Tactic:
← TensorProduct.map_tmul,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (TensorProduct.map g (AlgHom.id R S)) (s ⊗ₜ[R] 1) = 1 ⊗ₜ[R] s
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ (freeObj R X).topologicalSpace ≤ TopologicalSpace.induced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun τ

Tactic:
refine sInf_le ⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom),
      continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom), ?_⟩

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) X.str ≤
    TopologicalSpace.induced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun τ
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ Nonempty (Cocone F)

Tactic:
rw [hasCardinalLT_aleph0_iff] at hA

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l✝ : ι → J
p : (i : ι) → k ⟶ l✝ i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
l : J
a : (i : ι) → l✝ i ⟶ l
b : k ⟶ l
h : ∀ (i : ι), p i ≫ a i = b
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
exact ⟨l, b, fun i ↦ by grind⟩

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
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 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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ f₂ (ι₂ k) = ι₃ x

Tactic:
hk,

Goal state after:
case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
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 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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ f₂ (σ (ι₃ x) - f₁ y) = ι₃ x
Module: Mathlib.Algebra.CharP.MixedCharZero

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

Tactic:
rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
⊢ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p
Module: Mathlib.Algebra.CharP.MixedCharZero

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

Tactic:
intro h_char_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ False
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑↑1 = 1

Tactic:
rw [PNat.one_coe, Nat.cast_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(Rat.num 0) /ₚ ↑(Rat.pnatDen 0) = 0

Tactic:
simp [divp]

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:
by
  apply destruct_eq_cons
  simp [h]

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

Goal state before:
pp: α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive' s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'

Tactic:
simp only [motive'] at ih ⊢

Goal state after:
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : s₁ = s₂ ∨ motive s₁ s₂
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ some (s.tail.get k) = some (s.get (k + 1))

Tactic:
get_succ

Goal state after:
α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ some (s.tail.get k) = some (s.tail.get k)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
n : ℕ
⊢ ((pure a).thinkN n).Results a n

Tactic:
have := results_thinkN n (results_pure a)

Goal state after:
α : Type u
a : α
n : ℕ
this : ((pure a).thinkN n).Results a (0 + n)
⊢ ((pure a).thinkN n).Results a n
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:
have := h.len_unique (results_pure _)

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)
this : n + 1 = 0
⊢ pure a' = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
| cons a₁ l₁ ih =>

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)

Tactic:
get_succ

Goal state after:
case succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
apply
    eq_of_bisim fun c₁ c₂ =>
      c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g

Goal state after:
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ IsBisimulation fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g

case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (take (n + 1) s).length = n + 1

Tactic:
rw [take, destruct]

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
⊢ (match (fun a' ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1
Module: Mathlib.Data.Seq.Computation

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

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

Tactic:
· intro c₁ c₂ h
    match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
      induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)

Tactic:
apply memRecOn this _ fun s IH => _

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, (pure a).Results a m → ((pure a).bind f).Results b (n + m)

α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
rw [dens_stable_of_terminated n.le_succ terminatedAt_n,
      nums_stable_of_terminated n.le_succ terminatedAt_n, Finset.prod_range_succ,
      partNum_none_iff_s_none.mpr terminatedAt_n]
    grind

Goal state after:
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
⊢ ⊤ = s.length'

Tactic:
length'_of_not_terminates h'

Goal state after:
case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ ⊤ = ⊤
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
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with
    ⟨ifp_n, seq_nth_eq, _, rfl⟩

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ none = Stream'.Seq.nil.get? n

Tactic:
Stream'.Seq.get?_nil

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ none = none
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m n : ℕ
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h

Goal state after:
case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
intro ε

Goal state after:
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
⊢ ε > 0 → ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt 0
⊢ g.squashGCF 0 = g

Tactic:
change g.s.get? 0 = none at terminatedAt_n

Goal state after:
case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? 0 = none
⊢ g.squashGCF 0 = g
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case zero
q : ℚ
n : ℕ
⊢ ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q 0 = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑0

Tactic:
intro ifp_zero stream_zero_eq
    have : IntFractPair.of q = ifp_zero := by injection stream_zero_eq
    simp [this.symm]

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

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

Tactic:
let B := g.dens n
    let nB := g.dens (n + 1)
    have abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB) :=
      abs_sub_convs_le not_terminatedAt_n
    suffices 1 / (B * nB) < ε from lt_of_le_of_lt abs_v_sub_conv_le this
    -- show that `0 < (B * nB)` and then multiply by `B * nB` to get rid of the division
    have nB_ineq : (fib (n + 2) : K) ≤ nB :=
      succ_nth_fib_le_of_nth_den (Or.inr not_terminatedAt_n)
    have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)
    have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos
    have nB_pos : 0 < nB := nB_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
    have zero_lt_mul_conts : 0 < B * nB := by positivity
    suffices 1 < ε * (B * nB) from (div_lt_iff₀ zero_lt_mul_conts).mpr this
    -- use that `N' ≥ n` was obtained from the archimedean property to show the following
    calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
      _ ≤ ε * (B * nB) := ?_
    -- cancel `ε`
    gcongr
    calc
      (N' : K) ≤ (N : K) := mod_cast le_max_left _ _
      _ ≤ n := mod_cast n_ge_N
      _ ≤ fib n := mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
      _ ≤ fib (n + 1) := mod_cast fib_le_fib_succ
      _ ≤ fib (n + 1) * fib (n + 1) := mod_cast (fib (n + 1)).le_mul_self
      _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; lia
      _ ≤ B * nB := by gcongr

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
⊢ (∀ n > 3,
      ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) +
          if n = 0 then P.d else 0) =
        0) ∧
    ((((if True then P.a else 0) + if 3 = 2 then P.b else 0) + if 3 = 1 then P.c else 0) + if 3 = 0 then P.d else 0) =
        P.a ∧
      ((((if 2 = 3 then P.a else 0) + if True then P.b else 0) + if 2 = 1 then P.c else 0) + if 2 = 0 then P.d else 0) =
          P.b ∧
        ((((if 1 = 3 then P.a else 0) + if 1 = 2 then P.b else 0) + if True then P.c else 0) +
              if 1 = 0 then P.d else 0) =
            P.c ∧
          ((((if 0 = 3 then P.a else 0) + if 0 = 2 then P.b else 0) + if 0 = 1 then P.c else 0) +
              if True then P.d else 0) =
            P.d

Tactic:
grind [zero_add]

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

Goal state before:

Tactic:
g.dens n ≤ b * g.dens n := by
        simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
      _ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ eval x P.toPoly = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
toPoly

Goal state after:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ eval x (C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this : Nonempty { l // ↑l ≤ k }
m n : { i // ↑i ≤ k }
h : m ≤ n
⊢ ((f - μ • 1) ^ ↑m).ker ≤ ((f - μ • 1) ^ ↑n).ker

Tactic:
simpa using (f - μ • 1).iterateKer.monotone h

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ x ∈ ((f - μ • 1) ^ k).ker → ∃ l, ↑l ≤ ↑k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
· intro hx
    exact ⟨k, le_rfl, hx⟩

Goal state after: