mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
⊢ { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.copy
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
      ⋯
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm
      ⋯
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source
      ⋯
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
      ⋯ =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ⇑e.toEquiv.symm = codRestrict (e.target.domRestrict e.invFun) e.source ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)

Tactic:
by
  rw [← image_source_eq_target, exists_mem_image]

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Defs

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialEquiv✝ : PartialEquiv X Y
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
⊢ { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
          continuousOn_invFun := continuousOn_invFun✝ }.replacePartialEquiv
      { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
          continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
      continuousOn_invFun := continuousOn_invFun✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialHomeomorph✝ : PartialHomeomorph X Y
open_source✝ : IsOpen[inst✝¹] toPartialHomeomorph✝.source
open_target✝ : IsOpen[inst✝] toPartialHomeomorph✝.target
⊢ { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
          open_target := open_target✝ }.replacePartialEquiv
      { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
          open_target := open_target✝ }.toPartialEquiv
      ⋯ =
    { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝, open_target := open_target✝ }

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
f1 : α → Set α := fun a ↦ Ioi a
f2 : α → Set α := fun a ↦ Iio a
s : Set α
hs : s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
⊢ s ∈ range f1 ∪ range f2

Tactic:
grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}

Tactic:
rfl

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'

Tactic:
refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ ↑e.symm x = ↑e'.symm x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case a
α : Type u
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s | ∃ a, s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : Set α → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ t ⊆ {s | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}

Tactic:
grind

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
x✝ : Set α
⊢ x✝ ∈ k ↔ x✝ ∈ kl ∪ kr

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑G
⊢ (Hom.hom (factorThruImage f ≫ ι f)) x✝ = (Hom.hom f) x✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ ↑(x + y) = ↑x + ↑y

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ ↑x = (Hom.hom (ι f)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
x✝¹ : CharacterModule C
x✝ : A
⊢ ((dual (g ∘ₗ f)) x✝¹) x✝ = ((dual f ∘ₗ dual g) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = (↑(if addOrderOf a = 0 then 2 else addOrderOf a))⁻¹.den
⊢ 0 < if addOrderOf a = 0 then 2 else addOrderOf a

Tactic:
grind

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst✝³] (Ioc (z x) x)

Tactic:
rw [H]; exact isOpen_Ioo

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : AddCircle p
x_ne_a : x ≠ ↑a
x_eq_b : x = ↑↑((equivIco p a) x)
⊢ ↑((equivIco p a) x) ∈ Ioc a (a + p)

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑((a % ↑n) • p / ↑n)

Tactic:
← Int.cast_natCast,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p) + ↑((a % ↑n) • p / ↑n)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
⊢ (∀ (x : ℤ), ¬x = 0 → ∀ (x_1 : ℤ), ¬p * ↑x_1 = a * ↑x) ↔ ∀ (a_1 b : ℤ), ¬b = 0 → ¬p * ↑a_1 = a * ↑b

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
· obtain ⟨m, hmn, hg, he⟩ := (addOrderOf_eq_pos_iff hn).mp u.2
          exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
x✝ :
  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⊗
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ Multiplicative.toAdd ((ConcreteCategory.hom μ) x✝) =
    (Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)))
        (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2) +
      (Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)))
        (Multiplicative.toAdd x✝.1, Multiplicative.toAdd x✝.2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
x : ↑(of R ↥N)
⊢ (Hom.hom (underlyingIso (↟N.subtype)).inv) x = (Hom.hom (↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
x : ↑(underlying.obj S)
⊢ (Hom.hom
        ((LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯)
                ⋯).toModuleIso.hom ≫
          ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype))
      x =
    (Hom.hom S.arrow) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : HopfAlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : HopfAlgCat R
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ x✝¹)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).inv ≫
          (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ X₂✝)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((Iso.refl
              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝² ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹) ≫
            (Iso.refl
                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom))
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝⁵ x✝⁴ x✝³ : HopfAlgCat R
x✝² : x✝⁵.carrier
x✝¹ : x✝⁴.carrier
x✝ : x✝³.carrier
⊢ ((((TensorProduct.mk R x✝⁵.carrier x✝⁴.carrier).compr₂ₛₗ
            ((TensorProduct.mk R (x✝⁵ ⊗ x✝⁴).carrier x✝³.carrier).compr₂ₛₗ
              ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (α_ x✝⁵ x✝⁴ x✝³).hom).toBialgHom')))
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.mk R x✝⁵.carrier x✝⁴.carrier).compr₂ₛₗ
            ((TensorProduct.mk R (x✝⁵ ⊗ x✝⁴).carrier x✝³.carrier).compr₂ₛₗ
              ((fun x ↦ ↑x)
                (((Iso.refl
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁵ ⊗ x✝⁴) ⊗
                              (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)).symm ≪≫
                        ((Iso.refl
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵ ⊗
                                (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴)).symm ⊗ᵢ
                          Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³))) ≪≫
                      α_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴)
                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³) ≪≫
                        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵) ⊗ᵢ
                            Iso.refl
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗
                                (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)) ≪≫
                          Iso.refl
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵ ⊗
                              (forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³))).hom.toBialgHom')))
          x✝²)
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝¹).hom).toBialgHom'))
        1)
      x✝ =
    (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        1)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝¹).hom).toBialgHom'))
        x✝)
      1 =
    (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
                  ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        x✝)
      1

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
intro _ A a

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
a✝ : Epi f
A : C
a : A ⟶ Y
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ a = x ≫ f
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
suffices S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
      S.liftCycles (x₂ - x₂') (by simp [hx₂, hx₂']) ≫ S.homologyπ = 0 by
    simp [this, S.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements,
      sub_eq_iff_eq_add']

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔ S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ = 0
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
z₂ : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = x₁ ≫ S.toCycles

Tactic:
obtain ⟨x₂, hx₂, rfl⟩ : ∃ (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0), z₂ = S.liftCycles x₂ hx₂ :=
    ⟨z₂ ≫ S.iCycles, by simp, by simp [← cancel_mono S.iCycles, liftCycles_i]⟩
  simp [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, ← cancel_mono S.iCycles]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A : C
a : A ⟶ S.L₁.X₂
b : A ⟶ S.L₀.X₃
h : a ≫ S.L₁.g = b ≫ S.v₀₁.τ₃
⊢ pullback.lift a b h ≫ S.φ₂ = a ≫ S.v₁₂.τ₂

Tactic:
by
  simp [φ₂]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.L₁'.Exact

Tactic:
exact S.op.L₁'_exact

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
⊢ x = y

Tactic:
apply ConcreteCategory.injective_of_mono_of_preservesPullback (PreservesProduct.iso F f).hom
  apply Concrete.limit_ext _ (piComparison F _ x) (piComparison F _ y)
  intro ⟨j⟩
  rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, piComparison_comp_π]
  exact h j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left.left.id
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
a : J.L
⊢ (hom (𝟙 ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left a)))) (↑x a) = ↑x a

Tactic:
rfl

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

Goal state before:
pp: case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
a₁✝ a₂✝ : X₁
h : (hom t) a₁✝ = (hom t) a₂✝ ∧ (hom l) a₁✝ = (hom l) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: case left.right.fst
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.fst b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

Tactic:
rfl

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

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
x : PullbackObj r b
⊢ (hom r) (↑x).1 = (hom b) (↑x).2

Tactic:
grind

Goal state after: