mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
        (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))

Tactic:
adj₁.homEquiv_unit,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₁.unit.app F ≫
      G.op.ran.map
        (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
          (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
⊢ ℱ.obj ≅ ℱ'.obj

Tactic:
haveI : IsIso (sheafHom i.hom) := by apply NatIso.isIso_of_isIso_app

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
this✝ : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
this : IsIso (sheafHom i.hom)
⊢ ℱ.obj ≅ ℱ'.obj
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝² E✝¹ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i'✝ j✝ j'✝ : E✝.I₀
hii'✝ : i✝ = i'✝
hjj'✝ : j✝ = j'✝
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq hii' hjj') k) = E.Y k

Tactic:
by subst hii' hjj'; simp

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteColimitCocone (Discrete.functor f)).cocone.pt = Finset.univ.sup f

Tactic:
change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f

Goal state after:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.sup f
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.univ.inf (cospan f g).obj

Tactic:
rw [finite_limit_eq_finset_univ_inf]

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)
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
⊢ (ConcreteCategory.hom (F.map (homOfLE hVU).op ≫ F.germ V x hxV)) s = (ConcreteCategory.hom (F.germ U x hxU)) s

Tactic:
F.germ_res'

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)
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
⊢ (ConcreteCategory.hom (F.germ U x ⋯)) s = (ConcreteCategory.hom (F.germ U x hxU)) s
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U₁ : C
a₁ : (R ⋙ forget RingCat).obj U₁
U₂ V : C
b : (M ⋙ forget Ab).obj V
f : U₁ ⟶ U₂
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)))
          ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd)

Tactic:
obtain ⟨s, α, β, h₁, h₂⟩ :=
      bowtie (leftToMax U₁ V) (f ≫ leftToMax U₂ V)
        (rightToMax U₁ V) (rightToMax U₂ V)

Goal state after:
case refine_2
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U₁ : C
a₁ : (R ⋙ forget RingCat).obj U₁
U₂ V : C
b : (M ⋙ forget Ab).obj V
f : U₁ ⟶ U₂
s : C
α : IsFiltered.max U₁ V ⟶ s
β : IsFiltered.max U₂ V ⟶ s
h₁ : leftToMax U₁ V ≫ α = (f ≫ leftToMax U₂ V) ≫ β
h₂ : rightToMax U₁ V ≫ α = rightToMax U₂ V ≫ β
⊢ (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (M ⋙ forget Ab).ιColimitType (IsFiltered.max ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)))
          ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd)
Module: Mathlib.Topology.Algebra.Module.Equiv

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

Tactic:
by simp [h 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
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
⊢ PreservesColimitsOfShape J F

Tactic:
have := IsCardinalFiltered.of_le J h
    exact F.preservesColimitsOfShape_of_isCardinalAccessible κ J

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable (F.obj X) κ ↔ IsCardinalPresentable X κ

Tactic:
by
  constructor
  · intro
    exact isCardinalPresentable_of_iso
      (show F.inv.obj (F.obj X) ≅ X from F.asEquivalence.unitIso.symm.app X :) κ
  · intro
    infer_instance

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Subring.closure
      (Set.range ⇑(ConcreteCategory.hom (pushout.inl φ ψ)) ∪ Set.range ⇑(ConcreteCategory.hom (pushout.inr φ ψ))) ≤
    (ConcreteCategory.hom fBC).range

Tactic:
Subring.closure_le

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Set.range ⇑(ConcreteCategory.hom (pushout.inl φ ψ)) ∪ Set.range ⇑(ConcreteCategory.hom (pushout.inr φ ψ)) ⊆
    ↑(ConcreteCategory.hom fBC).range
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mp
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
N₃ : Type u_7
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₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[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₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ ι₃ (F k) = ι₃ x

Tactic:
rw [← ι₃.comp_apply, ← hF, f₂.comp_apply, hk, map_sub, H₁, hf.apply_apply_eq_zero, sub_zero]

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ P.underObj.op.IsClosedUnderLimitsOfShape WalkingSpanᵒᵖ

Tactic:
←
    ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff _ _ (Over.opEquivOpUnder _),

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (P.underObj.op.inverseImage (Over.opEquivOpUnder X).functor).IsClosedUnderLimitsOfShape WalkingSpanᵒᵖ
Module: Mathlib.RingTheory.Flat.Equalizer

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

Tactic:
by
  induction x <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

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

Tactic:
by
  induction x <;> simp_all

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.destruct = none → s = nil

Tactic:
dsimp [destruct]
  rcases f0 : get? s 0 <;> intro h
  · exact get?_zero_eq_none.mp f0
  · contradiction

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s

Tactic:
by
    rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = s.length' + 1

Tactic:
by_cases h : (cons x s).Terminates

Goal state after:
case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.length h = 0 ↔ s = nil

Tactic:
simp [length, TerminatedAt]

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
rw [nth_cont_eq_succ_nth_contAux,
    contsAux_recurrence nth_s_eq nth_contsAux_eq succ_nth_contsAux_eq]

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

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).Results b (n + m✝)

Tactic:
h1.len_unique (results_pure _)

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m✝ : ℕ
h1 : (pure a).Results a m✝
⊢ (f a).Results b (n + 0)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : 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₂
s₁ : Seq α
⊢ a ∈ s₁.append s₂ → s₁.append s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂

Tactic:
cases s₁ with

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

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ ↑(l ++ₛ s) = (↑l).append ↑s

Tactic:
induction l <;> simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) b a = LiftRelAux R C a b

Tactic:
rcases a with a | ca

Goal state after:
case inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
a : α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inl a) = LiftRelAux R C (Sum.inl a) b

case inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
ca : Computation α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (nil.append (cons x✝ t))).destruct ((map f nil).append (map f (cons x✝ t))).destruct

Tactic:
simpa using ⟨nil, t, by simp, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case ih
ι : 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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (lift G f P g✝ Hg) ((of G f i✝) g) = 0
⊢ (of G f i✝) g = 0

Tactic:
lift_of

Goal state after:
case ih
ι : 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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

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

Tactic:
by rw [Int.fract_add_floor]

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
m n : ℕ
h : n ≠ m
⊢ (s.set m x).get? n = s.get? n

Tactic:
simp [set, get?_update, h]

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

Goal state before:
pp: n : ℕ
⊢ fib (n + n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
fib_add

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
⊢ Pairwise R s

Tactic:
by
  simp only [Pairwise]
  intro i j h_ij x hx y hy
  obtain ⟨k, hj⟩ := Nat.exists_eq_add_of_lt h_ij
  rw [← head_dropn] at hx
  rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy
  have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) i
  generalize s.drop i = s' at *
  cases s' with
  | nil => simp at hx
  | cons hd tl =>
    simp only [head_cons, Option.mem_def, Option.some.injEq, get?_cons_succ] at hx hy
    exact hx ▸ all_get (step hd tl this).left hy

Goal state after: