mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
U' : OpenNhds x := ⟨↑(unop U), ⋯⟩
⊢ F.map ((OpenNhds.inclusion y).map i.unop).op ≫ colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩)

Tactic:
let V' : OpenNhds x := ⟨_, (specializes_iff_forall_open.mp h _ (unop V).1.2 (unop V).2 :)⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
U' : OpenNhds x := ⟨↑(unop U), ⋯⟩
V' : OpenNhds x := ⟨↑(unop V), ⋯⟩
⊢ F.map ((OpenNhds.inclusion y).map i.unop).op ≫ colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝¹ : ContinuousAdd A
this✝ : ContinuousAdd B'
this : Continuous[inst✝⁴, τB] ⇑φ
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
rw [continuous_iff_coinduced_le] at this

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝¹ : ContinuousAdd A
this✝ : ContinuousAdd B'
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴
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:
rw [← smul_eq_mul, map_smul, h, map_smul]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (Algebra.linearMap R S) (g s) = 1 ⊗ₜ[R] s

Tactic:
← mul_one ((Algebra.linearMap R S) _),

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] ((Algebra.linearMap R S) (g s) * 1) = 1 ⊗ₜ[R] s
Module: Mathlib.Algebra.Category.Ring.EqualizerPushout

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
let isLimit : IsLimit fork :=
    (Fork.isLimitEquivOfIsos _
      (equalizerFork (pushoutCocone R S S).inl (pushoutCocone R S S).inr) (Iso.refl _) (Iso.refl _)
      (RingEquiv.toCommRingCatIso <| RingEquiv.ofBijective _
        (Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat R S))
      (by cat_disch) (by cat_disch) (by cat_disch)).symm
    (equalizerForkIsLimit (pushoutCocone R S S).inl (pushoutCocone R S S).inr)

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
isLimit : IsLimit fork :=
  (fork.isLimitEquivOfIsos (equalizerFork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr) (Iso.refl (of ↑S))
        (Iso.refl (pushoutCocone ↑R ↑S ↑S).pt)
        (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone ↑R ↑S) ⋯).toCommRingCatIso ⋯ ⋯ ⋯).symm
    (equalizerForkIsLimit (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr)
⊢ IsLimit (Fork.ofι f ⋯)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: 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₂
f : M →L[R] M₂
hf : f.inverse.IsInvertible
⊢ f.IsInvertible

Tactic:
by_contra H
  obtain ⟨_, _⟩ : Subsingleton M₂ ∧ Subsingleton M := by simpa [inverse, H] using hf
  simp_all [Subsingleton.elim f 0]

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
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ ((const J).obj (F.obj i₀)).map φ

Tactic:
dsimp
        rw [comp_id]
        let i := IsFiltered.max i₀ j'
        let α : i₀ ⟶ i := IsFiltered.leftToMax _ _
        let β : j' ⟶ i := IsFiltered.rightToMax _ _
        rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, assoc]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤
    (freeObj R Y).topologicalSpace

Tactic:
refine le_sInf fun (τ : TopologicalSpace (_ →₀ R)) ⟨hτ₁, hτ₂, hτ₃⟩ ↦ ?_

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤ τ
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
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
have : Fact (κF ⊔ κG).IsRegular := ⟨iteInduction (fun _ ↦ Fact.out) (fun _ ↦ Fact.out)⟩

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
this : Fact (max κF κG).IsRegular
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : C₁
⊢ x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) → G x = 0

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ G ((δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x) = 0
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✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
heq : Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
rw [P.costructuredArrowObj_iff, heq, ← hd.coconePointUniqueUpToIso_hom_desc (hc _),
      P.cancel_left_of_respectsIso]

Goal state after:
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✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
heq : Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ P ((hc (d.diag ⋙ proj L X ⋙ L)).desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } })
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
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
x : T ⊗[R] ↥(f.equalizer g)
⊢ ↑((tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) x

Tactic:
induction x with
  | zero => rfl
  | tmul => rfl
  | add x y hx hy => simp [hx, hy]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n = ↑0

Tactic:
rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})
⊢ ↑↑n ∈ Ideal.span {↑↑n}
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ (algebraMap K L).fieldRange
⊢ x ∈ Set.range ⇑(algebraMap K L)

Tactic:
by rwa [Set.mem_range, ← RingHom.mem_fieldRange]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
o : Option β
⊢ corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none

Tactic:
induction n generalizing o with
  | zero =>
    change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
    rcases o with - | b <;> intro h
    · rfl
    dsimp [Corec.f] at h
    dsimp [Corec.f]
    revert h; rcases h₁ : f b with - | s <;> intro h
    · rfl
    · obtain ⟨a, b'⟩ := s
      contradiction
  | succ n IH =>
    rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

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

Goal state before:
pp: case some.succ
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : s.val n = (pure a).val n
⊢ s.val (n + 1) = (pure a).val (n + 1)

Tactic:
exact s.2 IH

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    nil.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
trivial

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (nil.append nil).destruct nil.destruct

Tactic:
trivial

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

Goal state before:
pp: case nil
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) nil.destruct
    nil.destruct

Tactic:
trivial

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (of v).s.get? 0 = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
rw [of, IntFractPair.seq1]
  simp only [Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.get?, Stream'.map]
  rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
  split <;> simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ (g₂ j).comp ((f' i j h).comp (g₁ i)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
← RingHom.comp_assoc,

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ ((g₂ j).comp (f' i j h)).comp (g₁ i) = (f'' i j h).comp ((g₂ i).comp (g₁ i))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.cons
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α}, (∀ x ∈ s, p x) → x ∈ take m s → p x
hd : α
tl : Seq α
h_all : ∀ x ∈ cons hd tl, p x
hx : x ∈ take (m + 1) (cons hd tl)
⊢ p x

Tactic:
simp only [take_succ_cons, List.mem_cons, mem_cons_iff, forall_eq_or_imp] at hx h_all

Goal state after:
case succ.cons
α : Type u
p : α → Prop
x : α
m : ℕ
ih : ∀ {s : Seq α}, (∀ x ∈ s, p x) → x ∈ take m s → p x
hd : α
tl : Seq α
hx : x = hd ∨ x ∈ take m tl
h_all : p hd ∧ ∀ a ∈ tl, p a
⊢ p x
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num

Tactic:
obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
    ∃ ifp_n',
      IntFractPair.stream q n = some ifp_n' ∧
        ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
  have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
  cases this
  rw [← IntFractPair.of_eq_ifp_succ_n]
  obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq
  have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
  exact of_inv_fr_num_lt_num_of_pos this

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).toPoly.roots = (Polynomial.map φ P.toPoly).roots

Tactic:
map_toPoly

Goal state after:
R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (Polynomial.map φ P.toPoly).roots = (Polynomial.map φ P.toPoly).roots
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ P.toPoly.IsRoot x ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0

Tactic:
IsRoot,

Goal state after:
R : Type u_1
P : Cubic R
inst✝¹ : CommRing R
inst✝ : IsDomain R
h0 : P.toPoly ≠ 0
x : R
⊢ eval x P.toPoly = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 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
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
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : 1 / |den'| = 1 / den'
⊢ |(-1) ^ n / den'| = 1 / den'

Tactic:
abs_div,

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
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this✝ : 1 / den' ≤ 1 / den
this : 1 / |den'| = 1 / den'
⊢ |(-1) ^ n| / |den'| = 1 / den'