mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_2.pair.right.single.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 ι
down✝ : WalkingPair
g : Pairwise.single { down := WalkingPair.right } ⟶ Pairwise.pair { down := WalkingPair.right } { down := down✝ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn (op (Pairwise.single { down := WalkingPair.right })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map g.op

Tactic:
rcases g with ⟨⟩

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

Goal state before:
pp: case refine_2.pair.right.pair.left
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 ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.left } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.right } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.left } { down := down✝ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝¹ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map g.op

Tactic:
rcases g with ⟨⟩

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

Goal state before:
pp: case refine_2.pair.right.pair.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 ι
down✝¹ down✝ : WalkingPair
g :
  Pairwise.pair { down := WalkingPair.right } { down := down✝ } ⟶
    Pairwise.pair { down := WalkingPair.right } { down := down✝¹ }
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map g.op ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝¹ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map g.op

Tactic:
rcases g with ⟨⟩

Goal state after:
case refine_2.pair.right.pair.right.id_pair
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 ι
down✝ : WalkingPair
⊢ (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map
        (Quiver.Hom.op (Pairwise.Hom.id_pair { down := WalkingPair.right } { down := down✝ })) ≫
      Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
    (Opposite.casesOn (op (Pairwise.pair { down := WalkingPair.right } { down := down✝ })) fun unop ↦
        Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
          ULift.casesOn a fun down ↦
            WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
      ((Pairwise.diagram ι).op ⋙ F.presheaf).map
        (Quiver.Hom.op (Pairwise.Hom.id_pair { down := WalkingPair.right } { down := down✝ }))
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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
V : Opens ↑X
hV : V ∈ B
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ∃ U_1,
    ∃ (m : x ∈ U_1) (_ : U_1 ∈ B),
      ∃ s_1, (ConcreteCategory.hom (F.germ U_1 x m)) s_1 = (ConcreteCategory.hom (F.germ U x hxU)) s

Tactic:
exact ⟨V, hxV, hV, F.map (homOfLE hVU).op s, by rw [← ConcreteCategory.comp_apply, F.germ_res']⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
i : Fin n
x✝ : i ∈ Finset.univ
⊢ Continuous[Pi.topologicalSpace, inst✝⁴] fun a ↦ (a i).1 • (a i).2

Tactic:
exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : PreservesFilteredColimits (forget C)
inst✝³ : HasLimits C
inst✝² : PreservesLimits (forget C)
inst✝¹ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.hom)
x : ↑X
hx : x ∈ U
⊢ IsIso (↾⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom)))

Tactic:
exact Functor.map_isIso (forget C) ((stalkFunctor C (⟨x, hx⟩ : U).1).map f.1)

Goal state after:
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:
simp only [← coe_inj, LinearMap.prod_ext_iff]
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Ring R₁
inst✝⁸ : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(↑f₁).ker
⊢ (f₁.projKerOfRightInverse f₂ h) ↑x = x

Tactic:
ext1
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe

Tactic:
rintro ⟨hfc, f, rfl⟩

Goal state after:
case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hfc : ⇑f ∈ {f | Continuous[inst✝⁵, inst✝³] f}
⊢ ⇑f ∈ Set.range DFunLike.coe
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
x : ULift.{u_1, v} ↑S.X₂
⊢ (Hom.hom S.g) (ULift.moduleEquiv x) = 0 ↔ ∃ y, (Hom.hom S.f) (ULift.moduleEquiv y) = ULift.moduleEquiv x

Tactic:
(CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact S).mp h

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
x : ULift.{u_1, v} ↑S.X₂
⊢ ULift.moduleEquiv x ∈ Set.range ⇑(ConcreteCategory.hom S.f) ↔
    ∃ y, (Hom.hom S.f) (ULift.moduleEquiv y) = ULift.moduleEquiv x
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MulticospanShape
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 b = a
h₂ : J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

pp: case neg
J : MulticospanShape
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 b = a
h₂ : ¬J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + 0).Nodup

pp: case pos
J : MulticospanShape
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 b = a
h✝ : J.snd b = a
⊢ (0 + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

pp: case neg
J : MulticospanShape
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 b = a
h✝ : ¬J.snd b = a
⊢ (0 + 0).Nodup

Tactic:
· simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMulticospan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
          simp

Goal state after:
case neg
J : MulticospanShape
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 b = a
h₂ : ¬J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + 0).Nodup

case pos
J : MulticospanShape
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 b = a
h✝ : J.snd b = a
⊢ (0 + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

case neg
J : MulticospanShape
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 b = a
h✝ : ¬J.snd b = a
⊢ (0 + 0).Nodup
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map (δ ≫ β)

Tactic:
← h₁,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map (γ ≫ minToRight i₀ j)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (β ≫ δ) = F.map (rightToMax i₀ j) ≫ F.map γ

Tactic:
← h₁,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j ≫ γ) =
    F.map (rightToMax i₀ j) ≫ F.map γ
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map (φ ≫ β) ≫ (h.isoMap α ⋯).inv

Tactic:
map_comp,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = (F.map φ ≫ F.map β) ≫ (h.isoMap α ⋯).inv
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M : TopCat
x : ↑(freeObj R M).toModuleCat
⊢ (hom (freeMap R (𝟙 M))) x = (hom (𝟙 (freeObj R M))) x

Tactic:
exact DFunLike.congr_fun (Finsupp.lmapDomain_id _ _) x

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
A : C
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} ((const C).obj A)

Tactic:
have : Fact Cardinal.aleph0.IsRegular := Cardinal.fact_isRegular_aleph0

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
A : C
this : Fact Cardinal.aleph0.IsRegular
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} ((const C).obj A)
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set ↑S),
    Ideal.span s = ⊤ → (∀ f ∈ s, Q (of (Localization.Away f))) → s.Finite → (ObjectProperty.ofObj f).isoClosure S
hs' : ¬s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
obtain ⟨s', hs's, hs'⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
    exact this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ (z₁ - z₂) = (i₂ ∘ₗ f₁) d
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
← h₁,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ (z₁ - z₂) = (g₁ ∘ₗ i₁) d
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
⊢ CharP R p

Tactic:
by
  obtain ⟨q, h⟩ := CharP.exists R
  exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra

Tactic:
AlgHom.fieldRange_toSubalgebra,

Goal state after:
F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).range = Subalgebra.map f L.toSubalgebra
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p

Tactic:
contrapose!
  rw [← EqualCharZero.iff_not_mixedCharZero]
  apply EqualCharZero.nonempty_algebraRat_iff

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
z : ℤ
hz : z ≠ 0
⊢ z • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p

Tactic:
AddSubgroup.mem_zmultiples_iff

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
⊢ iterate id a = const a

Tactic:
iterate_id

Goal state after:
α : Type u
a : α
⊢ const a = const a
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      fun x ↦
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
unfold corecOn

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1
α : 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 (pure r') s' → BisimO R (pure r').destruct s'.destruct → (pure r').head = s'.head ∧ R (pure r').tail s'.tail

Tactic:
refine recOn s' ?_ ?_

Goal state after:
case refine_1.refine_1
α : 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' : α
⊢ ∀ (a : α),
    R (pure r') (pure a) →
      BisimO R (pure r').destruct (pure a).destruct → (pure r').head = (pure a).head ∧ R (pure r').tail (pure a).tail

case refine_1.refine_2
α : 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' : α
⊢ ∀ (s : Computation α),
    R (pure r') s.think →
      BisimO R (pure r').destruct s.think.destruct → (pure r').head = s.think.head ∧ R (pure r').tail s.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2
α : 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' r' : Computation α
⊢ R r'.think s' → BisimO R r'.think.destruct s'.destruct → r'.think.head = s'.head ∧ R r'.think.tail s'.tail

Tactic:
refine recOn s' ?_ ?_

Goal state after:
case refine_2.refine_1
α : 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' r' : Computation α
⊢ ∀ (a : α),
    R r'.think (pure a) →
      BisimO R r'.think.destruct (pure a).destruct → r'.think.head = (pure a).head ∧ R r'.think.tail (pure a).tail

case refine_2.refine_2
α : 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' r' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail
Module: Mathlib.Data.Stream.Init

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

Tactic:
cases n with
  | zero => simp
  | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

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

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
this : (s.think.val s.think.length).isSome = true
⊢ s.length + 1 ≤ s.think.length

Tactic:
revert this

Goal state after:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ (s.think.val s.think.length).isSome = true → s.length + 1 ≤ s.think.length