mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, ts] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
simp_rw +instances [OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff]

Goal state after:
α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ (∀ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}, IsOpen[inst✝] (f ⁻¹' s)) ↔
    ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s

Tactic:
exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst✝³] U
U_nonempty : U.Nonempty
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst✝³] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ (U ∩ s).Nonempty
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] A'
⊢ Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)

Tactic:
by
  simp [← dual_rTensor_conj_homEquiv, dual_surjective_iff_injective]

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

Tactic:
have : Nonempty α := Nonempty.map f (by infer_instance)

Goal state after:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
inst✝ : SecondCountableTopology α
t : Set β
f : β → α
a✝ : Nontrivial β
this : Nonempty α
⊢ {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ LaxMonoidal.μ F M M ≫ F.map (β_ M M).hom ≫ F.map μ = LaxMonoidal.μ F M M ≫ F.map μ

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ LaxMonoidal.μ F M M ≫ F.map ((β_ M M).hom ≫ μ) = LaxMonoidal.μ F M M ≫ F.map μ
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ LaxMonoidal.μ F A.X A.X ≫ F.map (β_ A.X A.X).hom ≫ F.map μ = LaxMonoidal.μ F A.X A.X ≫ F.map μ

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ LaxMonoidal.μ F A.X A.X ≫ F.map ((β_ A.X A.X).hom ≫ μ) = LaxMonoidal.μ F A.X A.X ≫ F.map μ
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₁ = (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₂
⊢ ↑m₁ = ↑m₂

pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
· simp_rw [Subtype.mk_eq_mk, natCast_div_mul_eq_nsmul] at h
          refine nsmul_injOn_Iio_addOrderOf ?_ ?_ h <;> rw [addOrderOf_period_div hn]
          exacts [m₁.2.1, m₂.2.1]

Goal state after:
case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map (Functor.LaxMonoidal.μ F X X) ≫
          (forget AddCommGrpCat).map
            (F.map (SemiCartesianMonoidalCategory.fst X X) + F.map (SemiCartesianMonoidalCategory.snd X X))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map
          (Functor.LaxMonoidal.μ F X X ≫
            (F.map (SemiCartesianMonoidalCategory.fst X X) + F.map (SemiCartesianMonoidalCategory.snd X X)))
Module: Mathlib.CategoryTheory.Monoidal.CommGrp_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ LaxMonoidal.μ F A.X A.X ≫ F.map (β_ A.X A.X).hom ≫ F.map μ = LaxMonoidal.μ F A.X A.X ≫ F.map μ

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ LaxMonoidal.μ F A.X A.X ≫ F.map ((β_ A.X A.X).hom ≫ μ) = LaxMonoidal.μ F A.X A.X ≫ F.map μ
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
have := CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements
        S.homologyIsCokernel (S.liftCycles x₂ hx₂)
  dsimp at this
  simp [this, ← cancel_mono S.iCycles]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ ↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit) = 𝟙 (𝟙_ (ModuleCat R))

Tactic:
by
    ext
    simp [free]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (ρ_ ((free R).obj X)).hom = (free R).obj X ◁ (εIso R).hom ≫ (μIso R X (𝟙_ (Type u))).hom ≫ (free R).map (ρ_ X).hom

Tactic:
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id]

Goal state after:
R : Type u
inst✝ : CommRing R
X : Type u
⊢ 𝟙 ((free R).obj X) =
    (ρ_ ((free R).obj X)).inv ≫ (free R).obj X ◁ (εIso R).hom ≫ (μIso R X (𝟙_ (Type u))).hom ≫ (free R).map (ρ_ X).hom
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx : (hom r) x₂ = (hom b) x₃
⊢ ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
obtain ⟨x₁, hx₁⟩ :=
    (PullbackCone.IsLimit.equivPullbackObj h.isLimit).surjective ⟨⟨x₂, x₃⟩, hx⟩
  rw [Subtype.ext_iff] at hx₁
  exact ⟨x₁, congr_arg _root_.Prod.fst hx₁,
    congr_arg _root_.Prod.snd hx₁⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.f ≫ (forget₂ C Ab).map S.g)) x = 0

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (S.f ≫ S.g))) x = 0
Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles

Tactic:
by
  simp [S.moduleCatLeftHomologyData.exact_iff_epi_f',
    ModuleCat.epi_iff_surjective, moduleCatLeftHomologyData_K]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.map X.a ≫ T.map (T.ε.app X.A) = 𝟙 (T.obj X.A)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.map (X.a ≫ T.ε.app X.A) = 𝟙 (T.obj X.A)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map ((whiskerRight (L.whiskerLeft h.counit) R).app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X =
    (whiskerRight (L.whiskerLeft h.counit) R).app ((L ⋙ R).obj X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X

Tactic:
by
    dsimp
    rw [← R.map_comp]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (h.unit.app X) ≫ (whiskerRight (L.whiskerLeft h.counit) R).app X = 𝟙 ((L ⋙ R).obj ((𝟭 C).obj X))

Tactic:
by
    dsimp
    rw [← R.map_comp]
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
⊢ I.fstSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π =
    I.sndSigmaMapOfIsColimit d hc ≫ Cofan.IsColimit.desc hd K.π

Tactic:
apply Cofan.IsColimit.hom_ext hc
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A)) ≫ R.map ((reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A) ≫ (reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫ R.map ((coreflector R).map ((coreflectorAdjunction R).counit.app X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ R.map ((coreflector R).map X.a ≫ (coreflector R).map ((coreflectorAdjunction R).counit.app X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)),
    StructuredArrow.mk (𝟙 WalkingReflexivePair.zero) ∈ p →
      (∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂),
          j₁ ∈ p ↔ j₂ ∈ p) →
        ∀ (j : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair), j ∈ p

Tactic:
rintro p h₁ h₂ ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩

Goal state after:
case zero.zero.reflexion
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := zero, hom := reflexion } ∈ p

case zero.one.id
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.zero) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ { left := { as := PUnit.unit }, right := one,
      hom := Hom.id ((Functor.fromPUnit WalkingReflexivePair.zero).obj { as := PUnit.unit }) } ∈
    p
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ Flat R ↑M ↔ PreservesFiniteLimits (tensorLeft M)

Tactic:
rw [Module.Flat.iff_lTensor_preserves_shortComplex_exact,
    ((Functor.exact_tfae <| tensorLeft M).out 1 3 :)]
  simp [show PreservesFiniteColimits (tensorLeft M) from inferInstance]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j ≫ t.desc (newCocone D c))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) = T.forget.map (s.ι.app j) ≫ s.pt.a

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) = T.forget.map (s.ι.app j) ≫ s.pt.a
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ lambda c t ≫ T.map (c.π.app j) ≫ T.δ.app ((D ⋙ T.forget).obj j) =
    lambda c t ≫ T.map (lambda c t) ≫ T.map (T.map (c.π.app j))

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ lambda c t ≫ T.map (c.π.app j) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (lambda c t ≫ T.map (c.π.app j))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (c.π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s) ≫ c.π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
IsPrimary,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ Submodule.IsPrimary I ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ↑(localized' S p f ⊥) = ↑⊥

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_bot p f

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
by simp_rw [and_iff_right bot_le]

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
x y : R'
e : (algebraMap R' S') x = (algebraMap R' S') y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
obtain ⟨x, rfl⟩ := hf x

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
y : R'
x : R
e : (algebraMap R' S') (f x) = (algebraMap R' S') y
⊢ ∃ c, ↑c * f x = ↑c * y
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (algebraMap R S) x✝¹ = (algebraMap R S) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
IsLocalization.eq_iff_exists M

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
x✝¹ x✝ : R
⊢ (∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝