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
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U)
⊢ X.val.presheaf.map (α.inv.app (Opposite.unop U)).op ≫ X.val.presheaf.map (α.hom.app (Opposite.unop U)).op =
    𝟙 (X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop U))))

Tactic:
simp only [← Functor.map_comp, ← op_comp,
      Iso.hom_inv_id_app, op_id, CategoryTheory.Functor.map_id]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
X✝ Y✝ : SheafOfModules R
e : X✝ ≅ Y✝
⊢ isQuasicoherent R X✝ → isQuasicoherent R Y✝

Tactic:
intro ⟨⟨q⟩⟩
    exact ⟨⟨q.ofIsIso e.hom⟩⟩

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

Goal state before:
pp: 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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
⊢ (ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x) =
    (ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y)

Tactic:
apply section_ext

Goal state after:
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
⊢ ∀ (x_1 : ↑X) (hx : x_1 ∈ V x ⊓ V y),
    (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x)) =
      (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y))
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_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)

Tactic:
have module := ModuleTopology.eq_coinduced_of_surjective <| Submodule.mkQ_surjective S

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_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵
module : moduleTopology R (A ⧸ S) = TopologicalSpace.coinduced (⇑S.mkQ) inferInstance
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
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
s : KernelFork φ
m : s.pt ⟶ (KernelFork.ofι (kerι φ) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (kerι φ) ⋯) = Fork.ι s
⊢ m = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯)

Tactic:
by dsimp at h ⊢; rw [← cancel_mono (kerι φ), h]; rfl

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

Goal state before:
pp: case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] R
⊢ ((↑(Algebra.linearMap T (T ⊗[R] S))).comp (TensorProduct.rid R R T).toAddEquiv.toAddMonoidHom) x✝ =
    ((AddMonoidHom.id (T ⊗[R] S)).comp ↑(LinearMap.lTensor T (Algebra.linearMap R S))) x✝

Tactic:
simp [← Algebra.TensorProduct.linearMap_comp_rid]

Goal state after:
case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] R
⊢ (TensorProduct.rid R R T) x✝ ⊗ₜ[R] 1 = (TensorProduct.AlgebraTensorModule.rid R R T) x✝ ⊗ₜ[R] 1
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) → M ⟶ (X✝ i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (induced c.π.app)).map f ≫ fromInduced c.π.app Y = fromInduced c.π.app X ≫ F.map f

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

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

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
⊢ IsCardinalFiltered J Cardinal.aleph0 → IsFiltered J

pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0

Tactic:
· intro
    exact isFiltered_of_isCardinalFiltered J Cardinal.aleph0

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
⊢ IsFiltered J → IsCardinalFiltered J Cardinal.aleph0
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)
x : ↑B
⊢ (Hom.hom fB) (MvPolynomial.X x) = x

Tactic:
by simp [PB, fB]

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ (iP ≫ π) ≫
      CommRingCat.ofHom
        (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) =
    α.app c'.pt

Tactic:
ext x
    suffices (iP ≫ g' ≫ F.map (c'.ι.app none)) x = α.app c'.pt x by
      simpa [RingHom.liftOfRightInverse_comp_apply] using! this
    rw [← Category.assoc, hg'', ← NatTrans.naturality]
    simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_obj
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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Under Q Z), (map Q ⋯).obj X_1 = (map Q hg ⋙ map Q hf).obj X_1

Tactic:
simp [map, Comma.mapLeft, CategoryTheory.Comma.mapLeft, Comma.lift]

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
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
by
  let c : Fork f g := Under.equalizerFork f g
  let hc : IsLimit c := Under.equalizerForkIsLimit f g
  let ι : R.mkUnder (AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder
  let h' := (R.tensorProd S).map ι
  have w' : h' ≫ (tensorProd R S).map f = h' ≫ (tensorProd R S).map g := by
    simpa using! congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
  let e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') :=
    isLimitMapConeForkEquiv (tensorProd R S) (Under.equalizer_comp f g)
  rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]
  have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
        Under.homMk (CommRingCat.ofHom (.id _)) := by
    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
    rw [Fork.IsLimit.lift_ι]
    ext : 2
    dsimp
    ext x <;> rfl
  rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
    ConcreteCategory.isIso_iff_bijective]
  rfl

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
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
let Q := A →₀ R

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
⊢ Function.Injective ⇑(lTensor A g)
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.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive s

Tactic:
rw [destruct_eq_pure H]

Goal state after:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive (Computation.pure v)
Module: Mathlib.Data.Seq.Computation

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

Tactic:
apply le_antisymm
  · exact Nat.find_min' _ (Nat.find_spec ((terminates_def _).1 h))
  · have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
      Nat.find_spec ((terminates_def _).1 s.think_terminates)
    revert this; rcases length (think s) with - | n <;> intro this
    · simp [think, Stream'.cons] at this
    · apply Nat.succ_le_succ
      apply Nat.find_min'
      apply this

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
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:
by
        intro x hx
        exact (mem_bot P).1 (this hx)

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

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ a ∈ c₁

Tactic:
← ab

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x1 x2 ↦ x1 = x2) b a
⊢ b ∈ c₁
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
stream_zero,

Goal state after:
case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (0 + 1) = some (IntFractPair.of (Int.fract v)⁻¹)
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
  simp only [get?_zipWith, map_get?]
  cases s₁.get? n <;> cases s₂.get? n <;> simp

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
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
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i j : ι
h : i ≤ j
x : G' i
eq1 : (e j) ((f i j h) ((e i).symm x)) = (f' i j h) x
⊢ (e j).symm ((f' i j h) x) = (f i j h) ((e i).symm x)

Tactic:
simp [← eq1]

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

Goal state before:
pp: case cons
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
hd : α
tl : Seq α
this : motive (cons hd tl)
⊢ ∀ (x : α), (cons hd tl).head = some x → p x

Tactic:
| cons hd tl =>

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

Goal state before:
pp: case succ.cons
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α}, (∀ x ∈ s, p x) → x ∈ take m s → p x
hd : α
tl : Seq α
h_all : ∀ x ∈ cons hd tl, p x
hx : x ∈ take (m + 1) (cons hd tl)
⊢ p x

Tactic:
| cons hd tl =>

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ 1

Tactic:
← (Ring.DirectLimit.of _ _ _).map_one

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1

ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ ι
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x y : α
k : ℕ
hj : j = i + k + 1
hd : α
tl : Seq α
hx : x ∈ (Seq.cons hd tl).head
hy : y ∈ (Seq.cons hd tl).get? (k + 1)
this : motive (Seq.cons hd tl)
⊢ R x y

Tactic:
| cons hd tl =>

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

Goal state before:
pp: n : ℕ
ih : fib (n + 1) = ∑ k ∈ Finset.range n, fib k + 1
⊢ fib n + ∑ k ∈ Finset.range n, fib k + 1 = ∑ k ∈ Finset.range (n + 1), fib k + 1

Tactic:
by simp [Finset.range_add_one]

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
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ mapFr Rat.cast (IntFractPair.of q) = IntFractPair.of v

Tactic:
simp [IntFractPair.of, v_eq_q]

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

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

Tactic:
have : v = g.convs n := of_correctness_of_terminatedAt terminatedAt_n

Goal state after:
case inl
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
this : v = g.convs n
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
⊢ gp.a = 1 ∧ ∃ z, gp.b = ↑z

Tactic:
by
  obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
  have : gp = ⟨1, ifp.b⟩ := by
    have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
    have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
    injection this
  simp [this]

Goal state after:
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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr not_terminatedAt_pred_n

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
⊢ x * y = 0 ∧ y * x = 0 ∧ y = 1 - x ↔ IsIdempotentElem x ∧ y = 1 - x

Tactic:
← and_assoc,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
⊢ (x * y = 0 ∧ y * x = 0) ∧ y = 1 - x ↔ IsIdempotentElem x ∧ y = 1 - x
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents fun x ↦ 1 - e x
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {e i}))

Tactic:
by
  obtain ⟨e', rfl, h⟩ : ∃ e' : I → R, (e' = e) ∧ Function.Bijective (RingHom.pi fun i ↦
      Ideal.Quotient.mk (Ideal.span {e' i})) := ⟨_, funext (by simp), he.bijective_pi⟩
  exact h

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalRing R
⊢ ∀ {x : R}, x ∈ (NonUnitalSubsemiring.corner e).carrier → -x ∈ (NonUnitalSubsemiring.corner e).carrier

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
R : Type u_1
e : R
inst✝ : NonUnitalRing R
a : R
⊢ -(fun x ↦ e * x * e) a ∈ (NonUnitalSubsemiring.corner e).carrier