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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : ((overEquiv Y) (generate R)).arrows g
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g

Tactic:
overEquiv_iff

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : (generate R).arrows (Over.homMk g ⋯)
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.map f) ((Sieve.overEquiv U).symm S) ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
Sieve.functorPushforward_over_map

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f → f ≠ 0

Tactic:
intro h w
        have j : IsIso (f ≫ i.hom) := by infer_instance
        rw [Simple.mono_isIso_iff_nonzero] at j
        subst w
        simp at j

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
⊢ f ≫ i.hom ≠ 0

Tactic:
intro w

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ False
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
⊢ f ≠ 0

Tactic:
intro w

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
⊢ ∀ (f_1 : ι → Opens ↑X), PreservesLimit (Discrete.functor f_1) hf.functor

Tactic:
intro g

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
g : ι → Opens ↑X
⊢ PreservesLimit (Discrete.functor g) hf.functor
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U

pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)

Tactic:
· refine iSup_le ?_
    intro f
    exact f.2.1.le

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case hF₂
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) h.functor

Tactic:
exact h.isOpenMap.coverPreserving

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
V : (Opens ↑Y)ᵒᵖ
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ unop V
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F ((Opens.map f).obj (unop V)) x hx =
    F.germ (unop V) ((ConcreteCategory.hom f) x) hx

Tactic:
by
  simpa using pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk
    C f F ((Opens.map f).obj V.unop) x hx V.unop (by rfl)

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ

Tactic:
· intro c hc
    simpa [hy] using hc

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

Goal state before:
pp: 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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ α.addCommGroupIsoToAddEquiv ((ConcreteCategory.hom (cM.ι.app i)) (r • m)) =
    ↑(hcR.coconePointUniqueUpToIso
                  (RingCat.FilteredColimits.colimitCoconeIsColimit
                    R)).ringCatIsoToRingEquiv.toRingHom.toMonoidWithZeroHom
        ((ConcreteCategory.hom (cR.ι.app i)) r) •
      (hcM.coconePointUniqueUpToIso
              (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)).addCommGroupIsoToAddEquiv.toFun
        ((ConcreteCategory.hom (cM.ι.app i)) m)

Tactic:
change (cM.ι.app i ≫ α.hom) _ = (HSMul.hSMul (α := RingCat.FilteredColimits.colimit R)
    (β := AddCommGrpCat.FilteredColimits.colimit M)
    ((cR.ι.app i ≫ β.hom) r) ((cM.ι.app i ≫ α.hom) m))

Goal state after:
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ (ConcreteCategory.hom (cM.ι.app i ≫ α.hom)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app i ≫ β.hom)) r • (ConcreteCategory.hom (cM.ι.app i ≫ α.hom)) m
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
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
⊢ f = g

Tactic:
ext s

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
s : ↑(of S)
⊢ (Hom.hom f) s = (Hom.hom g) s
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
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
s : ↑(of S)
⊢ (Hom.hom f) s = (Hom.hom g) s

Tactic:
simpa using! congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
h : IsEffective R S
⊢ ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom) = Set.range ⇑(algebraMap R S)

Tactic:
ext s

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
h : IsEffective R S
s : S
⊢ s ∈ ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom) ↔ s ∈ Set.range ⇑(algebraMap R S)
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
h : IsEffective R S
⊢ ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom) = Set.range ⇑(algebraMap R S)

Tactic:
ext s
  refine ⟨?_, fun ⟨_, hr⟩ ↦ by simp [← hr]⟩
  intro hs
  exact (h s).mp <| (TensorProduct.includeLeftSubRight_apply (R := R) s).symm ▸ sub_eq_zero.mpr hs

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e (↑F x✝) = f x✝

Tactic:
hF

Goal state after:
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e ((↑e.symm ∘SL f) x✝) = f x✝
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
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsCofiltered.bowtie
    (IsCofiltered.minToRight i₀ j) β (IsCofiltered.minToLeft i₀ j) α
  dsimp [coneπApp]
  rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]

Goal state after:
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
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j

Tactic:
let i := IsFiltered.max i₀ j

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
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
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 : T
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.IsStableUnderBaseChange
A : P.Over Q Y
⊢ ((pullbackCongr ⋯).hom.app A).left ≫ pullback.fst A.hom f = pullback.fst A.hom f

Tactic:
simp [pullbackCongr]

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

Goal state before:
pp: case tmul.tmul.tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm (r ⊗ₜ[R] s • x ⊗ₜ[R] z ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
smul_tmul'

Goal state after:
case tmul.tmul.tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm ((r ⊗ₜ[R] s • x ⊗ₜ[R] z) ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ P

Tactic:
apply h r r_prime

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ⋯
r_pos : r ≠ 0
r_prime : Nat.Prime r
⊢ MixedCharZero R r
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) → ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
intro g

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
g : ∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
⊢ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ F

Tactic:
exact (mem_restrict h y).1 ((mem_lift y).1 hx)

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

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b ↦ a = b) (s₁.get n)
⊢ (fun b ↦ s₁.get n = b) ((s₁ ⋈ s₂).get (2 * n))

Tactic:
get_interleave_left

Goal state after:
α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b ↦ a = b) (s₁.get n)
⊢ (fun b ↦ s₁.get n = b) (s₁.get n)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
hn : s.get? n = none
⊢ False

Tactic:
exact h n hn n le_rfl hn

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

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none

Tactic:
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: case cons
α : 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₂
c : α
t₁ : Seq α
⊢ a ∈ (cons c t₁).append s₂ → (cons c t₁).append s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
| cons c t₁ =>

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

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

Tactic:
rw [Nat.add_comm]; symm; apply dropn_add

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

Goal state before:
pp: m n k : ℕ
⊢ (fib m).gcd (fib (n + (k + 1) * m)) = (fib m).gcd (fib n)

Tactic:
rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]

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

Goal state before:
pp: case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ { h := h✝, s := s✝ }.squashGCF (n✝ + 1) = { h := h✝, s := s✝ }

Tactic:
simp only [squashGCF, mk.injEq, true_and]

Goal state after:
case succ.mk
K : Type u_1
inst✝ : DivisionRing K
n✝ : ℕ
h✝ : K
s✝ : Stream'.Seq (Pair K)
terminatedAt_n : { h := h✝, s := s✝ }.TerminatedAt (n✝ + 1)
⊢ squashSeq s✝ n✝ = s✝
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this✝ : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
this : ↑(fib n) + ↑(fib (n + 1)) ≤ gp.a * ppconts.b + gp.b * pconts.b
⊢ ↑(fib (n + 2)) ≤ ((of v).contsAux (n + 2)).b

Tactic:
simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ ↑(((decompose V) ↑(((decompose V) 1) i)) i) = ↑(((decompose V) 1) i)

Tactic:
decompose_coe,

Goal state after:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ ↑(((of (fun i ↦ ↥(V i)) i) (((decompose V) 1) i)) i) = ↑(((decompose V) 1) i)
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ ↑(((of (fun i ↦ ↥(V i)) i) (((decompose V) 1) i)) i) = ↑(((decompose V) 1) i)

Tactic:
of_eq_same

Goal state after:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ ↑(((decompose V) 1) i) = ↑(((decompose V) 1) i)
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ ↑(((decompose V) ↑(((decompose V) 1) i)) j) = 0

Tactic:
decompose_coe,

Goal state after:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ ↑(((of (fun i ↦ ↥(V i)) i) (((decompose V) 1) i)) j) = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
by
  let g := of v
  rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated
  · have : g.TerminatedAt n :=
      terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)
    have : g.dens (n + 1) = g.dens n :=
      dens_stable_of_terminated n.le_succ this
    rw [this]
  · obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b :=
      Option.ne_none_iff_exists'.mp not_terminated
    have : 1 ≤ b := of_one_le_get?_partDen nth_partDen_eq
    calc
      g.dens n ≤ b * g.dens n := by
        simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
      _ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)

Tactic:
obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
    Option.ne_none_iff_exists'.1 not_terminatedAt_n

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)