mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₂
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ ∀ x ∈ hf.finset,
    (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))) x =
      (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))) x

Tactic:
intro x

Goal state after:
case h₂
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
x : ↑S
⊢ x ∈ hf.finset →
    (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))) x =
      (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))) x
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: 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))
⊢ Exact ⇑F ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Tactic:
intro x

Goal state after:
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₃
⊢ (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0 ↔ x ∈ Set.range ⇑F
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: 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_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
⊢ Exact ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) ⇑G

Tactic:
intro x

Goal state after:
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_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : C₁
⊢ G x = 0 ↔ x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P Y.hom

Tactic:
rw [show Y.hom = L.map (pres.π.app .left).left ≫ (pres.diag.obj .left).hom by simp]

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom)
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p + ↑k • p * (↑z)⁻¹ = r

Tactic:
conv_rhs => simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, ↑z * (k_1 • p + ↑k • p * (↑z)⁻¹) = ↑z * r
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
h : s.get? 0 = none
⊢ s = nil

Tactic:
ext1 n

Goal state after:
α : Type u
s : Seq α
h : s.get? 0 = none
n : ℕ
⊢ s.get? n = nil.get? n
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s = cons x s.tail

Tactic:
ext1 n

Goal state after:
α : Type u
s : Seq α
x : α
h : s.head = some x
n : ℕ
⊢ s.get? n = (cons x s.tail).get? n
Module: Mathlib.Data.Seq.Defs

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

Tactic:
cases s <;> cases s'

Goal state after:
case nil.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'
⊢ R nil nil → BisimO R nil.destruct nil.destruct → nil.head = nil.head ∧ R nil.tail nil.tail

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

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

case cons.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 α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝¹ s✝¹) (cons x✝ s✝) →
    BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct →
      (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n

Tactic:
refine absurd ?_ H

Goal state after:
case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ s.Terminates
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

Tactic:
exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
have := of_think_terminates h.terminates
  have := results_of_terminates' _ (of_think_mem h.mem)
  exact ⟨_, this, Results.len_unique h (results_think this)⟩

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

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

Tactic:
rw [corec_eq]; rfl

Goal state after:
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:
rw [corec_eq, Stream'.cycle_g_cons, ih a₁]; rfl

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

Goal state before:
pp: α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail

Tactic:
cycle_eq,

Goal state after:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr ([a] ++ₛ cycle [a] ⋯).tail = fr (const a).tail
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
simp [nth_cont_eq_succ_nth_contAux, second_contAux_eq zeroth_s_eq]

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✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C z * Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) X ^ (n + 1) = C z * X ^ (n + 1)

Tactic:
map_X

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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
n : ℕ
z : DirectLimit G fun i j h ↦ ⇑(f' i j h)
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = C z * X ^ n
i : ι
x : G i
h : (of G (fun i j h ↦ ⇑(f' i j h)) i) x = z
⊢ C z * X ^ (n + 1) = C z * X ^ (n + 1)
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
this : Ideal.span ?m.44 ≤ Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥
⊢ ∀
    a ∈
      Ideal.span
        {a |
          (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
            (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
              (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a},
    (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) a = 0

Tactic:
intro x

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
this : Ideal.span ?m.44 ≤ Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥
x : FreeCommRing ((i : ι) × G i)
⊢ x ∈
      Ideal.span
        {a |
          (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
            (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
              (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} →
    (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x = 0
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
⊢ {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} ⊆
    ↑(Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥)

Tactic:
intro x

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
x : FreeCommRing ((i : ι) × G i)
⊢ x ∈
      {a |
        (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
          (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
            (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
              ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} →
    x ∈ ↑(Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
by simp [join]

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

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

Tactic:
by simp [join]

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

Goal state before:
pp: α : 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 β), C ca cb → LiftRel R ca cb

Tactic:
refine memRecOn (C := (fun ca ↦ ∀ (cb : Computation β), C ca cb → LiftRel R ca cb))
    ha ?_ (fun ca' IH => ?_) <;> intro cb Hc

Goal state after:
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
⊢ LiftRel R (pure a) cb

case refine_2
α : 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
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
⊢ LiftRel R ca'.think cb
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

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
⊢ zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun a b ↦ g (f₁ a) (f₂ b)) s₁ s₂

Tactic:
ext1 n

Goal state after:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ (zipWith g (map f₁ s₁) (map f₂ s₂)).get? n = (zipWith (fun a b ↦ g (f₁ a) (f₂ b)) s₁ s₂).get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
⊢ (map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)

Tactic:
ext1 n

Goal state after:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
⊢ (cons hd tl).update 0 f = cons (f hd) tl

Tactic:
ext1 n

Goal state after:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ (cons hd tl).update (n + 1) f = cons hd (tl.update n f)

Tactic:
ext1 n

Goal state after:
α : Type u
hd : α
tl : Seq α
f : α → α
n✝ n : ℕ
⊢ ((cons hd tl).update (n✝ + 1) f).get? n = (cons hd (tl.update n✝ f)).get? n
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).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]
    exact congr_arg (1 / ·) (by rw [convs', of_h_eq_floor, add_right_inj, of_s_tail])

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

Goal state before:
pp: case succ.inl
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
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ v = conts.a / conts.b

Tactic:
rw [← ifp_n_fract_inv_eq_floor] at s_nth_eq

Goal state after:
case succ.inl
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
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_inv_eq_floor : ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
s_nth_eq : g.s.get? n = some { a := 1, b := ifp_n.fr⁻¹ }
⊢ v = conts.a / conts.b
Module: Mathlib.Data.Seq.Basic

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

Tactic:
intro x

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
⊢ x ∈ tl → R hd x