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

Goal state before:
pp: case property.refine_3.single.left
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)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.left }))) =
    F.interUnionPullbackConeLift U V s ≫
      F.obj.map ((eqToHom ⋯).op ≫ (Pairwise.cocone ι).op.π.app (op (Pairwise.single { down := WalkingPair.left })))

Tactic:
convert! h₁
      apply interUnionPullbackConeLift_left

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

Goal state before:
pp: case property.refine_3.pair.left.e_a
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)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)

Tactic:
convert! h₁
      apply interUnionPullbackConeLift_left

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e.toHomeomorph.symm) (TopologicalSpace.induced (⇑e) τ) = τ

Tactic:
rw [induced_compose]

Goal state after:
case h
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_1
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
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul S B'

Tactic:
apply ContinuousSMul.mk
      -- We know that `• : R × A → A` is continuous, by assumption.
      obtain ⟨hA⟩ : ContinuousSMul R A := inferInstance
      /- By linearity of φ, this diagram commutes:
        R × A --(•)--> A
          |            |
          |σ × φ      |φ
          |            |
         \/            \/
        S × B --(•)--> B
      -/
      have hφ2 : (fun p ↦ p.1 • p.2 : S × B' → B') ∘ (Prod.map σ φ) =
        φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) := by ext; simp
      -- Furthermore, `σ` is an open quotient map as is `φ`,
      -- so the product `σ × φ` is an open quotient map, by a result in the library.
      have hoq : IsOpenQuotientMap (_ : R × A → S × B') := IsOpenQuotientMap.prodMap hσ hφo
      -- This is the left map in the diagram. So by a standard fact about open quotient maps,
      -- to prove that the bottom map is continuous, it suffices to prove
      -- that the diagonal map is continuous.
      rw [← hoq.continuous_comp_iff]
      -- but the diagonal is the composite of the continuous maps `φ` and `• : R × A → A`
      rw [hφ2]
      -- so we're done
      exact Continuous.comp hφo.continuous hA

Goal state after:
Module: Mathlib.Algebra.PEmptyInstances

Goal state before:
pp: x x✝ : PEmpty
⊢ PEmpty

Tactic:
by cases x

Goal state after:
Module: Mathlib.Algebra.PEmptyInstances

Goal state before:
pp: x y z : PEmpty
⊢ x * y * z = x * (y * z)

Tactic:
by cases x

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

Goal state before:
pp: S : Type u_1
inst✝⁹ : Semiring S
S₁ : Type u_6
M : Type u_7
M₁ : Type u_8
inst✝⁸ : Semiring S₁
σ : S →+* S₁
σ' : S₁ →+* S
inst✝⁷ : RingHomInvPair σ σ'
inst✝⁶ : RingHomInvPair σ' σ
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module S₁ M₁
f : M ≃ₛₗ[σ] M₁
hf : IsHomeomorph ⇑f
⊢ ⇑(ofIsHomeomorph f hf) = ⇑f

Tactic:
dsimp [ofIsHomeomorph]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
A : C
this : Fact Cardinal.aleph0.IsRegular
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} ((const C).obj A)

Tactic:
exact ⟨Cardinal.aleph0, inferInstance, inferInstance⟩

Goal state after:
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))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
⊢ (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y✝).trans Equiv.ulift.symm)).toIso.hom =
    (Equiv.ulift.trans ((e.toAdjunction.homEquiv X X✝).trans Equiv.ulift.symm)).toIso.hom ≫
      (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f

Tactic:
ext ⟨g⟩

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))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ (ConcreteCategory.hom
          ((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
            (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y✝).trans Equiv.ulift.symm)).toIso.hom)).toFun
      { down := g } =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans ((e.toAdjunction.homEquiv X X✝).trans Equiv.ulift.symm)).toIso.hom ≫
            (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)).toFun
      { down := g }
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
inst✝² : IsCardinalPresentable X κ
inst✝¹ : EssentiallySmall.{w, v_1, u_1} J
inst✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this✝ : PreservesColimitsOfShape J (coyoneda.obj (op X))
this : IsFiltered J
⊢ ∃ j u v, f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
exact exists_eq_of_preservesColimit_coyoneda hc f₁ f₂ hf

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

Goal state before:
pp: R A : CommRingCat
inst✝ : TopologicalSpace ↑R
x✝¹ x✝ : A ⟶ R
e : ⇑(Hom.hom x✝¹) = ⇑(Hom.hom x✝)
⊢ x✝¹ = x✝

Tactic:
by ext; rw [e]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ ((algebraMap R S) (i j) * s) • x = (s • (toSpanSingleton R N x).compLeft ι) i j

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ (s * (algebraMap R S) (i j)) • x = (s • (toSpanSingleton R N x).compLeft ι) i j
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯ ≫ pullback.fst ((map Q hPf).obj A).hom f)

Tactic:
· simpa using Q.of_isIso _

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w') ≫
      (Under.equalizerFork ((R.tensorProd S).map f) ((R.tensorProd S).map g)).ι =
    ((AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
        CategoryTheory.Under.homMk
          (ofHom
            (RingHom.id
              ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                  (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)))))
          ⋯) ≫
      (Under.equalizerFork ((R.tensorProd S).map f) ((R.tensorProd S).map g)).ι

Tactic:
rw [Fork.IsLimit.lift_ι]

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ (Fork.ofι h' w').ι =
    ((AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
        CategoryTheory.Under.homMk
          (ofHom
            (RingHom.id
              ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                  (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)))))
          ⋯) ≫
      (Under.equalizerFork ((R.tensorProd S).map f) ((R.tensorProd S).map g)).ι
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ Q (pushout.inl ((map Q hPf).obj A).hom f ≫ pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯)

Tactic:
· simpa using Q.of_isIso _

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
⊢ IsPrimePow q

Tactic:
have n_pos : n ≠ 0 := fun n_zero =>
      absurd (by simpa [n_zero] using q_eq_rn) (CharP.char_ne_one R q)

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
⊢ x⁻¹ ∈ S

Tactic:
let hS' := hS.toField

Goal state after:
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
⊢ x⁻¹ ∈ S
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ (f x)⁻¹ ∈ S

Tactic:
exact S.inv_mem hx

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ Prod.fst <$> some (a, s) = some a

Tactic:
Option.map_eq_map,

Goal state after:
α : Type u
a : α
s : Seq α
⊢ Option.map Prod.fst (some (a, s)) = some a
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none

Tactic:
intro h
    simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Seq α

Tactic:
by
  refine ⟨Stream'.corec' (Corec.f f) (some b), fun {n} h => ?_⟩
  rw [Stream'.corec'_eq]
  change Stream'.corec' (Corec.f f) (Corec.f f (some b)).2 n = none
  revert h; generalize some b = o
  induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
    rcases o with - | b <;> intro h
    · rfl
    dsimp [Corec.f] at h
    dsimp [Corec.f]
    revert h; rcases h₁ : f b with - | s <;> intro h
    · rfl
    · obtain ⟨a, b'⟩ := s
      contradiction
  | succ n IH =>
    rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

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

Goal state before:
pp: α : Type u
a : α
x✝ : a ∈ nil
w✝ : ℕ
h : some a = none
⊢ False

Tactic:
by injection h

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

Goal state before:
pp: α : Type u
a b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
h✝ : a ∈ cons b ⟨val✝, property✝⟩
h : some a = some b
⊢ a = b

Tactic:
by injection h

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

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

Tactic:
rw [take_succ, List.getElem?_cons_succ, getElem?_take (Nat.lt_of_succ_lt_succ h), get_succ]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a

Tactic:
apply List.take_prefix

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

Goal state before:
pp: case none
α : Type u
n k : ℕ
s : Seq α
h : s.destruct = none
⊢ (match none with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
| none =>

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

Goal state before:
pp: case succ.none
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (match none with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
| none =>

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: case succ.none
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
s_head_eq : s.head = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
| none =>

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: case step
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m✝ : ℕ
n_le_m : n.le m✝
IH : convs'Aux s m✝ = convs'Aux s n
⊢ convs'Aux s m✝.succ = convs'Aux s n

Tactic:
refine (convs'Aux_stable_step_of_terminated (?_)).trans IH

Goal state after:
case step
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m✝ : ℕ
n_le_m : n.le m✝
IH : convs'Aux s m✝ = convs'Aux s n
⊢ s.TerminatedAt m✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = ss → a ∈ s₁ ∨ a ∈ s₂

Tactic:
apply mem_rec_on h _

Goal state after:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
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 β), C (pure a) cb → LiftRel R (pure a) cb

Tactic:
intro cb

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 β
⊢ C (pure a) cb → LiftRel R (pure a) cb
Module: Mathlib.Data.Seq.Computation

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

Tactic:
intro cb

Goal state after:
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 β
⊢ C ca'.think cb → LiftRel R ca'.think cb
Module: Mathlib.Data.Seq.Basic

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

Tactic:
simp [corec_nil]

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))

Tactic:
by
        rw [← fib_add n.pred _]
        ring_nf

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

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

Tactic:
one_mul,

Goal state after:
m n k : ℕ
⊢ (fib m).gcd (fib (n + k * m + m)) = (fib m).gcd (fib (n + k * m))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := ⋯
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ { a := g.h, b := 1 } = Pair.map Rat.cast { a := ↑⌊v⌋, b := 1 }

Tactic:
simp [g]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
| none =>

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
| none =>

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = none
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)

Tactic:
| none =>

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
⊢ ∃ q, v = ↑q

Tactic:
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
⊢ ∃ q, v = ↑q
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.none
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
stream_q_nth_eq : IntFractPair.stream q n = none
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
| none =>

Goal state after:
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
    simp only [squashGCF, terminatedAt_n]

Goal state after: