mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = fg

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (λ_ (F.map f)).hom = ((F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv) ≫ (F.map₂Iso (λ_ f)).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (λ_ (F.map f)).hom = ((F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv) ≫ (F.map₂Iso (λ_ f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (λ_ f).inv = (λ_ (F.map f)).inv ≫ (F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv

Tactic:
rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (λ_ (F.map f)).hom = ((F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv) ≫ (F.map₂Iso (λ_ f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (ρ_ (F.map f)).hom = (F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv) ≫ (F.map₂Iso (ρ_ f)).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (ρ_ (F.map f)).hom = (F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv) ≫ (F.map₂Iso (ρ_ f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (ρ_ f).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv

Tactic:
rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (ρ_ (F.map f)).hom = (F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv) ≫ (F.map₂Iso (ρ_ f)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵖ C
a b✝ b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = 𝟙 b

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵖ C
a b b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = fg

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.map₂ (f ◁ η)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.map₂ (η ▷ h)

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
h : P.op = Q.op
⊢ Q.op.unop = Q.op.unop

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty Cᵒᵖ
h : P.unop = Q.unop
⊢ Q.unop.op = Q.unop.op

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : X i = unop Z
⊢ op (unop Z) = Z

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ X i = unop (op (X i))

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure = P.isoClosure

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv

Tactic:
rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.mapComp f g ≫ F.map f ◁ F.map₂ η = F.mapComp f g ≫ F.map f ◁ F.map₂ η

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
    (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
    (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.map₂ (f ◁ η)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.map₂ (η ▷ h)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)

Tactic:
]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)

Tactic:
]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)

Tactic:
]

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ (Ideal.map f I).FG

Tactic:
obtain ⟨s, hs⟩ := h

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ (Ideal.map f I).FG
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ Ideal.map f I = Ideal.map f I

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ x ^ n ∈ ↑I

Tactic:
]

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ x ^ n ∈ ↑I
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I

Tactic:
]

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (Submodule.span R ↑(s • t)).FG

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (Submodule.span R ↑(s • t)).FG
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
⊢ ⊤.FG

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ ⊤.FG
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 * I ^ n).FG

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n✝ : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I * I ^ n).FG
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
⊢ eval₂ ((algebraMap A B).comp (algebraMap R A)) x p = eval₂ ((algebraMap A B).comp (algebraMap R A)) x p

Tactic:
]

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
⊢ (eval₂Hom (algebraMap R B) fun x_1 ↦ (algebraMap A B) (x x_1)) p =
    (eval₂Hom (algebraMap R B) fun i ↦ (algebraMap A B) (x i)) p

Tactic:
]

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 x) p = 0 ↔ (aeval x) p = 0

Tactic:
]

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 x) p = 0 ↔ (aeval x) p = 0

Tactic:
]

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
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f ↦ congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j₀ ∈ p

Tactic:
]

Goal state after:
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
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f ↦ congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j₀ ∈ p
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₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
j j' : J
⊢ F j₀ = F j₀

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j b✝
hj : Zag b✝ c✝
ih : F j = F b✝
⊢ F b✝ = F c✝

Tactic:
]

Goal state after:
case tail
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j b✝
hj : Zag b✝ c✝
ih : F j = F b✝
⊢ F b✝ = F c✝
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:
simp [Subsingleton.allEq x j]

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 ↔ (ιOfLE h).EssSurj

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).IsEquivalence ↔ (ιOfLE h).EssSurj
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ P.isoClosure

Tactic:
]

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
hX : Q.inverseImage e.functor X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX✝ })

Tactic:
]

Goal state after:
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
hX : Q.inverseImage e.functor X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX✝ })
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
⊢ Q.inverseImage e.functor ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })

Tactic:
]

Goal state after:
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
⊢ Q.inverseImage e.functor ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })
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 ∘ ⇑f)

Tactic:
]

Goal state after:
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 ∘ ⇑f)
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 f.toRingHom).FG

Tactic:
]

Goal state after:
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 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
h : ((↑e).comp f).toRingHom = (↑e).comp f.toRingHom
h1 : ↑e.toRingEquiv = (↑e).toRingHom
⊢ (↑e).comp f.toRingHom = (↑e).comp f.toRingHom

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
]

Goal state after: