mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Tannaka

Goal state before:
pp: R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat))
M : ModuleCat R
x : ↑M
⊢ (AddCommGrpCat.Hom.hom
        ((End.asHom
                ((fun r ↦
                    ObjectProperty.homMk
                      { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) r), naturality := ⋯ })
                  ((fun φ ↦ (ConcreteCategory.hom (φ.hom.app (ModuleCat.of R R))) 1) φ))).hom.app
          M))
      x =
    (AddCommGrpCat.Hom.hom (φ.asHom.hom.app M)) x

Tactic:
have w := CategoryTheory.congr_fun
      (φ.hom.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)

Goal state after:
R : Type u
inst✝ : Ring R
φ : End (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat))
M : ModuleCat R
x : ↑M
w :
  (ConcreteCategory.hom
        ((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.map
            (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M) x)) ≫
          φ.hom.app (ModuleCat.of R ↑M)))
      1 =
    (ConcreteCategory.hom
        (φ.hom.app (ModuleCat.of R R) ≫
          (AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.map
            (ModuleCat.ofHom (LinearMap.toSpanSingleton R (↑M) x))))
      1
⊢ (AddCommGrpCat.Hom.hom
        ((End.asHom
                ((fun r ↦
                    ObjectProperty.homMk
                      { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) r), naturality := ⋯ })
                  ((fun φ ↦ (ConcreteCategory.hom (φ.hom.app (ModuleCat.of R R))) 1) φ))).hom.app
          M))
      x =
    (AddCommGrpCat.Hom.hom (φ.asHom.hom.app M)) x
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map (homOfLE ⋯).op = s.fst ≫ F.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc,
    Category.assoc, ← F.1.map_comp, ← F.1.map_comp]

Goal state after:
case refine_2.single.left.pair.right.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ s.snd ≫ F.obj.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op) = s.fst ≫ F.obj.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ x✝ ∈ ↑(iSup ι)

Tactic:
Opens.coe_iSup,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔
    x✝ ∈
      ⋃ i,
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)
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
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((forget C).map (f.hom.app (op U))))

Tactic:
apply app_bijective_of_stalkFunctor_map_bijective

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
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
⊢ ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
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
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
⊢ IsIso ((Sheaf.forget C X).map f)

Tactic:
suffices ∀ U : (Opens X)ᵒᵖ, IsIso (f.1.app U) by
    exact @NatIso.isIso_of_isIso_app _ _ _ _ F.1 G.1 f.1 this

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
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
⊢ ∀ (U : (Opens ↑X)ᵒᵖ), IsIso (f.hom.app U)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ f = g ↔ f ∘SL inl R M M₂ = g ∘SL inl R M M₂ ∧ f ∘SL inr R M M₂ = g ∘SL inr R M M₂

Tactic:
by
  simp only [← coe_inj, LinearMap.prod_ext_iff]
  rfl

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

Goal state before:
pp: case property.refine_3.pair.left.e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫ F.obj.map (homOfLE ⋯).op =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫ F.obj.map (homOfLE ⋯).op

Tactic:
simp_rw [Category.assoc, ← F.1.map_comp]

Goal state after:
case property.refine_3.pair.left.e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3.pair.right.e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ (m ≫ F.obj.map (eqToHom ⋯).op) ≫ F.obj.map (homOfLE ⋯).op =
    (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫ F.obj.map (homOfLE ⋯).op

Tactic:
simp_rw [Category.assoc, ← F.1.map_comp]

Goal state after:
case property.refine_3.pair.right.e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ (toSpanSingleton R₁ (c 1)) 1 = c 1

Tactic:
simp [← ContinuousLinearMap.map_smul_of_tower]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
suffices ∀ x y, S.g y = 0 → D₂.p y = D₂.p x → S.g x = 0 by
        simpa [Set.subset_def, D₁, kerι_apply S.g] using this

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ∀ (x y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : MonCat
x✝² : X'✝ ⟶ X✝
x✝¹ : X✝ ⟶ (forget MonCat).obj Y✝
x✝ : X'✝
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm (x✝² ≫ x✝¹)))
      (FreeMonoid.of x✝) =
    (ConcreteCategory.hom
        (free.map x✝² ≫ (ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm x✝¹))
      (FreeMonoid.of x✝)

Tactic:
by rfl

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

Goal state before:
pp: R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsEmbedding ((fun f ↦ ⇑(Hom.hom f)) ∘ fun x ↦ f ≫ x)

Tactic:
suffices IsEmbedding ((· ∘ f.hom) : (B → R) → (A → R)) from
    this.comp (.induced (fun f g e ↦ by ext a; exact congr($e a)))

Goal state after:
R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsEmbedding fun x ↦ x ∘ ⇑(Hom.hom f)
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
⊢ (MorphismProperty.structuredArrowObj L P).limitsOfShape J Y ≤ MorphismProperty.structuredArrowObj L P Y

Tactic:
intro ⟨d⟩
    let hd : IsLimit ((CategoryTheory.StructuredArrow.proj X L ⋙ L).mapCone d.cone) :=
      isLimitOfPreserves _ d.isLimit
    have heq : Y.hom = hd.lift { pt := X, π := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [IsLimit.fac]
      simp
    rw [P.structuredArrowObj_iff, heq, ← (hc _).lift_comp_conePointUniqueUpToIso_hom hd,
      P.cancel_right_of_respectsIso]
    exact H _ _ d.prop_diag_obj

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.IsClosedUnderLimitsOfShape WalkingParallelPair

Tactic:
refine ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
have hch := CharP.cast_eq_zero R (ringChar R)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
        Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

Tactic:
apply pushout.hom_ext

Goal state after:
case h₀
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

case h₁
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ ((map Q hPf ⋙ pushout P Q f).map g ≫
        Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

Tactic:
apply pushout.hom_ext

Goal state after:
case h₀
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
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inl ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inl ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

case h₁
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
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inr ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inr ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n

Tactic:
replace h := congr_arg (fun a ↦ a.get (x.length + n)) h

Goal state after:
α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (x ++ₛ a).get (x.length + n) = (x ++ₛ b).get (x.length + n)
⊢ a.get n = b.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m : ℕ
⊢ List.take m [] = []

Tactic:
List.take_nil

Goal state after:
α : Type u
s : Stream' α
m : ℕ
⊢ [] = []
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ take n xs = take (n + 1 - 1) xs

Tactic:
Nat.add_one_sub_one

Goal state after:
case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ take n xs = take n xs
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case bisim
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
⊢ BisimO (fun c₁ c₂ ↦ c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)) c₁.destruct c₂.destruct

Tactic:
match c₁, c₂, h with
    | _, _, Or.inl ⟨rfl, rfl⟩ =>
      simp only [BisimO, bind, Bind.f, corec_eq, rmap, destruct_pure]
      rcases destruct (f a) with b | cb <;> simp [Bind.g]
    | _, c, Or.inr rfl =>
      simp only [BisimO, Bind.f, corec_eq, rmap]
      rcases destruct c with b | cb <;> simp [Bind.g]

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.TerminatedAt n

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.s.get? n = none

Tactic:
by rfl

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s).get (m + 1) = none
this : ∃ a, a ∈ s.get? n
⊢ False

Tactic:
rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s).get (m + 1) = none
this : ∃ a, a ∈ none
⊢ False