awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h h' i i' : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
θ : g' ⟶ h'
θs : h' ⟶ i'
ηθ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) h h'
ηθs : tensorObj.{v, u} (𝒞 := inst) h h' ⟶ tensorObj.{v, u} (𝒞 := inst) i i'
ηθ₁ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) i i'
ηθ₂ : tensorObj.{v, u} (𝒞 := inst) f f' ⟶ tensorObj.{v, u} (𝒞 := inst) i i'
e_ηθ : η ⊗ₘ θ = ηθ
e_ηθs : ηs ⊗ₘ θs = ηθs
e_ηθ₁ : ηθ ≫ ηθs = ηθ₁
e_ηθ₂ : Iso.hom (α ⊗ᵢ β) ≫ ηθ₁ = ηθ₂
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom ≫ θ ≫ θs = ηθ₂

Tactic:
simp [← e_ηθ, ← e_ηθs, ← e_ηθ₁, ← e_ηθ₂]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfg pfgh : C
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) pf g ≅ pfg
η_h : tensorObj.{v, u} (𝒞 := inst) pfg h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f pf : C
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
⊢ Iso.hom (p ◁ λ_ f ≪≫ η_f) = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f pf : C
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
⊢ Iso.hom (p ◁ ρ_ f ≪≫ η_f) = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f pf : C
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
⊢ p ◁ Iso.refl f ≪≫ η_f = η_f

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf : C
η : f ≅ g
θ : g ≅ h
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
η_h : tensorObj.{v, u} (𝒞 := inst) p h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
simp_all
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfg : C
η : g ≅ h
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_fg : tensorObj.{v, u} (𝒞 := inst) pf g ≅ pfg
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
rw : p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg

Tactic:
rw [← ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfg : C
η : g ≅ h
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_fg : tensorObj.{v, u} (𝒞 := inst) pf g ≅ pfg
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
w : (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfg : C
η : g ≅ h
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_fg : tensorObj.{v, u} (𝒞 := inst) pf g ≅ pfg
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom

Tactic:
simp [← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfh : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
rw : p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Tactic:
rw [← ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfh : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
w : (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g h pf pfh : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
η_fh : tensorObj.{v, u} (𝒞 := inst) pf h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
rw : p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
⊢ p ◁ (η ⊗ᵢ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂

Tactic:
rw [tensorIso_def]

Premises used: CategoryTheory.MonoidalCategory.tensorIso_def
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
ih_η₁ : p ◁ η ▷ f₂ ≪≫ normalizeIsoComp η_g₁ η_f₂ = normalizeIsoComp η_f₁ η_f₂
ih_θ₁ : p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂
η_g : tensorObj.{v, u} (𝒞 := inst) p (tensorObj.{v, u} (𝒞 := inst) g₁ f₂) ≅ pf₁f₂
⊢ p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂

Tactic:
apply naturality_comp

Premises used: Mathlib.Tactic.Monoidal.naturality_comp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ η ▷ f₂ ≪≫ normalizeIsoComp η_g₁ η_f₂ = normalizeIsoComp η_f₁ η_f₂

Tactic:
apply naturality_whiskerRight _ _ _ ih_η

Premises used: Mathlib.Tactic.Monoidal.naturality_whiskerRight
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂

Tactic:
apply naturality_whiskerLeft _ _ _ ih_θ

Premises used: Mathlib.Tactic.Monoidal.naturality_whiskerLeft
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g pf : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
rw : p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
rw [← ih]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g pf : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
w : (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g pf : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
w : η.hom = θ.hom
⊢ η = θ

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
⊢ η.hom = Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g)

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_η)]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
⊢ Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g) = θ.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
simp : η.hom = Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g)
simp₁ : Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g) = θ.hom
⊢ η.hom = θ.hom

Tactic:
calc
    η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : tensorUnit.{v, u} C (𝒞 := inst) ◁ η' ≪≫ η_g = η_f
Hθ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g)

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hη)]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : tensorUnit.{v, u} C (𝒞 := inst) ◁ η' ≪≫ η_g = η_f
Hθ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ' ≪≫ η_g = η_f
⊢ Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g) = θ'.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hθ)]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.MonoidalComp
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ⊗≫ g = f ≫ g

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.Tactic.CategoryTheory.Reassoc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
rw rw₁ : g ≫ h = g ≫ h
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]
-- Module: Mathlib.Tactic.CategoryTheory.ToApp
Goal:
C D : Cat
F G : C ⟶ D
η θ : F ⟶ G
h : η = θ
⊢ η.toNatTrans = θ.toNatTrans

Tactic:
congr(($h).toNatTrans)

Premises used: congrArg, id, CategoryTheory.Cat.Hom₂.toNatTrans
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[>] c) l

Tactic:
simpa [← Function.comp_def, Tendsto, ← Filter.map_map] using h

Premises used: Filter.map_map, Function.comp_def, Filter.Tendsto
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
h₁ : Eq (α := 𝕜 → α) (fun (x : 𝕜) ↦ f (c - x⁻¹)) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv)
convert_to : ∀ (h : Tendsto (α := 𝕜) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l), Tendsto f (𝓝[<] c) l
⊢ Tendsto f (𝓝[<] c) l

Tactic:
convert_to Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l at h

Premises used: Function.comp, Filter.atTop, Inv.inv, HAdd.hAdd, Filter.Tendsto, Neg.neg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
h₁ : ∀ (x : 𝕜), f (c - x⁻¹) = (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) x
⊢ Eq (α := 𝕜 → α) (fun (x : 𝕜) ↦ f (c - x⁻¹)) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv)

Tactic:
ext
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
x : 𝕜
⊢ f (c - x⁻¹) = (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) x

Tactic:
simp [AddGroupWithOne.sub_eq_add_neg]

Premises used: AddGroupWithOne.sub_eq_add_neg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (α := 𝕜) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l
⊢ Tendsto f (𝓝[<] c) l

Tactic:
simpa [Tendsto, ← Filter.map_map] using h

Premises used: Filter.map_map, Filter.Tendsto
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h_neg : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
h_pos : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop l
⊢ Tendsto f (𝓝[≠] c) l

Tactic:
simpa [Tendsto, ← nhdsLT_sup_nhdsGT] using
    ⟨tendsto_nhdsLT_of_tendsto_atTop _ _ h_neg, tendsto_nhdsGT_of_tendsto_atTop _ _ h_pos⟩

Premises used: Filter.Tendsto, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst_5 : TopologicalSpace α
a b : α
h_neg : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
apply : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 a)
⊢ Tendsto f (𝓝[≠] c) (𝓝 a)

Tactic:
apply tendsto_nhdsNE_of_tendsto_atTop _ _ h_neg

Premises used: Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst_5 : TopologicalSpace α
a b : α
h_neg : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 b)

Tactic:
h_pos
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst_5 : TopologicalSpace α
a b : α
h_neg : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 a)

Tactic:
convert! h_pos
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
C : ℝ
f g : ℝ → ℝ
l : Filter ℝ
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ g x / f x) l atTop
hC : 0 < C
⊢ IsBigOWith C l f g

Tactic:
Asymptotics.IsLittleO.forall_isBigOWith (.of_tendsto_div_atTop h) hC

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_tendsto_div_atTop
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
C : ℝ
f g : ℝ → ℝ
l : Filter ℝ
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ g x / f x) l atBot
hC : 0 < C
⊢ IsBigOWith C l f g

Tactic:
Asymptotics.IsLittleO.forall_isBigOWith (.of_tendsto_div_atBot h) hC

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_tendsto_div_atBot
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
f g : ℝ → ℝ
l : Filter ℝ
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ g x / f x) l atTop
⊢ f =O[l] g

Tactic:
Asymptotics.IsLittleO.isBigO (.of_tendsto_div_atTop h)

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.IsLittleO.of_tendsto_div_atTop
-- Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas
Goal:
f g : ℝ → ℝ
l : Filter ℝ
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ g x / f x) l atBot
⊢ f =O[l] g

Tactic:
Asymptotics.IsLittleO.isBigO (.of_tendsto_div_atBot h)

Premises used: Asymptotics.IsLittleO.of_tendsto_div_atBot, Asymptotics.IsLittleO.isBigO
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
⊢ WellFormedBasis []

Tactic:
simp [WellFormedBasis]

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f : ℝ → ℝ
hf : Tendsto f atTop atTop
⊢ WellFormedBasis [f]

Tactic:
simpa [WellFormedBasis]

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis basis' : Basis
h : List.Sublist basis basis'
h_basis : WellFormedBasis basis'
⊢ WellFormedBasis basis

Tactic:
⟨h_basis.left.sublist h, fun _ hf ↦ h_basis.right _ (h.subset hf)⟩

Premises used: List.Pairwise.sublist, List.Sublist.subset, And.right, And.left, And.intro, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ List.Sublist basis_tl (basis_hd :: basis_tl)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
h : WellFormedBasis (left ++ right)
⊢ List.Sublist right (left ++ right)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
g : ℝ → ℝ
hg : g ∈ basis
inl :
  ∀ (h : WellFormedBasis [])
    (h_comp : ∀ (g : ℝ → ℝ), List.getLast? [] = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g))
    (hg : Membership.mem (γ := Basis) [] g), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
inr :
  ∀ (basis_begin : List (ℝ → ℝ)) (basis_end : ℝ → ℝ) (h : WellFormedBasis (basis_begin.concat basis_end))
    (h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g))
    (hg : g ∈ basis_begin.concat basis_end), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
rcases basis.eq_nil_or_concat with rfl | ⟨basis_begin, basis_end, rfl⟩

Premises used: List.eq_nil_or_concat, rfl
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
h : WellFormedBasis []
h_comp : ∀ (g : ℝ → ℝ), List.getLast? [] = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : Membership.mem (γ := Basis) [] g
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
simp at hg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
⊢ g ∈ basis_begin ∨ g = basis_end

Tactic:
simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp

Premises used: List.getLast?_append, Option.some.injEq, forall_eq', List.concat_eq_append, List.mem_append, List.getLast?_singleton, or_false, List.mem_cons, Option.some_or, List.not_mem_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
hg₁ : g ∈ basis_begin ∨ g = basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)

Tactic:
simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp

Premises used: List.getLast?_append, Option.some.injEq, forall_eq', List.concat_eq_append, List.mem_append, List.getLast?_singleton, or_false, List.mem_cons, Option.some_or, List.not_mem_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
hg : g ∈ basis_begin ∨ g = basis_end
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
inr : ∀ (hg : g ∈ basis_begin), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
inr₁ : ∀ (hg : g = basis_end), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
rcases hg with hg | hg