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
⊢ toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom =
    G.op.whiskerLeft (toSheafify K F)

Tactic:
by
  let adj₁ := G.op.ranAdjunction A
  let adj₂ := sheafificationAdjunction J A
  let adj₃ := sheafificationAdjunction K A
  let adj₄ := G.sheafAdjunctionCocontinuous A J K
  change 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) =
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)
  apply (adj₁.homEquiv _ _).injective
  have eq := (adj₁.comp adj₂).unit_leftAdjointUniq_hom_app (adj₃.comp adj₄) F
  rw [Adjunction.comp_unit_app, Adjunction.comp_unit_app, comp_map,
    Category.assoc] at eq
  rw [adj₁.homEquiv_unit, Functor.map_comp, eq]
  apply (adj₁.homEquiv _ _).symm.injective
  simp only [Adjunction.homEquiv_counit, map_comp, Category.assoc,
    Adjunction.homEquiv_unit, Adjunction.unit_naturality]
  congr 3
  exact G.sheafAdjunctionCocontinuous_unit_app_hom A J K ((presheafToSheaf K A).obj F)

Goal state after:
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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ (mapPreimage K G F f ≫ F.obj.map p.op) ≫ F.obj.map a.op = F.obj.map g.op ≫ F.obj.map a.op

Tactic:
rw [Category.assoc, ← Functor.map_comp, ← op_comp, mapPreimage]

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ ⋯.amalgamate ⟨G.imageSieve f, ⋯⟩
        (fun x ↦
          match x with
          | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op)
        ⋯ ≫
      F.obj.map (a ≫ p).op =
    F.obj.map g.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J K : GrothendieckTopology C
h : J ≤ K
inst✝ : K.Subcanonical
x✝³ x✝² : C
x✝¹ : Sieve x✝²
x✝ : x✝¹ ∈ J x✝²
⊢ generate x✝¹.arrows ∈ J x✝²

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), fh₁ k = gh₁ k ≫ 𝟙 (F.Y ((congrIndexOneOfEq ⋯ ⋯) (fs₁ k)))
i j : E.I₀
k : E.I₁ i j
⊢ fh₁ k = gh₁ k

Tactic:
rw [hh₁ i j k]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), fh₁ k = gh₁ k ≫ 𝟙 (F.Y ((congrIndexOneOfEq ⋯ ⋯) (fs₁ k)))
i j : E.I₀
k : E.I₁ i j
⊢ gh₁ k ≫ 𝟙 (F.Y ((congrIndexOneOfEq ⋯ ⋯) (fs₁ k))) = gh₁ k
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
← J.W_whiskerLeft_iff (G := G) (K := K)

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan

pp: case refine_2
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)

Tactic:
· refine WalkingMulticospan.functorExt ?_ ?_ ?_ ?_
    · intro i
      exact G.mapIso (asIso (f.hom.h₀ i)).symm.op
    · intro i
      exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₁]
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₂]

Goal state after:
case refine_2
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose
          (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
              (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ (overEquiv Y) (generate R) = generate (Presieve.functorPushforward (Over.forget X) R)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) ?_
  · rw [overEquiv_iff] at hg
    obtain ⟨W, u, v, hv, huv⟩ := hg
    exact ⟨W.left, u.left, v.left, ⟨W, v, 𝟙 _, hv, by simp⟩, congr($(huv).left)⟩
  · rw [generate_le_iff]
    rintro Z g ⟨W, u, v, hu, rfl⟩
    exact (overEquiv_iff _ _).mpr ⟨W, Over.homMk v, u, hu, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Presieve.functorPullback (Over.forget X) S ∈
    (Precoverage.comap (Over.forget X) K).coverings { left := Z, right := right, hom := s }

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Tactic:
subsingleton

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ ⋯.adjunction.counit.app (⋯.functor.obj V) = eqToHom ⋯

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
⊢ objPairwiseOfFamily sf ∈ ((Pairwise.diagram U).op ⋙ F).sections

Tactic:
let G := (Pairwise.diagram U).op ⋙ F

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
⊢ objPairwiseOfFamily sf ∈ ((Pairwise.diagram U).op ⋙ F).sections
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Tactic:
by ext <;> simp

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ f (x • 1) = g (x • 1)

Tactic:
map_smul,

Goal state after:
R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ x • f 1 = g (x • 1)
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
s : ↑(CommRingCat.of S)
hs :
  s ∈
    (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inl).eqLocus
      (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inr)
⊢ ∃ a, (codRestrictEqLocusPushoutCocone R S) a = ⟨s, hs⟩

Tactic:
obtain ⟨t, rfl⟩ := Set.mem_range.mp <|
    Algebra.IsEffective.eqLocus_includeLeft_includeRight hf ▸ SetLike.mem_coe.mpr hs

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
t : R
hs :
  (algebraMap R S) t ∈
    (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inl).eqLocus
      (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inr)
⊢ ∃ a, (codRestrictEqLocusPushoutCocone R S) a = ⟨(algebraMap R S) t, hs⟩
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
this✝¹ : Small.{w, max u' v'} (Arrow A)
this✝ : Small.{w, v'} A
this : LocallySmall.{w, u', v'} A
e : A ≌ ShrinkHoms.{w} (Shrink.{w, v'} A) := (Shrink.equivalence A).trans (ShrinkHoms.equivalence (Shrink.{w, v'} A))
⊢ HasCardinalLT (Arrow (ShrinkHoms.{w} (Shrink.{w, v'} A))) κ

Tactic:
by simpa

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

Goal state before:
pp: case h₂
J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := ⋯
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := ⋯
i j : A✝
f : i ⟶ j
⊢ (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).2 = ((c₁.ι.app i, c₂.ι.app i) ≫ ((Functor.const A✝).obj (c₁.pt, c₂.pt)).map f).2

Tactic:
· simpa using c₂.w f

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

Goal state before:
pp: R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
⊢ (fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
      ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f) =
    f

Tactic:
by ext <;> simp

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

Goal state before:
pp: R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
fx : (A ⟶ R) × (σ → ↑R)
⊢ (fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i)))
      ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2)) fx) =
    fx

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ AlgebraTensorModule.lift
        (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
          (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) ∘ₗ
      ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
        ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) =
    LinearMap.id

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
⊢ ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
        ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
      AlgebraTensorModule.lift
        (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
          (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃)) =
    LinearMap.id

Tactic:
by ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over B)

Tactic:
have := ConstructProducts.over_binaryProduct_of_pullback (B := B)
  have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
  have := ConstructProducts.over_products_of_widePullbacks (B := B)
  apply has_limits_of_hasEqualizers_and_products

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

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (MorphismProperty.costructuredArrowObj L P).limitsOfShape (Discrete PEmpty.{1}) ≤
    MorphismProperty.costructuredArrowObj L P

Tactic:
rintro X p
    let t : IsTerminal X := (ObjectProperty.limitsOfShape_isEmpty_iff _ _ _ |>.mp p).some
    let e : X ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) := t.uniqueUpToIso CostructuredArrow.mkIdTerminal
    simpa [MorphismProperty.costructuredArrowObj_iff,
      P.costructuredArrow_iso_iff e] using P.id_mem (L.obj Y)

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
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ HasLimit D

Tactic:
have := hQe.createsLimitsWalkingParallelPair hQi R

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
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h : (Corec.f f (some b)).fst = none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
dsimp [Corec.f] at h

Goal state after:
case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h :
  (match f b with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ f a = b) ((map f s).get n)

Tactic:
get_map,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ f a = b) (f (s.get n))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ s₁ = s₂

Tactic:
apply Subtype.ext
  apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'
  · dsimp [Stream'.IsBisimulation]
    intro t₁ t₂ e
    match t₁, t₂, e with
    | _, _, ⟨s, s', rfl, rfl, r⟩ =>
      suffices head s = head s' ∧ R (tail s) (tail s') from
        And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
      have h := bisim r; revert r h
      refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_ <;> intro a' r h
      · constructor <;> dsimp at h
        · rw [h]
        · rw [h] at r
          rw [tail_pure, tail_pure, h]
          assumption
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · rw [destruct_pure, destruct_think] at h
        exact False.elim h
      · simp_all
  · exact ⟨s₁, s₂, rfl, rfl, r⟩

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
have := of_think_terminates h.terminates

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ ∃ m, s.Results a m ∧ n = m + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = (map (List.cons s.head) s.tail.inits).get n✝

Tactic:
get_map,

Goal state after:
case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ take (n✝ + 1).succ s = s.head :: s.tail.inits.get n✝
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
A : K
nth_num_eq : g.nums n = A
⊢ ∃ conts, g.conts n = conts ∧ conts.a = A

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
B : K
nth_denom_eq : g.dens n = B
⊢ ∃ conts, g.conts n = conts ∧ conts.b = B

Tactic:
by simpa

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
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1

Tactic:
destruct

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
⊢ (match (fun a' ↦ (a', s.tail)) <$> s.get? 0 with
      | none => []
      | some (x, r) => x :: take n r).length =
    n + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
k : α
⊢ s.get? n = some k → ∀ m ≤ n, ¬s.get? m = none

Tactic:
intro h m hmn

Goal state after:
α : Type u
s : Seq α
h✝ : s.Terminates
n : ℕ
k : α
h : s.get? n = some k
m : ℕ
hmn : m ≤ n
⊢ ¬s.get? m = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'

Tactic:
rw [← h1 a's] at ba'

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ (cons x s).enum.get? (n✝ + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n✝ + 1)

Tactic:
simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
    congr

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

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
n : ℕ
x y : α
hx : (s.drop n).head = some x
hy : s.get? (n + 1) = some y
this : ∀ (n : ℕ), motive (s.drop n)
⊢ y ∈ (s.drop (n + 1)).head

Tactic:
by simpa

Goal state after: