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

Goal state before:
pp: case h₀
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)
a✝ : ⊤.arrows f
⊢ 𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.fst (E.f i) (E.f j) =
    (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit) ≫ pullback.fst (E.f i) (E.f j)

Tactic:
simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: case h₁
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)
a✝ : ⊤.arrows f
⊢ 𝟙 (pullback (E.f i) (E.f j)) ≫ pullback.snd (E.f i) (E.f j) =
    (eqToHom ⋯ ≫ E.toPreOneHypercover.toPullback PUnit.unit) ≫ pullback.snd (E.f i) (E.f j)

Tactic:
simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
x✝ : (E.refineOneHypercover F).I₁ i j
⊢ (E.refineOneHypercover F).toPullback x✝ ≫
      pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j) =
    (F i j).f x✝ ≫ pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)

Tactic:
simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
x✝ : (E.refineOneHypercover F).I₁ i j
⊢ (E.refineOneHypercover F).toPullback x✝ ≫
      pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j) =
    (F i j).f x✝ ≫ pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)

Tactic:
simp [PreOneHypercover.toPullback]

Goal state after:
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 ι
g : ι → Opens ↑X
⊢ Set.InjOn (fun a ↦ (ConcreteCategory.hom f) a) (⋃ i, ↑(g i))

Tactic:
exact hf.injective.injOn

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
refine ⟨fun h U ↦ h.isSheafPreservesLimitPairwiseIntersections,
    fun h ↦ F.isSheaf_iff_isSheafPairwiseIntersections.mpr fun ι U ↦ ?_⟩
  have := h U
  exact ⟨isLimitOfPreserves _ (Pairwise.coconeIsColimit U).op⟩

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

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
α✝ β✝ : Type u_2
a✝¹ : α✝ ≃ β✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : β✝ → Type u_3
inst✝³ : (i : β✝) → AddCommMonoid (A i)
inst✝² : (i : β✝) → Module R (A i)
inst✝¹ : (i : β✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : β✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : β✝) → A i)

pp: case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
· -- invariance under equivalence of the finite type we're taking the product over
    case of_equiv X Y e _ _ _ _ _ =>
    exact .iso (ContinuousLinearEquiv.piCongrLeft R A e)

Goal state after:
case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)
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.IsInvertible
⊢ Function.Bijective ⇑f

Tactic:
rcases hf with ⟨e, rfl⟩
  simp [ContinuousLinearEquiv.bijective]

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ ((const J).obj (F.obj i₀)).map φ ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
dsimp
        rw [id_comp]
        let i := IsCofiltered.min i₀ j
        let α : i ⟶ i₀ := IsCofiltered.minToLeft _ _
        let β : i ⟶ j := IsCofiltered.minToRight _ _
        rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]

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

Goal state before:
pp: case refine_1.hC
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := ⋯
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
⊢ ∀ (r : ↑R),
    (CommRingCat.Hom.hom (π ≫ g)) (MvPolynomial.C r) =
      (CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x_1 ↦
                (ConcreteCategory.hom (F.map (hi x_1))) (x x_1)) ≫
            c.ι.app i))
        (MvPolynomial.C r)

Tactic:
simpa using! fun x ↦ congr($(hg i).hom x)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ ∀ (j : Discrete WalkingPair), Over.homMk m ⋯ ≫ c.π.app j = (pullbackConeEquivBinaryFan.functor.obj s).π.app j

Tactic:
rintro (_ | _) <;> ext

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.left })

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Over.Hom.left (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right }) =
    Over.Hom.left ((pullbackConeEquivBinaryFan.functor.obj s).π.app { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ ∀ (j : Discrete WalkingPair), c.ι.app j ≫ Under.homMk m ⋯ = (pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app j

Tactic:
rintro (_ | _) <;> ext

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.left } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.left })

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ Under.Hom.right (c.ι.app { as := WalkingPair.right } ≫ Under.homMk m ⋯) =
    Under.Hom.right ((pushoutCoconeEquivBinaryCofan.functor.obj s).ι.app { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none.none.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        none = a →
          none = a_1 →
            WidePullbackShape.Hom.id none ≍ x →
              (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
        (fun X h ↦
          Eq.rec (motive := fun x x_1 ↦
            none = x →
              WidePullbackShape.Hom.id none ≍ 𝟙 x →
                (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
            (fun h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : none ⟶ x) →
                  f ≍ 𝟙 none →
                    (Option.rec B (fun val ↦ (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) none)) ⋯
                (WidePullbackShape.Hom.id none))
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ none) →
              none = none →
                f ≍ WidePullbackShape.Hom.term j →
                  (Option.rec B (fun val ↦ (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val ↦ (F.obj { as := val }).left) none))
            (fun f h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some j ⟶ x) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id none))
        (WidePullbackShape.Hom.id none) ⋯ ⋯ ⋯

Tactic:
rw [Category.id_comp, Category.comp_id]

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

Goal state before:
pp: case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝ = a →
          some val✝ = a_1 →
            WidePullbackShape.Hom.id (some val✝) ≍ x →
              (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
        (fun X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              WidePullbackShape.Hom.id (some val✝) ≍ 𝟙 x →
                (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some val✝ ⟶ x) →
                  f ≍ 𝟙 (some val✝) →
                    (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝))) ⋯
                (WidePullbackShape.Hom.id (some val✝)))
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                f ≍ WidePullbackShape.Hom.term j →
                  (Option.rec B (fun val ↦ (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun f h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some j ⟶ x) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id (some val✝)))
        (WidePullbackShape.Hom.id (some val✝)) ⋯ ⋯ ⋯

Tactic:
rw [Category.id_comp, Category.comp_id]

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

Goal state before:
pp: ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ ↑x = 0

Tactic:
← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x,

Goal state after:
ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ (Pi.evalRingHom (fun x ↦ R) i) ↑x = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case intro.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hp : CharP (R ⧸ I) 0
⊢ CharP (R ⧸ I) 0

Tactic:
exact hp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_charP : CharP R p
h : ¬p = 0
⊢ P

Tactic:
· exact h_pos p h p_charP

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

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

Tactic:
simp [think, Stream'.cons] at this

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = s.length' + 1

Tactic:
by
  by_cases h : (cons x s).Terminates <;> have h' := h <;> rw [terminates_cons_iff] at h'
  · simp [length'_of_terminates h, length'_of_terminates h', length_cons h']
  · simp [length'_of_not_terminates h, length'_of_not_terminates h']

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

Goal state before:
pp: case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
have := IH this

Goal state after:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.convs' m = g.convs' n

Tactic:
simp only [convs', convs'Aux_stable_of_terminated n_le_m terminatedAt_n]

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

Goal state before:
pp: case succ
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop (k + 1)).get? m = s.get? (k + 1 + m)

Tactic:
simp only [drop, get?_tail]

Goal state after:
case succ
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop k).get? (m + 1) = s.get? (k + 1 + m)
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
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
hix : (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) x = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
by
  have := Nonempty.intro i
  apply_fun ringEquiv _ _ at hix
  rwa [map_zero, ringEquiv_of, DirectLimit.exists_eq_zero] at hix

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

Goal state before:
pp: α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
⊢ b.length' ≤ a.length'

Tactic:
by
  have (n) (hb : b.drop n ≠ .nil) : motive (a.drop n) (b.drop n) := by
    induction n with
    | zero => simpa
    | succ m ih =>
      simp only [drop] at hb ⊢
      generalize b.drop m = tb at *
      cases tb with
      | nil => simp at hb
      | cons tb_hd tb_tl =>
        simp only [ne_eq, cons_ne_nil, not_false_eq_true, forall_const] at ih
        obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl
        simpa [ha]
  by_cases ha : a.Terminates; swap
  · simp [length'_of_not_terminates ha]
  simp only [length'_of_terminates ha, length'_le_iff]
  by_contra hb
  have hb_cons : b.drop (a.length ha) ≠ .nil := by
    intro hb'
    simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'
    contradiction
  specialize this (a.length ha) hb_cons
  generalize b.drop (a.length ha) = b' at *
  cases b' with
  | nil =>
    contradiction
  | cons b_hd b_tl =>
    obtain ⟨a_hd, a_tl, ha', _⟩ := step _ _ this _ _ rfl
    apply_fun length' at ha'
    simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'
    generalize a_tl.length' = u at ha'
    enat_to_nat
    lia

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

Goal state before:
pp: n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ fib (n + 2 + 1) = ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2

Tactic:
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
    simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x✝ : M
⊢ x✝ ∈ (f.genEigenspace μ) 0 ↔ x✝ ∈ ⊥

Tactic:
apply mem_genEigenspace_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
unfold HasUnifEigenvalue at *

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) k ≠ ⊥
⊢ (f.genEigenspace μ) m ≠ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
eq_bot_iff

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective ⇑(f - μ • 1)
⊢ (f.genEigenspace μ) k ≤ ⊥
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
⊢ (toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f =
    Matrix.blockDiagonal' fun i ↦ (toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)

Tactic:
by
  ext ⟨i, _⟩ ⟨j, _⟩
  simp only [toMatrix_apply, Matrix.blockDiagonal'_apply]
  rcases eq_or_ne i j with rfl | hij
  · simp [h₂.collectedBasis_repr_of_mem _ (hf _ (Subtype.mem _)), restrict_apply]
  · simp [hij, h₂.collectedBasis_repr_of_mem_ne _ hij.symm (hf _ (Subtype.mem _))]

Goal state after: