mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n✝ : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I ^ n.succ).FG

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
⊢ f.hom ≫
      { pt := Over.mk (t₂.π.app star),
            π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.pt.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.homMk f.hom ⋯ ≫
      { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Over X
F : C ⥤ D
t : Cone K
t₁ t₂ : Cone (liftFromOver.obj K)
f : t₁ ⟶ t₂
j : J
⊢ Over.homMk f.hom ⋯ ≫
      { pt := Over.mk (t₂.π.app star), π := { app := fun a ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }.π.app
        j =
    { pt := Over.mk (t₁.π.app star), π := { app := fun a ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }.π.app j

Tactic:
by ext; simp [dsimp% f.w (of j)]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ t : Cocone K
x✝ : star ⟶ star
⊢ ((liftFromUnder.obj K).map x✝ ≫
      match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) =
    (match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      ((Functor.const (WithInitial J)).obj t.pt.right).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ t : Cocone K
b : J
x✝ : star ⟶ of b
⊢ ((liftFromUnder.obj K).map x✝ ≫
      match of b with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) =
    (match star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      ((Functor.const (WithInitial J)).obj t.pt.right).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ t : Cocone K
a b : J
f : of a ⟶ of b
⊢ ((liftFromUnder.obj K).map f ≫
      match of b with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) =
    (match of a with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      ((Functor.const (WithInitial J)).obj t.pt.right).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t t₁ t₂ : Cocone K
f : t₁ ⟶ t₂
⊢ { pt := t₁.pt.right,
              ι :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Under.Hom.right (t₁.ι.app a)
                    | star => t₁.pt.hom,
                  naturality := ⋯ } }.ι.app
        star ≫
      Under.Hom.right f.hom =
    { pt := t₂.pt.right,
            ι :=
              {
                app := fun x ↦
                  match x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } }.ι.app
      star

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t t₁ t₂ : Cocone K
f : t₁ ⟶ t₂
a : J
⊢ { pt := t₁.pt.right,
              ι :=
                {
                  app := fun x ↦
                    match x with
                    | of a => Under.Hom.right (t₁.ι.app a)
                    | star => t₁.pt.hom,
                  naturality := ⋯ } }.ι.app
        (of a) ≫
      Under.Hom.right f.hom =
    { pt := t₂.pt.right,
            ι :=
              {
                app := fun x ↦
                  match x with
                  | of a => Under.Hom.right (t₂.ι.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } }.ι.app
      (of a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯ =
    Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ { pt := Under.mk (t₁.ι.app star), ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j ≫
      Under.homMk f.hom ⋯ =
    { pt := Under.mk (t₂.ι.app star), ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Cone

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
X : C
K : J ⥤ Under X
F : C ⥤ D
t : Cocone K
t₁ t₂ : Cocone (liftFromUnder.obj K)
f : t₁ ⟶ t₂
j : J
⊢ { pt := Under.mk (t₁.ι.app star), ι := { app := fun a ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j ≫
      Under.homMk f.hom ⋯ =
    { pt := Under.mk (t₂.ι.app star), ι := { app := fun a ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } }.ι.app j

Tactic:
by ext; simp [dsimp% f.w (of j)]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
⊢ (aeval x) ((map (algebraMap R A)) p) = (aeval x) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((aeval x) p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : σ → ↥S
p : MvPolynomial σ R
⊢ (aeval fun i ↦ ↑(x i)) p = ↑((aeval x) p)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
α : Type u₂
F : J ⥤ Discrete α
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (liftToDiscrete F ⋙ Discrete.functor F.obj).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j : J
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((const J).obj ((IsPreconnected.IsoConstantAux.liftToDiscrete F).obj j) ⋙ Discrete.functor F.obj).map f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ ((const J).obj (F.obj j)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ F.obj j = F.obj j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
inst✝¹ : IsPreconnected J
inst✝ : IsPreconnected K
⊢ IsPreconnected (J × K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (Discrete.mk ∘ F) X✝ = (Discrete.mk ∘ F) Y✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
α✝ : Type u₁
F : J ⥤ Discrete α✝
j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ F.obj j₁✝ = F.obj j₂✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
⊢ j ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ j₁ ∈ {j | F j = F j₀} ↔ j₂ ∈ {j | F j = F j₀}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : ?j₀ ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
⊢ Classical.choice ⋯ ∈ p'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
⊢ IsConnected (ULiftHom (ULift.{u₂, u₁} J))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₁✝ ∈ {j | Nonempty (Z j)} → j₂✝ ∈ {j | Nonempty (Z j)}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
Z : J → Sort u_1
h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂
h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁
j₀ : J
x : Z j₀
j j₁✝ j₂✝ : J
f : j₁✝ ⟶ j₂✝
⊢ j₂✝ ∈ {j | Nonempty (Z j)} → j₁✝ ∈ {j | Nonempty (Z j)}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
e : J ≌ K
inst✝ : IsConnected J
⊢ Nonempty J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: X : Type u_1
a b : Discrete X
h : Zigzag a b
⊢ a.as = b.as

Tactic:
induction h with
  | refl => rfl
  | tail _ h eq => exact eq.trans (eq_of_zag _ h)

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: X : Type u_1
a b : Discrete X
h : Zigzag a b
⊢ a.as = b.as

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
⊢ ∀ (j₁ j₂ : J), r j₁ j₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsPreconnected J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsPreconnected J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (const J).obj X ⟶ (const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ α.app x✝¹ = α.app x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsConnected J
X✝ Y✝ : C
f : (const J).obj X✝ ⟶ (const J).obj Y✝
⊢ (const J).map (f.app (Classical.arbitrary J)) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: G : Type u_1
inst✝¹ : Groupoid G
inst✝ : IsPreconnected G
⊢ ∀ (x y : G), Nonempty (x ⟶ y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : Subsingleton J
α : Type u₁
F : J ⥤ Discrete α
j x : J
⊢ F.obj x = ((const J).obj (F.obj j)).obj x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: β : Type v
f : β → Type v
P : Type v
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ (ConcreteCategory.hom (Pi.π f b)) ((ConcreteCategory.hom (Pi.lift s)) x) = (ConcreteCategory.hom (s b)) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: β : Type v
f g : β → Type v
α : (j : β) → f j ⟶ g j
b : β
x : (fun X ↦ X) (∏ᶜ f)
⊢ (ConcreteCategory.hom (Pi.π g b)) ((ConcreteCategory.hom (Pi.map α)) x) =
    (ConcreteCategory.hom (α b)) ((ConcreteCategory.hom (Pi.π f b)) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: X : Type u
⊢ IsTerminal X ≃ (X ≅ PUnit.{u + 1})

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun x ↦ ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: ⊢ binaryProductFunctor ≅ prod.functor

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type (max v u)
x✝¹ : Cone (Discrete.functor F)
x✝ :
  x✝¹.pt ⟶
    { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun f ↦ f j }.pt
w :
  ∀ (j : Discrete J),
    x✝ ≫
        { pt := (j : J) → F j,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun f ↦ f j }.π.app
          j =
      x✝¹.π.app j
⊢ x✝ = ↾fun x j ↦ (ConcreteCategory.hom (x✝¹.π.app { as := j })) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type (max v u)
j : J
⊢ ((productIso F).hom ≫ ↾fun f ↦ f j) = Pi.π F j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type u
inst✝ : Small.{u, v} J
s : Cone (Discrete.functor F)
m :
  s.pt ⟶
    { pt := Shrink.{u, max u v} ((j : J) → F j),
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun f ↦ (equivShrink ((j : J) → F j)).symm f j }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        { pt := Shrink.{u, max u v} ((j : J) → F j),
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun f ↦ (equivShrink ((j : J) → F j)).symm f j }.π.app
          j =
      s.π.app j
x : s.pt
j : J
⊢ (equivShrink ((x : J) → F x)).symm ((ConcreteCategory.hom m) x) j =
    (equivShrink ((x : J) → F x)).symm
      ((ConcreteCategory.hom
          (↾fun x ↦ (equivShrink ((j : J) → F j)) fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x))
        x)
      j

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
⊢ FiniteType R A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
⊢ FiniteType R A ↔ FinitePresentation R A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).EssSurj ↔ Q ≤ P.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE ⋯).IsEquivalence

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ ∀ (X : C), ⊤ ((𝟭 C).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ ∀ (X : ⊤.FullSubcategory),
    ⊤.ι.map ((Iso.refl (𝟭 ⊤.FullSubcategory)).hom.app X) ≫ (Iso.refl (⊤.lift (𝟭 C) ⋯ ⋙ ⊤.ι)).hom.app (⊤.ι.obj X) =
      𝟙 (⊤.ι.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : P.FullSubcategory
X : C
hX : P X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX })

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : P.FullSubcategory
X : C
hX : P X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX })

Tactic:
by rwa [← h] at hX

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ P ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f)

pp: case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG

Tactic:
· rw [AlgHom.coe_comp]
    exact Function.Surjective.comp e.surjective hf.1

Goal state after:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
this : RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty Cᵒᵖ
inst✝ : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.unop

Tactic:
by

Goal state after: