mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
G' : Over X ⥤ Over Y := Over.post G ⋙ Over.map f
this✝ : G'.IsContinuous (K.over X) (J.over Y)
this : G'.IsCocontinuous (K.over X) (J.over Y)
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))

Tactic:
let a : S.over X ⟶
      (G'.sheafPushforwardContinuous RingCat.{u} (K.over X) (J.over Y)).obj (R.over Y) :=
    ((Over.forget X).sheafPushforwardContinuous RingCat.{u} (K.over X) K).map φ

Goal state after:
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
G' : Over X ⥤ Over Y := Over.post G ⋙ Over.map f
this✝ : G'.IsContinuous (K.over X) (J.over Y)
this : G'.IsCocontinuous (K.over X) (J.over Y)
a : S.over X ⟶ (G'.sheafPushforwardContinuous RingCat (K.over X) (J.over Y)).obj (R.over Y) :=
  ((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a },
      { left := { as := PUnit.unit }, right := single i, hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := single i', hom := b }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.singleton _)))

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
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd).left)ᵒᵖ
⊢ (Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.counit)
          (R.over ((D i.fst).X i.snd).left).obj).app
      x✝ =
    ((𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.inverse.op.whiskerLeft
            (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom).app
      x✝

Tactic:
exact R.1.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
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd))ᵒᵖ
⊢ ((𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.functor.op.whiskerLeft (𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
            Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.unit)
              ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app
      x✝ =
    (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app x✝

Tactic:
exact R.1.map_id _

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U : (OpenNhds y)ᵒᵖ
⊢ (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).obj U ⟶
    ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).obj U

Tactic:
exact
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F)
        (op ⟨(unop U).1, (specializes_iff_forall_open.mp h _ (unop U).1.2 (unop U).2 :)⟩)

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 : 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
⊢ s = t

Tactic:
apply F.eq_of_locally_eq' V U i₁

Goal state after:
case hcover
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
⊢ U ≤ iSup V

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
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := ↑φ, map_smul' := ⋯ }
⊢ Continuous ⇑φ

Tactic:
have : ContinuousSMul R B := ⟨(hφ.comp continuous_fst).mul continuous_snd⟩

Goal state after:
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := ↑φ, map_smul' := ⋯ }
this : ContinuousSMul R B
⊢ Continuous ⇑φ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
⊢ IsModuleTopology R (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t))))

Tactic:
have :=
      IsModuleTopology.iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm

Goal state after:
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
this : IsModuleTopology R ((t : Unit) → A (e.symm (Sum.inr t)))
⊢ IsModuleTopology R (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t))))
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

Tactic:
by
  have := ((CategoryTheory.Functor.exact_tfae (uliftFunctor.{v', v} R)).out 1 3).mp
    (uliftFunctor_map_exact R)
  exact this.2

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

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a = Over.homMk Y.hom ⋯ ⋯

Tactic:
by
    ext
    · simp only [mk_left, homMk_hom, Over.homMk_left]
      rw [← Over.w a]
      simp only [mk_left, Functor.const_obj_obj, mk_hom, Category.comp_id]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p ∣ ringChar R ↔ p ∣ Fintype.card R

Tactic:
refine
    ⟨fun h =>
      h.trans <|
        Int.natCast_dvd_natCast.mp <|
          (CharP.intCast_eq_zero_iff R (ringChar R) (Fintype.card R)).mp <|
            mod_cast Nat.cast_card_eq_zero R,
      fun h => ?_⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
⊢ p ∣ ringChar R
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f).eqLocus ((AlgebraTensorModule.lTensor S M) g) =
    ((AlgebraTensorModule.lTensor S M) (f.eqLocus g).subtype).range

Tactic:
rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f - (AlgebraTensorModule.lTensor S M) g).ker =
    ((AlgebraTensorModule.lTensor S M) (f - g).ker.subtype).range
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

Tactic:
by
  constructor
  · intro h q q_prime q_mixedChar
    exact h q (Nat.Prime.pos q_prime) q_mixedChar
  · intro h q q_pos q_mixedChar
    rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
    -- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
    rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
    let r := ringChar (R ⧸ M)
    have r_pos : r ≠ 0 := by
      have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
      simp only [map_natCast, map_zero] at q_zero
      apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
      exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
    have r_prime : Nat.Prime r :=
      or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
    apply h r r_prime
    have : CharZero R := q_mixedChar.toCharZero
    exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ ∀ p > 0, ¬MixedCharZero R p

Tactic:
intro p p_pos
  by_contra hp_mixedChar
  rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩
  replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)
  exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
h_alg' : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
apply of_algebraRat

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

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b ↦ a = b) (s.odd.get n)
⊢ (fun b ↦ a = b) (s.get (2 * n + 1))

Tactic:
rw [h, get_odd]

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

Goal state before:
pp: case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (x ++ₛ a).get (n + m + p) = (List.drop n x ++ₛ a).get (m + p)

Tactic:
← hm,

Goal state after:
case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
hm' : m = (List.drop n x).length
⊢ (x ++ₛ a).get (x.length + p) = (List.drop n x ++ₛ a).get (m + p)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
cases s.destruct with
    | none => simp
    | some v =>
      obtain ⟨x, r⟩ := v
      simpa using ih

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a' b

Tactic:
rw [mem_unique ma' ma]; exact ⟨b, mb, ab⟩

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

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).length h = s.length ⋯

Tactic:
rw [length]
  congr
  ext
  simp

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

Goal state before:
pp: case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.think.destruct ↔ ∃ b, b ∈ cb.think ∧ R a b

Tactic:
rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ Int.fract v + ↑⌊v⌋ = ↑⌊v⌋

Tactic:
by simp [fract_eq_zero]

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

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = conts.a / conts.b

Tactic:
obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
          ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
        IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero

Goal state after:
case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
ifp_n' : IntFractPair K
nth_stream_eq' : IntFractPair.stream v n = some ifp_n'
ifp_n_fract_inv_eq_floor : ifp_n'.fr⁻¹ = ↑⌊ifp_n'.fr⁻¹⌋
⊢ v = conts.a / conts.b
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 : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ?m.64) 1
j : ι
hij : ?m.64 ≤ j
hf : (f' ?m.64 j hij) 1 = 0
⊢ False

Tactic:
(f' i j hij).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 : ι
H : 0 = (Ring.DirectLimit.of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) 1
j : ι
hij : i ≤ j
hf : 1 = 0
⊢ False
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))

Tactic:
simp only [← add_assoc, add_tsub_cancel_right]

Goal state after:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : 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
s' : Seq α
hx : x ∈ s'.head
hy : y ∈ s'.get? (k + 1)
this : motive s'
⊢ R x y

Tactic:
cases s' with
  | nil => simp at hx
  | cons hd tl =>
    simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy
    exact hx ▸ all_get (step hd tl this).left hy

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

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

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | h
  · simp
  replace h := Nat.succ_pred_eq_of_pos h; rw [← h, succ_eq_add_one]
  calc
    gcd (fib m) (fib (n.pred + 1 + m)) =
        gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
        rw [← fib_add n.pred _]
        ring_nf
    _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
        rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
    _ = gcd (fib m) (fib (n.pred + 1)) :=
      Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))

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

Goal state before:
pp: m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
| (fib m).gcd (fib n)

Tactic:
rw [← mod_add_div' n m]

Goal state after:
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
| (fib m).gcd (fib (n % m + n / m * m))