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
⊢ pushforwardNatTrans φ α.hom ≫
      pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
        (pushforwardCongr ⋯).hom =
    𝟙 (pushforward φ)

Tactic:
ext X U x
    suffices X.val.presheaf.map (α.hom.app U.unop).op ≫
      X.val.presheaf.map (α.inv.app U.unop).op = 𝟙 _ from congr($this x)
    simp only [← Functor.map_comp, ← op_comp,
      Iso.inv_hom_id_app, op_id, CategoryTheory.Functor.map_id]

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible U sf
⊢ ∃! s, F.IsGluing U sf s

Tactic:
simp_rw [isGluing_iff_pairwise]

Goal state after:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
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
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.germ U x hxU)) sU = (ConcreteCategory.hom (F.germ V x hxV)) sV

Tactic:
← F.germ_res iWU x hxW,

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
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.map iWU.op ≫ F.germ W x hxW)) sU = (ConcreteCategory.hom (F.germ V x hxV)) sV
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case hcover
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ U₁ ⊔ U₂ ≤ ⨆ t, if t = true then U₁ else U₂

Tactic:
rw [sup_le_iff]

Goal state after:
case hcover
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (U₁ ≤ ⨆ t, if t = true then U₁ else U₂) ∧ U₂ ≤ ⨆ t, if t = true then U₁ else U₂
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)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
hV : x ∈ V
⊢ ∃ U ≤ V, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
by
  rcases F.exists_germ_eq t with ⟨U, hxU, s, rfl⟩
  refine ⟨U ⊓ V, inf_le_right, by simp [*], F.map (homOfLE inf_le_left).op s, ?_⟩
  exact germ_res_apply ..

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

Goal state before:
pp: case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {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)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
· -- empty case
    infer_instance

Goal state after:
case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {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)
⊢ IsModuleTopology R ((i : Option α✝) → A i)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {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)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
· -- "inductive step" is to check for product over `Option ι` case when known for product over `ι`
    case h_option ι _ hind _ _ _ _ =>
    -- `Option ι` is a `Sum` of `ι` and `Unit`
    let e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
    -- so suffices to check for a product of modules over `ι ⊕ Unit`
    suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from
      .iso (.piCongrLeft R A e.symm)
    -- but such a product is isomorphic to a binary product
    -- of (product over `ι`) and (product over `Unit`)
    suffices IsModuleTopology R
      (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t)))) from
      .iso (ContinuousLinearEquiv.sumPiEquivProdPi R ι Unit _).symm
    -- The product over `ι` has the module topology by the inductive hypothesis,
    -- and the product over `Unit` is just a module which is assumed to have the module topology
    have :=
      IsModuleTopology.iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm
    -- so the result follows from the previous lemma (binary products).
    infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(f x • Finsupp.single x 1)) b = f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
push_cast

Goal state after:
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil (f x • ⇑(Finsupp.single x 1))) b = f x • (bil ⇑(Finsupp.single x 1)) b
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
⊢ φ ≫ cokerπ φ = 0

Tactic:
ext m

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
m : ↑M.toModuleCat
⊢ (ConcreteCategory.hom (φ ≫ cokerπ φ)) m = (ConcreteCategory.hom 0) m
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 b : J.L
⊢ ∀ (x : left a ⟶ left b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩; simp

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 b : J.R
⊢ ∀ (x : right a ⟶ right b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

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 b : J.L
⊢ ∀ (x : left a ⟶ left b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩; simp

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

Goal state before:
pp: case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
⊢ ¬Hom.fst a ≫ eqToHom ⋯ = Hom.snd a ≫ eqToHom ⋯

Tactic:
let f : ((left a : WalkingMultispan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False

Goal state after:
case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ¬Hom.fst a ≫ eqToHom ⋯ = Hom.snd a ≫ eqToHom ⋯
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 b : J.R
⊢ ∀ (x : right a ⟶ right b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩; simp

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

Goal state before:
pp: J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
by
    obtain ⟨j, hj⟩ := h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
        hasCardinalLT_of_hasCardinalLT_arrow hA)
    exact ⟨Cocone.mk j
      { app a := homOfLE (hj a)
        naturality _ _ _ := rfl }⟩

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
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)
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
have h : IsPullback (L.map (pres.π.app .left).left) (L.map (pres.π.app .right).left)
        (L.map (pres.diag.map WalkingCospan.Hom.inl).left)
          (L.map (pres.diag.map WalkingCospan.Hom.inr).left) :=
      IsPullback.of_isLimit_cone <| isLimitOfPreserves
        (CategoryTheory.CostructuredArrow.toOver L X ⋙ CategoryTheory.Over.forget X) pres.isLimit

Goal state after:
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)
⊢ MorphismProperty.costructuredArrowObj L P Y
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
⊢ Under.Hom.right c.inl ≫ Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)) = s.inl

Tactic:
simpa only using! congr($(hc.fac _ _).right)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
⊢ Under.Hom.right c.inr ≫ Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)) = s.inr

Tactic:
simpa only using! congr($(hc.fac _ _).right)

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

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
⊢ ExpChar R 1

Tactic:
have := f.charZero

Goal state after:
case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
this : CharZero R
⊢ ExpChar R 1
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))

Tactic:
exact hPse _ _ hA hB

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ ↑n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ f s = g s

Tactic:
refine eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩

Goal state after:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ IsBisimulation fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : 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✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s.tail.val = s.val.tail

Tactic:
cases s; rfl

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

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u
⊢ nil.TerminatedAt 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.think.val.get n)
⊢ a ∈ s

Tactic:
rcases n with - | n'
    · contradiction
    · exact ⟨n', h⟩

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

Goal state before:
pp: case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rw [e']
      exact Or.inl (mem_cons _ _)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
b : β
s : Seq α
h : b ∈ map f s
⊢ ∃ a ∈ s, f a = b

Tactic:
by match s with
  | ⟨g, al⟩ =>
    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
    rcases o with - | a
    · injection oe
    · injection oe with h'; exact ⟨a, om, h'⟩

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
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ ((g₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
hg₂ i,

Goal state after:
ι : 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
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ ((f'' i j h).comp (g₂ i)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ ↑⌊↑a⌋ + convs'Aux (of ↑a).s (n✝ + 1) = ↑a

Tactic:
floor_intCast,

Goal state after:
case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ ↑a + convs'Aux (of ↑a).s (n✝ + 1) = ↑a
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m

Tactic:
split_ifs with h_if

Goal state after:
case pos
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : m = n
⊢ Option.map f (s.get? n) = Option.map f (s.get? m)

case neg
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : ¬m = n
⊢ s.get? m = s.get? m
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join

Tactic:
cases s <;> simp [map]

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

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
⊢ ε > 0 → ∃ N, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
ε_pos

Goal state after:
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, ∀ n ≥ N, |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

Tactic:
by
  cases s_succ_nth_eq : s.get? (n + 1) with
  | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
  | some =>
    obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq
    simp [*, squashSeq, m_lt_n.ne]

Goal state after: