mathlib-initiative/mathlib-tactics huggingface dataset:
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
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
⊢ (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) ≫
      (sheafPushforwardContinuousNatTrans α.inv RingCat J K).app S =
    φ

Tactic:
by ext : 3; simp [← Functor.map_comp, ← op_comp]

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

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

Tactic:
Opens.mem_iSup

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
⊢ ∃ i, x ∈ coveringOfPresieve U R i
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ Opens.IsBasis (Set.range B.obj)

Tactic:
Opens.isBasis_iff_nbhd

Goal state after:
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
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✝⁸ : Semiring R
inst✝⁷ : Semiring S
A : Type u_3
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B' : Type u_5
inst✝³ : AddCommMonoid B'
inst✝² : Module S B'
aB' : TopologicalSpace B'
inst✝¹ : ContinuousAdd B'
inst✝ : ContinuousSMul S B'
σ : R →* S
hσ : Continuous ⇑σ
φ : A →ₑ+[σ] B'
⊢ Continuous ⇑φ

Tactic:
rw [eq_moduleTopology R A, continuous_iff_le_induced]
  exact sInf_le <| ⟨continuousSMul_inducedₛₗ φ hσ, continuousAdd_induced φ⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ Continuous (↑(Hom.hom φ)).range.mkQ.toFun

Tactic:
by tauto

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
a✝¹ a✝ : Prequotient F
⊢ descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝¹ * Quot.mk (⇑(colimitSetoid F)) a✝) =
    descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝¹) * descFun F s (Quot.mk (⇑(colimitSetoid F)) a✝)

Tactic:
solve_by_elim

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x) *
      (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y)

Tactic:
solve_by_elim

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
h : IsEffective R S
s : S
x✝ : s ∈ Set.range ⇑(algebraMap R S)
w✝ : R
hr : (algebraMap R S) w✝ = s
⊢ s ∈ ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom)

Tactic:
simp [← hr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ∀ (x : left a ⟶ right b),
    x ∈
      {
        val :=
          (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
            if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0,
        nodup := ⋯ }

Tactic:
rintro ⟨⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ∀ (x : left a ⟶ right b),
    x ∈
      {
        val :=
          (if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
            if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0,
        nodup := ⋯ }

Tactic:
rintro ⟨⟩ <;> simp

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → (X✝ i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ toCoinduced c.ι.app Y = toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f

Tactic:
by ext x; exact congr($(c.ι.naturality f).hom x)

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this : TopologicalSpace ↑X := ⊤
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this

Tactic:
exact le_top

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this✝ : TopologicalSpace ↑X := ⊤
this : ContinuousAdd ↑X
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this✝

Tactic:
exact le_top

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace

Tactic:
exact le_top

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace

Tactic:
exact le_top

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.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j

Tactic:
rw [← c.w α, ← c.w β, h.coconeιApp_eq j _ β α, assoc, isoMap_inv_hom_id_assoc]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ { app := fun X ↦ TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ }, naturality := ⋯ }.app
        ((forget₂ (TopModuleCat R) TopCat).obj X) ≫
      (forget₂ (TopModuleCat R) TopCat).map
        ({
              app := fun X ↦
                ConcreteCategory.ofHom
                  { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id,
                    cont := ⋯ },
              naturality := ⋯ }.app
          X) =
    𝟙 ((forget₂ (TopModuleCat R) TopCat).obj X)

Tactic:
ext
    simp [freeObj]

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Function.Surjective ⇑(ConcreteCategory.hom fBC)

Tactic:
rw [← RingHom.range_eq_top, ← top_le_iff,
      ← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _), Subring.closure_le]

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Set.range ⇑(ConcreteCategory.hom (pushout.inl φ ψ)) ∪ Set.range ⇑(ConcreteCategory.hom (pushout.inr φ ψ)) ⊆
    ↑(ConcreteCategory.hom fBC).range
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ IsFinitelyPresentable S

Tactic:
rw [isFinitelyPresentable_iff_preservesFilteredColimits]
  exact preservesFilteredColimits_coyoneda R S hS

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
K : Submodule R Q := π.ker
this :
  Function.Exact
    ⇑(SnakeLemma.δ' (rTensor M K.subtype) (rTensor N K.subtype) (rTensor P K.subtype) (lTensor (↥K) g) (lTensor (↥K) f)
        ⋯ (lTensor Q g) (lTensor Q f) ⋯ ⋯ ⋯ 0 ⋯ (rTensor M π) ⋯ ⋯ ⋯)
    ⇑(lTensor A g)
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
Subsingleton.elim (SnakeLemma.δ' ..) 0

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
K : Submodule R Q := π.ker
this : Function.Exact ⇑0 ⇑(lTensor A g)
⊢ Function.Injective ⇑(lTensor A g)
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: 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
⊢ ↑a_unit.unit⁻¹ * ↑(a * r ^ n) = 0

Tactic:
← q_eq_a_mul_rn,

Goal state after:
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
⊢ ↑a_unit.unit⁻¹ * ↑q = 0
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
⊢ x ∈ lift (restrict h) ↔ x ∈ F

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

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
⊢ x ∈ F

case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)
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, z • k_1 • p + ↑k • p = z • r

Tactic:
← natCast_zsmul,

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 • r
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = k • p

Tactic:
← Int.mul_ediv_add_emod k z

Goal state after:
case mp.refine_2
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = (z * (k / z) + k % z) • p
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
a : α
s' : Seq α
⊢ (fun a' ↦ (a', s.tail)) <$> s.get? 0 = some (a, s') → s = cons a s'

Tactic:
rcases f0 : get? s 0 with - | a'

Goal state after:
case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
⊢ (fun a' ↦ (a', s.tail)) <$> none = some (a, s') → s = cons a s'

case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
⊢ (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s') → s = cons a s'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)

Tactic:
corec_eq

Goal state after:
α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ g a :: corec g f (f a) = g a :: corec g f (f a)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t

Tactic:
corec_eq

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t

Tactic:
corec_eq

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x ↦ x.fst.head) (fun x ↦ (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
corec_eq

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x ↦
            match x with
            | (s₁, snd) => s₁.head)
          (fun x ↦
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)

Tactic:
change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ (corec head (fun s ↦ s.tail.tail) s).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail

Tactic:
corec_eq

Goal state after:
α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s ↦ s.tail.tail) s.tail.tail).tail = corec head (fun s ↦ s.tail.tail) s.tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s) = a₁ :: corec head (fun s ↦ s.tail.tail) s

Tactic:
corec_eq

Goal state after:
α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).head :: corec head (fun s ↦ s.tail.tail) (a₁ :: a₂ :: s).tail.tail =
    a₁ :: corec head (fun s ↦ s.tail.tail) s
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: x : ℕ∞
⊢ ¬⊤ < x

Tactic:
cases x <;> simp

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

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ m = n

Tactic:
have := h1.terminates; have := h2.terminates; rw [← h1.length, h2.length]

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:
corec_eq

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

Goal state before:
pp: α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail

Tactic:
corec_eq

Goal state after:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ corec
      (fun x ↦
        match x with
        | (a, snd) => a)
      (fun p ↦
        match p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)

Tactic:
corec_eq

Goal state after:
α : Type u
l : List α
s : Stream' α
⊢ (match (l, s) with
      | (a, snd) => a) ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (match (l, s) with
        | (l', s') => (l' ++ [s'.head], s'.tail)) =
    l ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inl
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
b : β
⊢ match
    match Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
simp [Bind.g]

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

Goal state before:
pp: case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
simp [Bind.g]

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

Goal state before:
pp: case inl
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
b : β
⊢ match
    match Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
simp [Bind.g]

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

Goal state before:
pp: case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
simp [Bind.g]

Goal state after:
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.nums 1 = gp.b * g.h + gp.a

Tactic:
simp [num_eq_conts_a, first_cont_eq zeroth_s_eq]

Goal state after: