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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
W : C
q : W ⟶ Z
⊢ (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)).arrows q →
    (Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))).arrows q

Tactic:
⟨x, h⟩

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
W : C
q : W ⟶ Z
x : ToType ((H.op ⋙ F).obj (Opposite.op W))
h :
  (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op W))) x =
    (ConcreteCategory.hom ((H.op ⋙ G).map q.op)) ((ConcreteCategory.hom (G.map m.op)) a)
⊢ (Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))).arrows q
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h
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 F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom = 𝟙 (E.Y k) ∧
    (e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom) ≫ e.hom.h₁ k = 𝟙 (F.Y (e.hom.s₁ k))

Tactic:
simp only [PreOneHypercover.hom_inv_h₁_assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp,
    Iso.inv_hom_id, Category.assoc, true_and, PreOneHypercover.congrIndexOneOfEqIso_hom_naturality]

Goal state after:
case h
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 F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      eqToHom ⋯ ≫ e.hom.h₁ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
apply +allowSynthFailures createsColimitsOfShapeLeftOp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F
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
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f

Tactic:
by
  rw [← W_inverseImage_whiskeringLeft J K G]
  rfl

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

Goal state before:
pp: case refine_2.left
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
a✝ : E.multicospanShape.L
⊢ ((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)).π.app
      (WalkingMulticospan.left a✝) =
    (Iso.refl
          ((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)).pt).hom ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.left a✝)

Tactic:
| left _ =>

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g → ((overEquiv ((Over.map f).obj Z)).symm S).arrows g

Tactic:
rintro ⟨T, a, b, ha, rfl⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
T : Over X
a : T ⟶ Z
b : W ⟶ (Over.map f).obj T
ha : ((overEquiv Z).symm S).arrows a
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows (b ≫ (Over.map f).map a)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ ⊤ ≤ E.toPreOneHypercover.sieve₁' i j

Tactic:
intro Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
⊢ ∀ (f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)),
    ⊤.arrows f → (E.toPreOneHypercover.sieve₁' i j).arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
⊢ (Over.forget X).PreservesOneHypercovers (J.over X) J

Tactic:
intro Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
⊢ ∀ (E : (J.over X).OneHypercover Y), E.IsPreservedBy (Over.forget X) J
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
⊢ (Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))

Tactic:
intro Y

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
⊢ ∀ (E : (J.over X).OneHypercover Y), E.IsPreservedBy (Over.post F) (K.over (F.obj X))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage

Tactic:
intro Y

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
⊢ (Precoverage.comap (Over.forget X) K).coverings Y ⊆ (K.toGrothendieck.over X).toPrecoverage.coverings Y
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
Y : D
X : CostructuredArrow F Y := Classical.arbitrary (CostructuredArrow F Y)
this : ↑s₁ (F.obj X.left) = ↑s₂ (F.obj X.left)
h₁ : (ConcreteCategory.hom (P.map X.hom)) (↑s₁ (F.obj X.left)) = ↑s₁ Y
h₂ : (ConcreteCategory.hom (P.map X.hom)) (↑s₂ (F.obj X.left)) = ↑s₂ Y
⊢ ↑s₁ Y = ↑s₂ Y

Tactic:
rw [← h₁, this, h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: 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) [Mono f], IsIso f ↔ f ≠ 0

Tactic:
intro Y

Goal state after:
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) [Mono f], IsIso f ↔ f ≠ 0
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U

Tactic:
rintro x ⟨_, ⟨s, rfl⟩, _, ⟨rfl : _ = U, rfl⟩, hx : f x ∈ s⟩

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
s : Opens ↑Y
hx : (ConcreteCategory.hom f) x ∈ s
⊢ x ∈ (Opens.map f).obj s
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₁
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : s ∈ Module.End.invtSubmodule ↑f
⊢ s.topologicalClosure ∈ Module.End.invtSubmodule ↑f

Tactic:
rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢

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₁
inst✝¹ : ContinuousSMul R₁ M₁
inst✝ : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : Submodule.map (↑f) s ≤ s
⊢ Submodule.map (↑f) s.topologicalClosure ≤ s.topologicalClosure
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_9
E : Type u_10
F : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : g ∘SL f = ContinuousLinearMap.id R E
⊢ Function.LeftInverse ⇑g ⇑f

Tactic:
by
  simpa [coe_comp, ← Function.leftInverse_iff_comp] using congr(⇑$hinv)

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.one
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) one) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) one)

Tactic:
rw [quot_one, map_one]
      rfl

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝ : Fact κF.IsRegular
h✝ : F.IsCardinalAccessible κF
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
obtain ⟨κG, _, _⟩ := IsAccessible.exists_cardinal (F := G)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
⊢ (MorphismProperty.structuredArrowObj L P).limitsOfShape J Y ≤ MorphismProperty.structuredArrowObj L P Y

Tactic:
by
    intro ⟨d⟩
    let hd : IsLimit ((CategoryTheory.StructuredArrow.proj X L ⋙ L).mapCone d.cone) :=
      isLimitOfPreserves _ d.isLimit
    have heq : Y.hom = hd.lift { pt := X, π := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [IsLimit.fac]
      simp
    rw [P.structuredArrowObj_iff, heq, ← (hc _).lift_comp_conePointUniqueUpToIso_hom hd,
      P.cancel_right_of_respectsIso]
    exact H _ _ d.prop_diag_obj

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✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a.left = a.left ≫ (Over.mk ⊤ (𝟙 X) ⋯).hom

Tactic:
simp only [mk_left, Functor.const_obj_obj, mk_hom, Category.comp_id]

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

Goal state before:
pp: case h_obj
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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Over Q X), (map Q ⋯).obj X_1 = (map Q hf ⋙ map Q hg).obj X_1

Tactic:
simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
x : L
⊢ f x ∈ ↑(map f S) ↔ x ∈ S

Tactic:
simp [Function.Injective.mem_set_image (f := f) f.injective]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
F E✝ E'✝ : Subfield L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
exact extendScalars_le_extendScalars_iff _ _

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

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E✝ E'✝ : IntermediateField K L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'

Tactic:
exact extendScalars_le_extendScalars_iff _ _

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
by
  constructor
  · intro h_alg
    have h_alg' : Algebra ℚ R := h_alg.some
    apply of_algebraRat
  · intro h
    apply Nonempty.intro
    exact algebraRat h

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.head = Prod.fst <$> s.destruct

Tactic:
unfold destruct head

Goal state after:
α : Type u
s : Seq α
⊢ s.get? 0 = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> s.get? 0
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
      subst conts
      rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
      ring

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Seq α
⊢ (map f s).Terminates ↔ s.Terminates

Tactic:
simp [Terminates]

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

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

Tactic:
simpa using ⟨s, t, rfl, rfl⟩

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

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
obtain ⟨ifp_n, nth_stream_eq, nth_fract_ne_zero, -⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
        ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
      IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
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
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
Module: Mathlib.Data.Nat.Fib.Basic

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

Tactic:
exact fib_lt_fib_succ (self_le_add_left _ _)

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
⊢ Pairwise R s

Tactic:
simp only [Pairwise]

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 : ℕ), i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
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
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
⊢ Pairwise R s

Tactic:
simp only [Pairwise]

Goal state after:
α : 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
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
⊢ ∀ (i j : ℕ), i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join

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

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

Goal state before:
pp: case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
this : (↑fr)⁻¹ = ↑fr⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
have coe_of_fr := coe_of_rat_eq this

Goal state after:
case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
this : (↑fr)⁻¹ = ↑fr⁻¹
coe_of_fr : mapFr Rat.cast (IntFractPair.of fr⁻¹) = IntFractPair.of (↑fr)⁻¹
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Tactic:
intro m IH m_le_n

Goal state after:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
m_le_n : m ≤ n
⊢ g.contsAux m = (g.squashGCF n).contsAux m
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ P.toPoly.leadingCoeff = 1

Tactic:
leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero),

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ P.a = 1
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → (↑↑c).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
intro gp m _ s_nth_eq

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a✝ : m < n
s_nth_eq : (↑↑c).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Subsingleton V
a✝ : Nontrivial W
⊢ ∃ T, f = conjAlgEquiv K T

Tactic:
simpa using congr(f $(Subsingleton.allEq 0 1))

Goal state after: