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

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X)) =
    (RingCat.Hom.hom (φ.hom.app U)).comp (RingCat.Hom.hom (S.obj.map (hX.to U)))

Tactic:
rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality]

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app X ≫ R.obj.map (hX'.to (F.op.obj U))) =
    RingCat.Hom.hom (φ.hom.app X ≫ ((F.sheafPushforwardContinuous RingCat J K).obj R).obj.map (hX.to U))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝² : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
inst✝ : M.IsFinitePresentation
⊢ ∃ σ, σ.IsFiniteType

Tactic:
by
    obtain ⟨σ, _⟩ := IsFinitePresentation.exists_quasicoherentData M
    exact ⟨σ.localGeneratorsData, inferInstance⟩

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
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := ⋯
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ gl = t

Tactic:
symm

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
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := ⋯
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ t = gl
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ ((Opens.map f).obj U) x hU =
    ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom

Tactic:
symm

Goal state after:
case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
e_3✝ :
  ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) =
    colimit ((OpenNhds.map f x).op ⋙ (OpenNhds.inclusion x).op ⋙ F)
e_4✝ : F.stalk x = colimit ((OpenNhds.inclusion x).op ⋙ F)
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hU ≫
      (Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).hom =
    F.germ ((Opens.map f).obj U) x hU
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 G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
⊢ Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map α))

Tactic:
intro s t hst
  obtain ⟨U₁, hxU₁, hU₁, s, rfl⟩ := exists_mem_germ_eq_of_isBasis hB _ x s
  obtain ⟨U₂, hxU₂, hU₂, t, rfl⟩ := exists_mem_germ_eq_of_isBasis hB _ x t
  rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst
  obtain ⟨W, hxW, hW, iWU₁, iWU₂, heq⟩ := germ_eq_of_isBasis hB _ _ hxU₁ hxU₂ hst
  simp only [← α.naturality_apply, (hα W hW).eq_iff] at heq
  simpa [germ_res_apply'] using congr(F.germ W x hxW $heq)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ s.pt ⟶ F.obj.obj (op (U ⊔ V))

Tactic:
let ι : ULift.{w} WalkingPair → Opens X := fun j => WalkingPair.casesOn j.down U V
  have hι : U ⊔ V = iSup ι := by
    ext
    rw [Opens.coe_iSup, Set.mem_iUnion]
    constructor
    · rintro (h | h)
      exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
    · rintro ⟨⟨_ | _⟩, h⟩
      exacts [Or.inl h, Or.inr h]
  refine
    (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.lift
        ⟨s.pt,
          { app := ?_
            naturality := ?_ }⟩ ≫
      F.1.map (eqToHom hι).op
  · rintro ((_ | _) | (_ | _))
    exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op,
      s.snd ≫ F.1.map (homOfLE inf_le_left).op]
  rintro ⟨i⟩ ⟨j⟩ f
  let g : j ⟶ i := f.unop
  have : f = g.op := rfl
  clear_value g
  subst this
  rcases i with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩) <;>
  rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩) <;>
  rcases g with ⟨⟩ <;>
  dsimp [Pairwise.diagram] <;>
  simp only [ι, Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id]
  rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc,
    Category.assoc, ← F.1.map_comp, ← F.1.map_comp]
  exact s.condition.symm

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

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₁
T : (M₁ →L[R₁] M₁)ˣ
⊢ IsHomeomorph ⇑↑T

Tactic:
exact (homeomorphOfUnit T).isHomeomorph

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (F.map f)

Tactic:
by
    suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec
    exact ⟨F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι _)) f) ≫
      adj.counit.app (Injective.under (F.obj X)), by simp [← Functor.map_comp_assoc]⟩

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

Goal state before:
pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))

Tactic:
· refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩
    let : Algebra R T := (ofHom (algebraMap R S) ≫ g).hom.toAlgebra
    let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩
    let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩
    ext s
    simpa using! congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²¹ : Semiring R₁
inst✝²⁰ : Semiring R₂
inst✝¹⁹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁸ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁷ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁶ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹⁵ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹⁴ : RingHomInvPair σ₁₃ σ₃₁
inst✝¹³ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
M₄ : Type u_7
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommMonoid M₄
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h₁ : f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂
h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁
x : M₂
⊢ f₁ (f₂ x) = x

Tactic:
simpa using congr($(h₁) x)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ (↑f * f.inv) x = x

Tactic:
rw [f.val_inv]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ 1 x = x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
hf : f.IsInvertible
⊢ (g ∘SL f).IsInvertible

Tactic:
rcases hg with ⟨N, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
⊢ (↑N ∘SL f).IsInvertible
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (f ∘SL ↑e).inverse = ↑e.symm ∘SL f.inverse

Tactic:
rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, comp_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hg with ⟨N, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
N : M₂ ≃L[R] M₃
⊢ (↑N ∘SL f).inverse = f.inverse ∘SL (↑N).inverse
Module: Mathlib.Algebra.Category.Ring.Topology

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

Tactic:
refine IsEmbedding.of_comp (continuous_precomp _) (IsInducing.induced _).continuous ?_

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ (piScalarRightInv R S N ι) (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

Tactic:
by
  simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
⊢ Under.Hom.right c.inl ≫ Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)) = s.inl

Tactic:
by simpa only using! congr($(hc.fac _ _).right)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
⊢ Under.Hom.right c.inr ≫ Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)) = s.inr

Tactic:
by simpa only using! congr($(hc.fac _ _).right)

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

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

Tactic:
ext; apply pushout.hom_ext <;> simp

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

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ (map Q hPf ⋙ pushout P Q f).map g ≫ Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯ =
    Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g

Tactic:
ext; apply pushout.hom_ext <;> simp

Goal state after:
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
⊢ 2 ≠ 0

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
⊢ 3 ≠ 0

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ p = r

Tactic:
symm

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
r_dvd_p : r ∣ p
⊢ r = p
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

pp: case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Tactic:
· left
    exact h

Goal state after:
case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ take 0 s = []

Tactic:
by
  cases s <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
⊢ match
    match Bind.g c.destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    c.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
rcases destruct c with b | cb

Goal state after:
case inl
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
b : β
⊢ match
    match Bind.g (Sum.inl b) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

case inr
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c cb : Computation β
⊢ match
    match Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
⊢ (take (k + 1) s)[n]? = if n < k + 1 then s.get? n else none

Tactic:
by
    rw [take]
    cases h : destruct s with
    | none =>
      simp [destruct_eq_none h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.append nil = s

Tactic:
by
  apply coinduction2 s; intro s
  cases s
  · trivial
  · rw [cons_append, destruct_cons, destruct_cons]
    dsimp
    exact ⟨rfl, _, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
symm

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n
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:
by
  simp [set, get?_update, h]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_eq_zero : ifp_succ_n.fr = 0
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
      -- use the IH and the fact that ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ to prove this case
      obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
          ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
        IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero
      obtain rfl : ifp_n = ifp_n' := by injection Eq.trans nth_stream_eq.symm nth_stream_eq'
      have s_nth_eq : g.s.get? n = some ⟨1, ⌊ifp_n.fr⁻¹⌋⟩ :=
        get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq nth_fract_ne_zero
      rw [← ifp_n_fract_inv_eq_floor] at s_nth_eq
      suffices v = compExactValue ppconts pconts ifp_n.fr by
        simpa [conts, contsAux, s_nth_eq, compExactValue, nth_fract_ne_zero] using this
      exact IH nth_stream_eq

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

Goal state before:
pp: case succ
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
x : α
hx : x ∈ (Seq.cons hd tl).get? i
y : α
k : ℕ
h_ij : i < k + 1
hy : y ∈ tl.get? k
⊢ R x y

Tactic:
cases i with
    | zero =>
      simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx
      exact hx ▸ all_get h_hd hy
    | succ n => exact h_tl n k (by lia) x hx y hy

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

Goal state before:
pp: n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5

Tactic:
decide

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))

Tactic:
rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
    simp only [← add_assoc, add_tsub_cancel_right]
    ring

Goal state after:
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
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ s.get? (i + k + 1)
hj : j = i + k + 1
⊢ R x y

Tactic:
← head_dropn,

Goal state after:
α : 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
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop (i + k + 1)).head
hj : j = i + k + 1
⊢ R x y