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

Goal state before:
pp: case op
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)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
⊢ ∀
    (s :
      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj
        (op ⟨V, m⟩)),
    (ConcreteCategory.hom
            (((forget C).mapCocone
                    (colimit.cocone
                      (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
              (op ⟨V, m⟩)))
          s =
        t →
      ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
intro s

Goal state after:
case op
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)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
V : Opens ↑X
m : x ∈ V
s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj (op ⟨V, m⟩)
⊢ (ConcreteCategory.hom
          (((forget C).mapCocone
                  (colimit.cocone
                    (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app
            (op ⟨V, m⟩)))
        s =
      t →
    ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case h
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
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ ∀ (i : Bool),
    (ConcreteCategory.hom (F.obj.map (if h : i = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
      (ConcreteCategory.hom (F.obj.map (if h : i = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t

Tactic:
rintro ⟨_ | _⟩
    any_goals exact h₁
    any_goals exact h₂

Goal state after:
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

Goal state after:
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
s : CC ((stalkFunctor C x).obj F)
⊢ ∀ ⦃a₂ : CC ((stalkFunctor C x).obj F)⦄,
    (ConcreteCategory.hom ((stalkFunctor C x).map α)) s = (ConcreteCategory.hom ((stalkFunctor C x).map α)) a₂ → s = a₂
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)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
⊢ s = t

Tactic:
by
  -- We use `germ_eq` and the axiom of choice, to pick for every point `x` a neighbourhood
  -- `V x`, such that the restrictions of `s` and `t` to `V x` coincide.
  choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x.1 x.2)
  -- Since `F` is a sheaf, we can prove the equality locally, if we can show that these
  -- neighborhoods form a cover of `U`.
  apply F.eq_of_locally_eq' V U i₁
  · intro x hxU
    simp only [Opens.mem_iSup]
    exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
  · intro x
    rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ (Set.univ.pi fun i ↦ ↑(s i)) ⊆ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
simp only [Set.subset_def, mem_closure_iff]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ ∀ x ∈ Set.univ.pi fun i ↦ ↑(s i),
    ∀ (o : Set ((i : ι) → M i)),
      IsOpen[Pi.topologicalSpace] o → x ∈ o → (o ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
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)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
obtain ⟨s, s_spec, -⟩ := F.existsUnique_gluing' V U iVU V_cover sf this

Goal state after:
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)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t
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)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
hι : U ⊔ V = iSup ι
⊢ (s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)) →
    { l //
      l ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
        l ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
            m ≫ (F.interUnionPullbackCone U V).fst = s.fst → m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = l }

Tactic:
intro s

Goal state after:
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)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ { l //
    l ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
      l ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
          m ≫ (F.interUnionPullbackCone U V).fst = s.fst → m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = l }
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
g : S →ₐ[R] R
⊢ IsEffective R S

Tactic:
intro s

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
⊢ (TensorProduct.includeLeftSubRight R S) s = 0 ↔ s ∈ Set.range ⇑(Algebra.linearMap R S)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
inst✝⁹ : Semiring S
S₁ : Type u_6
M : Type u_7
M₁ : Type u_8
inst✝⁸ : Semiring S₁
σ : S →+* S₁
σ' : S₁ →+* S
inst✝⁷ : RingHomInvPair σ σ'
inst✝⁶ : RingHomInvPair σ' σ
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module S₁ M₁
f : M ≃ₛₗ[σ] M₁
hf : IsHomeomorph ⇑f
⊢ ↑(ofIsHomeomorph f hf) = f

Tactic:
by
  dsimp only [ofIsHomeomorph]

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

Goal state before:
pp: R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
f : of (MvPolynomial ↑A ↑(⊥_ CommRingCat)) ⟶ A := ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
x : ↑A
⊢ (ConcreteCategory.hom f) (MvPolynomial.X x) = x

Tactic:
simp [f]

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
x : ↑B
⊢ (Hom.hom fB) (MvPolynomial.X x) = x

Tactic:
simp [PB, fB]

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

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ HasPullbacks (P.CostructuredArrow ⊤ L X)

Tactic:
by
  apply +allowSynthFailures hasLimitsOfShape_of_closedUnderLimitsOfShape
  · exact inferInstanceAs (HasLimitsOfShape WalkingCospan (CostructuredArrow L X))
  · exact CostructuredArrow.closedUnderLimitsOfShape_walkingCospan _ _

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
inst✝ : P.RespectsIso
⊢ CreatesColimitsOfShape (Discrete PEmpty.{1}) (Under.forget P ⊤ X)

Tactic:
apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed

Goal state after:
case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ HasColimitsOfShape (Discrete PEmpty.{1}) (Comma (Functor.fromPUnit X) (𝟭 T))

case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
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✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ CreatesColimitsOfShape WalkingSpan (Under.forget P ⊤ X)

Tactic:
apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed

Goal state after:
case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ HasColimitsOfShape WalkingSpan (Comma (Functor.fromPUnit X) (𝟭 T))

case inst
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ (commaObj (Functor.fromPUnit X) (𝟭 T) P).IsClosedUnderColimitsOfShape WalkingSpan
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ False

Tactic:
have h₃ : ¬ringChar R ∣ q := by
      rintro ⟨r, hr⟩
      rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
      nth_rw 1 [← mul_one (ringChar R)] at hq
      exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
⊢ False
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this✝¹ :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this✝ :
  PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ S)
⊢ PreservesLimit K (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
exact preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)

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

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

Tactic:
intro I

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
⊢ I ≠ ⊤ → CharZero (R ⧸ I)
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
intro I

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
⊢ I ≠ ⊤ → CharZero (R ⧸ I)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s' : Seq α
⊢ R nil s' → BisimO R nil.destruct s'.destruct → nil.head = s'.head ∧ R nil.tail s'.tail

Tactic:
cases s'

Goal state after:
case nil.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
⊢ R nil nil → BisimO R nil.destruct nil.destruct → nil.head = nil.head ∧ R nil.tail nil.tail

case nil.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
⊢ R nil (cons x✝ s✝) →
    BisimO R nil.destruct (cons x✝ s✝).destruct → nil.head = (cons x✝ s✝).head ∧ R nil.tail (cons x✝ s✝).tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s' : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝ s✝) s' →
    BisimO R (cons x✝ s✝).destruct s'.destruct → (cons x✝ s✝).head = s'.head ∧ R (cons x✝ s✝).tail s'.tail

Tactic:
cases s'

Goal state after:
case cons.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝ : α
s✝ : Seq α
⊢ R (cons x✝ s✝) nil →
    BisimO R (cons x✝ s✝).destruct nil.destruct → (cons x✝ s✝).head = nil.head ∧ R (cons x✝ s✝).tail nil.tail

case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝¹ s✝¹) (cons x✝ s✝) →
    BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct →
      (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s'.tail.val = s'.val.tail

Tactic:
cases s'

Goal state after:
case mk
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ (tail ⟨val✝, property✝⟩).val = ⟨val✝, property✝⟩.val.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ s.length ≤ n

Tactic:
apply Nat.find_min'

Goal state after:
case a.succ
α : Type u
s : Computation α
h : s.Terminates
n : ℕ
this : (s.think.val (n + 1)).isSome = true
⊢ (s.val n).isSome = true
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₂)
⊢ match
    match Bind.g (f a).destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    (f a).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = corec (Bind.f f) (Sum.inl (pure a)) ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False

Tactic:
rcases destruct (f a) 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₂)
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 = corec (Bind.f f) (Sum.inl (pure a)) ∧ 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₂)
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 = corec (Bind.f f) (Sum.inl (pure a)) ∧ 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
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct

Tactic:
intro s

Goal state after:
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = nil.append s ∧ s2 = s) (nil.append s).destruct s.destruct
Module: Mathlib.Data.Seq.Basic

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

Tactic:
intro s

Goal state after:
α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case none
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (none.bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    none = none ∨ ∃ ifp, none = some ifp ∧ ifp.fr = 0

Tactic:
simp [imp_false]

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

Goal state before:
pp: case some
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
val✝ : IntFractPair K
⊢ ((some val✝).bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    some val✝ = none ∨ ∃ ifp, some val✝ = some ifp ∧ ifp.fr = 0

Tactic:
simp [imp_false]

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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
rwa [h₁, ← terminatedAt_iff_s_none,
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]

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

Goal state before:
pp: case succ.zero
α : 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
x y : α
k : ℕ
hy : y ∈ tl.get? k
h_ij : 0 < k + 1
hx : hd = x
⊢ R x y

Tactic:
exact hx ▸ all_get h_hd hy

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

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

Tactic:
by
  cases n
  · simp
  · rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
    simp only [← add_assoc, add_tsub_cancel_right]
    ring

Goal state after: