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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) a) =
    (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map m.op)) b)

Tactic:
rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ : E.I₀
⊢ ∀ (i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
i₂

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
⊢ ∀ ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ : E.I₀
⊢ ∀ (i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
i₂

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
⊢ ∀ ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mp
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

Tactic:
intro hd U x hx; rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩
    exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
by
  rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]
  apply (Presheaf.isSheaf_iff_isLimit _ _).mp h
  apply presieveOfCovering.mem_grothendieckTopology

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (i₁ i).op)) s = (ConcreteCategory.hom (F.obj.map (i₁ i).op)) t

Tactic:
intro x
    rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ IsModuleTopology R R

Tactic:
apply of_continuous_id

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous id
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case hg
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun rs ↦ rs.1 • rs.2

pp: case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)

Tactic:
· /-
    The map R × R → R is `•`, so by a fundamental property of the module topology,
    this is continuous. -/
    exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..

Goal state after:
case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)
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
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
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ) inst✝³

Tactic:
have hφo : IsOpenQuotientMap φ := AddMonoidHom.isOpenQuotientMap_of_isQuotientMap ⟨⟨rfl⟩, hφ⟩

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
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 ⇑φ
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ) inst✝³
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦ (if h : i ∈ I then LinearMap.proj ⟨i, h⟩ else 0) a

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h✝ : i ∈ I
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦ (LinearMap.proj ⟨i, h✝⟩) a

case neg
R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h✝ : i ∉ I
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦ 0 a
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 only [ofIsHomeomorph]

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 : TopModuleCat R
f : X ⟶ Y
⊢ hom
      ((forget₂ (TopModuleCat R) TopCat ⋙ free R).map f ≫
        ConcreteCategory.ofHom
          { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat) R ↑Y.toModuleCat) id,
            cont := ⋯ }) =
    hom
      (ConcreteCategory.ofHom
          { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id, cont := ⋯ } ≫
        (𝟭 (TopModuleCat R)).map f)

Tactic:
apply ContinuousLinearMap.coe_injective

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
⊢ ↑(hom
        ((forget₂ (TopModuleCat R) TopCat ⋙ free R).map f ≫
          ConcreteCategory.ofHom
            { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat) R ↑Y.toModuleCat) id,
              cont := ⋯ })) =
    ↑(hom
        (ConcreteCategory.ofHom
            { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id,
              cont := ⋯ } ≫
          (𝟭 (TopModuleCat R)).map f))
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

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

Tactic:
apply ContinuousLinearMap.coe_injective

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopCat
⊢ ↑(hom
        ((free R).map
            ({ app := fun X ↦ TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ },
                  naturality := ⋯ }.app
              X) ≫
          {
                app := fun X ↦
                  ConcreteCategory.ofHom
                    { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id,
                      cont := ⋯ },
                naturality := ⋯ }.app
            ((free R).obj X))) =
    ↑(hom (𝟙 ((free R).obj X)))
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 (L.map (pres.diag.map WalkingCospan.Hom.inr).left)

Tactic:
exact P.of_postcomp _ (pres.diag.obj WalkingCospan.one).hom (hpres .one)
      (by simpa using hpres .right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p ↦ p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p ↦ p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom ⋯

Tactic:
ext; simpa using m.w

Goal state after:
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
⊢ Function.Injective toSubalgebra

Tactic:
intro _ _ h

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
⊢ a₁✝ = a₂✝
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
⊢ Function.Injective toSubfield

Tactic:
intro _ _ h

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubfield = a₂✝.toSubfield
⊢ a₁✝ = a₂✝
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'
f : L →ₐ[K] L'
⊢ Function.Injective (map f)

Tactic:
intro _ _ h

Goal state after:
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'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : map f a₁✝ = map f a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Tactic:
h1

Goal state after:
case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
exact False.elim h

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

Goal state before:
pp: case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
exact False.elim h

Goal state after:
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✝ : ℕ
⊢ (pure a).Results a m✝ → ((pure a).bind f).Results b (n + m✝)

Tactic:
h1

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m✝ : ℕ
h1 : (pure a).Results a m✝
⊢ ((pure a).bind f).Results b (n + m✝)
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
s✝ : Computation α
h3 : ∀ {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✝)

Tactic:
h1

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
⊢ (s✝.think.bind f).Results b (n + m✝)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c : Computation α
⊢ (empty α <|> c) = c

Tactic:
apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl
  intro s' s h; rw [← h]
  induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
n : ℕ
h_terminated : s.TerminatedAt n
⊢ (s.set n x).get? n = none

Tactic:
simpa [set, get?_update] using! h_terminated

Goal state after:
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
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a / ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n) =
    1 / (of (fract v)⁻¹).convs' n

Tactic:
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.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:
by
  obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates
  obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convs n = (↑q : K) := exists_rat_eq_nth_conv v n
  have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
  use q, this

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

Goal state before:
pp: case inl
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
· have : squashGCF g n = g := squashGCF_eq_self_of_terminated terminatedAt_n
    simp only [this, convs_stable_of_terminated n.le_succ terminatedAt_n]

Goal state after:
case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ IsIdempotentElem (idempotent V i)

Tactic:
rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ P.roots.toFinset.card ≤ 3

Tactic:
apply (toFinset_card_le P.toPoly.roots).trans
  by_cases hP : P.toPoly = 0
  · simp [hP]
  · exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2 ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
pow_two

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup

Tactic:
rw [discr_ne_zero_iff_roots_ne ha h3, h3]

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ {x, y, z}.Nodup
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : 0 < den'
⊢ 1 / |den'| = 1 / den'

Tactic:
rw [abs_of_pos this]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : (1 - (1 - x ^ n) ^ n) ^ 2 = 1 - (1 - x ^ n) ^ n
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
pow_two

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
this : (1 - (1 - x ^ n) ^ n) * (1 - (1 - x ^ n) ^ n) = 1 - (1 - x ^ n) ^ n
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
⊢ a * e₂ = 0

Tactic:
rw [sub_mul, mul_assoc, he₂.eq, sub_self]

Goal state after: