awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
⊢ MonCat.units.IsRightAdjoint

Tactic:
⟨_, ⟨GrpCat.forget₂MonAdj⟩⟩

Premises used: Nonempty.intro, Exists.intro, GrpCat.forget₂MonAdj, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : CommGrpCat
Y : CommMonCat
f :
  Functor.obj
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
        CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
      X ⟶
    Y
⊢ Eq (α := X ⟶ CommMonCat.units.obj Y)
    (({
            toFun :=
              fun
                (f :
                  Functor.obj
                      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := CommMonCat.carrier))
                      X ⟶
                    Y) ↦
              ofHom (CommMonCat.Hom.hom f).toHomUnits,
            invFun := fun (f : X ⟶ CommMonCat.units.obj Y) ↦
              CommMonCat.ofHom (MonoidHom.comp (Units.coeHom (↑Y : Type u)) (Hom.hom f)),
            left_inv := ⋯, right_inv := ⋯ :
            (Functor.obj
                  (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                    CommMonCat.carrier))
                  X ⟶
                Y) ≃
              (X ⟶ CommMonCat.units.obj Y) } :
          (a : (forget₂ CommGrpCat CommMonCat).obj X ⟶ Y) → X ⟶ CommMonCat.units.obj Y)
        f :
      X ⟶ CommMonCat.units.obj Y)
    (NatTrans.app { app := fun (X : CommGrpCat.{u}) ↦ ofHom (MulEquiv.toMonoidHom toUnits), naturality := ⋯ } X ≫
        CommMonCat.units.map f :
      Functor.obj (𝟭 CommGrpCat) X ⟶ CommMonCat.units.obj Y)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : CommGrpCat
Y : CommMonCat
g : X ⟶ CommMonCat.units.obj Y
⊢ Eq (α :=
    Functor.obj
        (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        X ⟶
      Y)
    (({
              toFun :=
                fun
                  (f :
                    Functor.obj
                        (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦
                          (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
                        X ⟶
                      Y) ↦
                ofHom (CommMonCat.Hom.hom f).toHomUnits,
              invFun := fun (f : X ⟶ CommMonCat.units.obj Y) ↦
                CommMonCat.ofHom (MonoidHom.comp (Units.coeHom (↑Y : Type u)) (Hom.hom f)),
              left_inv := ⋯, right_inv := ⋯ :
              (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                      CommMonCat.carrier))
                    X ⟶
                  Y) ≃
                (X ⟶ CommMonCat.units.obj Y) }.symm :
          (a : X ⟶ CommMonCat.units.obj Y) → (forget₂ CommGrpCat CommMonCat).obj X ⟶ Y)
        g :
      Functor.obj
          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
            CommMonCat.carrier))
          X ⟶
        Y)
    (CategoryTheory.Functor.map
          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
            CommMonCat.carrier))
          g ≫
        NatTrans.app
          { app := fun (X : CommMonCat.{u}) ↦ CommMonCat.ofHom (Units.coeHom (↑X : Type u)), naturality := ⋯ } Y :
      Functor.obj
          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
            CommMonCat.carrier))
          X ⟶
        Functor.obj (𝟭 CommMonCat) Y)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
⊢ CommMonCat.units.IsRightAdjoint

Tactic:
⟨_, ⟨CommGrpCat.forget₂CommMonAdj⟩⟩

Premises used: CommGrpCat.forget₂CommMonAdj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Basic
Goal:
K : Type u_1
β : Type u_2
inst : Coe K β
b : ℤ
fr : K
⊢ Eq.{u_2 + 1} (α := IntFractPair β) (↑{ b := b, fr := fr : IntFractPair K } : IntFractPair β)
    { b := b, fr := Coe.coe fr }

Tactic:
rfl

Premises used: GenContFract.IntFractPair.coeFn, GenContFract.IntFractPair.mapFr, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
hyp : IntFractPair.stream v n = none
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
simp [IntFractPair.stream, hyp]

Premises used: GenContFract.IntFractPair.stream
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ countP' p 1 = 0

Tactic:
rfl

Premises used: List.countP.go, FreeMonoid.countP', rfl
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l₁ l₂ : FreeMonoid α
dsimp :
  List.countP (fun (b : α) ↦ decide (p b))
      (HAppend.hAppend (α := List α) (β := List α) ((toList : (a : FreeMonoid α) → List α) l₁ : List α)
        ((toList : (a : FreeMonoid α) → List α) l₂ : List α)) =
    List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₁) +
      List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₂)
⊢ countP' p (l₁ * l₂) = countP' p l₁ + countP' p l₂

Tactic:
dsimp [countP']

Premises used: FreeMonoid.countP'
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ List.countP (fun (b : α) ↦ decide (p b))
      (HAppend.hAppend (α := List α) (β := List α) ((toList : (a : FreeMonoid α) → List α) l₁ : List α)
        ((toList : (a : FreeMonoid α) → List α) l₂ : List α)) =
    List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₁) +
      List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₂)

Tactic:
simp only [List.countP_append]

Premises used: List.countP_append
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ Eq (α := Multiplicative ℕ) (((⇑Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) ∘ countP' p) 1) 1

Tactic:
simp [countP'_one p]

Premises used: FreeMonoid.countP'_one
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x y : FreeMonoid α
⊢ ((⇑Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) ∘ countP' p) (x * y) =
    HMul.hMul (α := Multiplicative ℕ) (((⇑Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) ∘ countP' p) x)
      (((⇑Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) ∘ countP' p) y)

Tactic:
simp [countP'_mul p]

Premises used: FreeMonoid.countP'_mul
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : FreeMonoid α
⊢ Eq (α := Multiplicative ℕ) ((countP p : (a : FreeMonoid α) → Multiplicative ℕ) l : Multiplicative ℕ)
    ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ)
        (List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l)) :
      Multiplicative ℕ)

Tactic:
rfl

Premises used: FreeMonoid.countP', rfl
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
rw :
  Eq (α := Multiplicative ℕ)
    (if decide (p x) = true then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)
    (if p x then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)
⊢ Eq (α := Multiplicative ℕ) ((countP p : (a : FreeMonoid α) → Multiplicative ℕ) (of x) : Multiplicative ℕ)
    (if p x then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)

Tactic:
rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]

Premises used: apply_ite, FreeMonoid.toList_of, List.countP_singleton, Multiplicative.ofAdd, FreeMonoid.countP_apply, DFunLike.coe
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
⊢ Eq (α := Multiplicative ℕ)
    (if decide (p x) = true then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)
    (if p x then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)

Tactic:
simp only [decide_eq_true_eq]

Premises used: decide_eq_true_eq
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : FreeAddMonoid α
⊢ Eq (α := Multiplicative ℕ) ((count x : (a : FreeMonoid α) → Multiplicative ℕ) l : Multiplicative ℕ)
    ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ)
        (List.count x ((FreeAddMonoid.toList : (a : FreeAddMonoid α) → List α) l)) :
      Multiplicative ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ Eq (α := Multiplicative ℕ) ((count x : (a : FreeMonoid α) → Multiplicative ℕ) (of y) : Multiplicative ℕ)
    (Pi.mulSingle (M := fun (x : α) ↦ Multiplicative ℕ) x
        ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ) y :
      Multiplicative ℕ)

Tactic:
simp [count, countP_of, Pi.mulSingle_apply]

Premises used: FreeMonoid.countP_of, Pi.mulSingle_apply, FreeMonoid.count
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : FreeAddMonoid α
⊢ (countP p : (a : FreeAddMonoid α) → ℕ) l =
    List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeAddMonoid α) → List α) l)

Tactic:
rfl

Premises used: FreeAddMonoid.countP', rfl
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
rw : Eq (α := ℕ) (if decide (p x) = true then 1 else 0) (if p x then 1 else 0)
⊢ Eq (α := ℕ) ((countP p : (a : FreeAddMonoid α) → ℕ) (of x) : ℕ) (if p x then 1 else 0 : ℕ)

Tactic:
rw [countP_apply, toList_of, List.countP_singleton]

Premises used: FreeAddMonoid.toList_of, List.countP_singleton, FreeAddMonoid.countP_apply
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
⊢ Eq (α := ℕ) (if decide (p x) = true then 1 else 0) (if p x then 1 else 0)

Tactic:
simp only [decide_eq_true_eq]

Premises used: decide_eq_true_eq
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
rw : Eq (α := ℕ) (if y = x then 1 else 0 : ℕ) (Pi.single (M := fun (a : α) ↦ ℕ) x 1 y : ℕ)
⊢ Eq (α := ℕ) ((countP fun (x_1 : α) ↦ x_1 = x : (a : FreeAddMonoid α) → ℕ) (of y) : ℕ)
    (Pi.single (M := fun (a : α) ↦ ℕ) x 1 y : ℕ)

Tactic:
rw [countP_of]

Premises used: FreeAddMonoid.countP_of
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ Eq (α := ℕ) (if y = x then 1 else 0 : ℕ) (Pi.single (M := fun (a : α) ↦ ℕ) x 1 y : ℕ)

Tactic:
simp [Pi.single, Function.update]

Premises used: Function.update, Pi.single
-- Module: Mathlib.Algebra.FreeMonoid.Count
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : FreeAddMonoid α
⊢ (count x : (a : FreeAddMonoid α) → ℕ) l = List.count x ((toList : (a : FreeAddMonoid α) → List α) l)

Tactic:
rfl

Premises used: FreeAddMonoid.countP', rfl
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x : M₀
rw : 0 * x = x * 0
rw₁ : 0 = x * 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ Commute 0 x

Tactic:
rw [commute_iff_eq, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, commute_iff_eq, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = 0 * x * x_1
rw₁ : 0 = 0 * x_1
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ 0 * (x * x_1) = 0 * x * x_1

Tactic:
rw [zero_mul, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = x * (x_1 * 0)
rw₁ : 0 = x * 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := M₀) 0 0
⊢ x * x_1 * 0 = x * (x_1 * 0)

Tactic:
rw [mul_zero, mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
s : Set M₀
⊢ 0 ∈ s.centralizer

Tactic:
simp [mem_centralizer_iff]

Premises used: Set.mem_centralizer_iff
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
simp_rw : ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * (↑x : G₀) = (↑x : G₀) * g
⊢ Subset (α := Set G₀ˣ) (center G₀ˣ) (Units.val ⁻¹' center G₀)

Tactic:
simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]

Premises used: Set.subset_def, Semigroup.mem_center_iff, Set.mem_preimage
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
inl : 0 * (↑u : G₀) = (↑u : G₀) * 0
inr : ∀ (ha : a ≠ 0), a * (↑u : G₀) = (↑u : G₀) * a
⊢ a * (↑u : G₀) = (↑u : G₀) * a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
inl : 0 = (↑u : G₀) * 0
inl₁ inl₂ : Eq.{u_2 + 1} (α := G₀) 0 0
⊢ 0 * (↑u : G₀) = (↑u : G₀) * 0

Tactic:
rw [zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * (↑u : G₀) = (↑u : G₀) * a

Tactic:
congr_arg Units.val <| hu <| Units.mk0 a ha

Premises used: Units.val, Units.mk0, congr_arg
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * (↑u : G₀) = (↑u : G₀) * a

Tactic:
exact congr_arg Units.val <| hu <| Units.mk0 a ha

Premises used: Units.val, Units.mk0, congr_arg
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ Eq (α := Set G₀ˣ) (center G₀ˣ) (Units.val ⁻¹' center G₀)

Tactic:
center_units_subset.antisymm subset_center_units

Premises used: Set.center_units_subset, HasSubset.Subset.antisymm, Set.subset_center_units
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
inl : ∀ (ha : 0 ∈ s.centralizer), 0⁻¹ ∈ s.centralizer
inr : ∀ (ha₀ : a ≠ 0), a⁻¹ ∈ s.centralizer
⊢ a⁻¹ ∈ s.centralizer

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
ha inl : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

Tactic:
rw [inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer

Tactic:
zero_mem_centralizer

Premises used: Set.zero_mem_centralizer
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer

Tactic:
exact zero_mem_centralizer

Premises used: Set.zero_mem_centralizer
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
inr : c = a⁻¹ * c * a
inr₁ : c = a⁻¹ * (c * a)
inr₂ : a * c = c * a
inr₃ inr₄ : a * c = a * c
⊢ c * a⁻¹ = a⁻¹ * c

Tactic:
rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]

Premises used: mul_assoc, eq_inv_mul_iff_mul_eq₀, mul_inv_eq_iff_eq_mul₀
-- Module: Mathlib.Algebra.GroupWithZero.Center
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a b : G₀
ha : a ∈ s.centralizer
hb : b ∈ s.centralizer
⊢ a / b ∈ s.centralizer

Tactic:
simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer₀ hb)

Premises used: Set.inv_mem_centralizer₀, div_eq_mul_inv, Set.mul_mem_centralizer
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : MulZeroClass α
inst_2 : MulZeroClass β
inst_3 : MulEquivClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (0 * EquivLike.inv f 0) : β)
rw₁ rw₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) 0 : β)
⊢ (f : (a : α) → β) 0 =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (EquivLike.inv f 0) : β)

Tactic:
rw [← map_mul, zero_mul]

Premises used: MulEquivClass.map_mul, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : MulZeroClass α
inst_2 : MulZeroClass β
inst_3 : MulEquivClass F α β
f : F
⊢ HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (EquivLike.inv f 0) : β) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : MulZeroOneClass α
inst_2 : MulZeroOneClass β
inst_3 : MulEquivClass F α β
⊢ MonoidWithZeroHomClass F α β

Tactic:
{ MulEquivClass.instMonoidHomClass F, MulEquivClass.toZeroHomClass with }

Premises used: MonoidWithZeroHomClass.mk, MulEquivClass.instMonoidHomClass, MulEquivClass.toZeroHomClass
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G ≃* H
x : G
⊢ Eq.{u_2 + 1} (α := H) ((f.toMonoidWithZeroHom : (a : G) → H) x : H) ((f : (a : G) → H) x : H)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G ≃* H
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f.toMonoidWithZeroHom : (a : G) → H)

Tactic:
f.injective

Premises used: MulEquiv.injective
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G ≃* H
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f.toMonoidWithZeroHom : (a : G) → H)

Tactic:
f.surjective

Premises used: MulEquiv.surjective
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f : G ≃* H
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f.toMonoidWithZeroHom : (a : G) → H)

Tactic:
f.bijective

Premises used: MulEquiv.bijective
-- Module: Mathlib.Algebra.GroupWithZero.Equiv
Goal:
G : Type u_1
H : Type u_2
inst : MulZeroOneClass G
inst_1 : MulZeroOneClass H
f g : G ≃* H
⊢ f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g

Tactic:
simp [MonoidWithZeroHom.ext_iff, MulEquiv.ext_iff]

Premises used: MulEquiv.ext_iff, MonoidWithZeroHom.ext_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
simp :
  (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
⊢ (∀ (X Y : C),
      HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ (Functor.obj (CochainComplex.singleFunctor C 0) X)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
simp only [hasSmallLocalizedShiftedHom_iff _ _ Q]

Premises used: DerivedCategory.Q, CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
mp :
  (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
mpr :
  (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))) →
    ∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
constructor