awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_3
A : Type u_4
inst : Semifield R
inst_1 : Semifield A
inst_2 : Algebra R A
r s : R
h : r⁻¹ = s
rw : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) r⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)
rw₁ rw₂ : Eq.{u_4 + 1} (α := A) ((algebraMap R A : (a : R) → A) s : A) ((algebraMap R A : (a : R) → A) s : A)
⊢ Eq.{u_4 + 1} (α := A) (((algebraMap R A : (a : R) → A) r)⁻¹ : A) ((algebraMap R A : (a : R) → A) s : A)

Tactic:
rw [← map_inv₀, h]

Premises used: map_inv₀
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
simp : IsNat.{u_2} (α := A) 1 1
⊢ IsNat.{u_2} (α := A) ((algebraMap R A : (a : R) → A) (r + 0) : A) 1

Tactic:
simp only [h.out, Nat.cast_one, add_zero, map_one]

Premises used: map_one, Mathlib.Meta.NormNum.IsNat.out, add_zero, Nat.cast_one
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ Eq.{u_2 + 1} (α := A) 1 (↑1 : A)

Tactic:
simp
-- Module: Mathlib.Tactic.Algebra.Lemmas
Goal:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat.{u_2} (α := A) 1 1

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Tactic.Bound
Goal:
R : Type
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
n : ℕ
⊢ 0 < n → LT.lt (α := R) 0 (↑n : R)

Tactic:
Nat.cast_pos.mpr

Premises used: Iff.mpr, Nat.cast_pos
-- Module: Mathlib.Tactic.Bound
Goal:
α : Type
inst : AddCommMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ 1 ≤ n → LE.le (α := α) 1 (↑n : α)

Tactic:
Nat.one_le_cast.mpr

Premises used: Iff.mpr, Nat.one_le_cast
-- Module: Mathlib.Tactic.Bound
Goal:
α : Type
inst : LinearOrder α
a b c : α
⊢ a ≤ b ∨ a ≤ c → a ≤ max b c

Tactic:
le_max_iff.mpr

Premises used: Iff.mpr, le_max_iff
-- Module: Mathlib.Tactic.Bound
Goal:
α : Type
inst : LinearOrder α
a b c : α
⊢ a < b ∨ a < c → a < max b c

Tactic:
lt_max_iff.mpr

Premises used: Iff.mpr, lt_max_iff
-- Module: Mathlib.Tactic.Bound
Goal:
α : Type
inst : LinearOrder α
a b c : α
⊢ a ≤ c ∨ b ≤ c → min a b ≤ c

Tactic:
min_le_iff.mpr

Premises used: Iff.mpr, min_le_iff
-- Module: Mathlib.Tactic.Bound
Goal:
α : Type
inst : LinearOrder α
a b c : α
⊢ a < c ∨ b < c → min a b < c

Tactic:
min_lt_iff.mpr

Premises used: Iff.mpr, min_lt_iff
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 * e2) = t1 * t2
rw₁ : n2 * n1 * (e1 * e2) = t1 * t2
rw₂ : n2 * (n1 * (e1 * e2)) = t1 * t2
rw₃ : n2 * (n1 * e1 * e2) = t1 * t2
rw₄ : n2 * (t1 * e2) = t1 * t2
rw₅ : n2 * t1 * e2 = t1 * t2
rw₆ : t1 * n2 * e2 = t1 * t2
rw₇ : t1 * (n2 * e2) = t1 * t2
rw₈ rw₉ : t1 * t2 = t1 * t2
⊢ k * (e1 * e2) = t1 * t2

Tactic:
rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
rw : n1 * n2 * (e1 / e2) = t1
rw₁ : n1 * (n2 * (e1 / e2)) = t1
rw₂ : n1 * (e1 * (n2 / e2)) = t1
rw₃ : n1 * (e1 * 1) = t1
rw₄ : n1 * e1 * 1 = t1
rw₅ : t1 * 1 = t1
rw₆ : 1 * t1 = t1
rw₇ rw₈ : t1 = t1
⊢ k * (e1 / e2) = t1

Tactic:
rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]

Premises used: mul_assoc, mul_comm, mul_div_left_comm, one_mul
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : e * n = e') (h2 : n ≠ 0), e * n = e'
⊢ e * n = e'

Tactic:
rwa [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 + e2) = t1 + t2

Tactic:
simp [left_distrib, *]

Premises used: left_distrib
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 - e2) = t1 - t2

Tactic:
simp [left_distrib, *, sub_eq_add_neg]

Premises used: sub_eq_add_neg, left_distrib
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Ring α
n e t : α
h1 : n * e = t
⊢ n * -e = -t

Tactic:
simp [*]
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
rw : l * n ^ e2 * e1 ^ e2 = l * t1 ^ e2
rw₁ : l * n ^ e2 * e1 ^ e2 = l * (n * e1) ^ e2
rw₂ : l * n ^ e2 * e1 ^ e2 = l * (n ^ e2 * e1 ^ e2)
rw₃ rw₄ : l * (n ^ e2 * e1 ^ e2) = l * (n ^ e2 * e1 ^ e2)
⊢ k * e1 ^ e2 = l * t1 ^ e2

Tactic:
rw [← h2, ← h1, mul_pow, mul_assoc]

Premises used: mul_assoc, mul_pow
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
rw : k / e = n
rw₁ : n * e / e = n
rw₂ rw₃ : n = n
⊢ k * e⁻¹ = n

Tactic:
rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]

Premises used: div_eq_mul_inv, mul_div_cancel_right₀
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
rw : 0 < ad * bd
rw₁ : 0 < 1 / gcd
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Tactic:
rw [mul_lt_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_lt_mul_iff_right₀]

Premises used: mul_assoc, mul_lt_mul_iff_right₀, mul_comm
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

Tactic:
mul_pos had hbd

Premises used: mul_pos
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

Tactic:
exact mul_pos had hbd

Premises used: mul_pos
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
one_div_pos.2 hgcd

Premises used: Iff.mpr, one_div_pos
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
exact one_div_pos.2 hgcd

Premises used: Iff.mpr, one_div_pos
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
rw : 0 < ad * bd
rw₁ : 0 < 1 / gcd
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Tactic:
rw [mul_le_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_le_mul_iff_right₀]

Premises used: mul_assoc, mul_comm, mul_le_mul_iff_right₀
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Tactic:
grind
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
rw : a ≠ b ↔ 1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b')
rw₁ : a = b ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
rw₂ rw₃ : 1 / gcd * (bd * a') = 1 / gcd * (ad * b') ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
rw [eq_iff_iff, not_iff_not, cancel_factors_eq ha hb had hbd hgcd]

Premises used: not_iff_not, Mathlib.Tactic.CancelDenoms.cancel_factors_eq, eq_iff_iff
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
rw : a ≠ b ↔ 1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b')
rw₁ : a = b ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
rw₂ rw₃ : 1 / gcd * (bd * a') = 1 / gcd * (ad * b') ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
classical
  rw [eq_iff_iff, not_iff_not, cancel_factors_eq ha hb had hbd hgcd]

Premises used: not_iff_not, Mathlib.Tactic.CancelDenoms.cancel_factors_eq, eq_iff_iff
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Mul α
a b c d : α
h : a = b
h' : c * b = d
⊢ c * a = d

Tactic:
h ▸ h'

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Tactic.CancelDenoms.Core
Goal:
α : Type u_1
inst : Mul α
a b c d e : α
h : a = b
h' : b = c
h'' : d * c = e
⊢ d * a = e

Tactic:
h ▸ h' ▸ h''

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Tactic.CategoryTheory.BicategoricalComp
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
dsimp : η ≫ 𝟙 g ≫ θ = η ≫ θ
⊢ η ⊗≫ θ = η ≫ θ

Tactic:
dsimp [bicategoricalComp]

Premises used: CategoryTheory.bicategoricalComp
-- Module: Mathlib.Tactic.CategoryTheory.BicategoricalComp
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ η.symm.hom = η.inv

Tactic:
simp only [Iso.symm_hom]

Premises used: CategoryTheory.Iso.symm_hom
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : g ⟶ h
θ' : g ≅ h
ih_θ : θ'.hom = θ
⊢ (η' ≪≫ θ').hom = η ≫ θ

Tactic:
simp [ih_η, ih_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (f ◁ᵢ η').hom = f ◁ η

Tactic:
simp [ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (η' ▷ᵢ h).hom = η ▷ h

Tactic:
simp [ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h i : a ⟶ b
inst_1 : BicategoricalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
simp [ih_η, ih_θ, bicategoricalIsoComp, bicategoricalComp]

Premises used: CategoryTheory.bicategoricalComp, CategoryTheory.bicategoricalIsoComp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
simp [e_ι]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
simp [e_η, e_θ, e_ηθ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = Iso.hom (Iso.refl f) ≫ η ≫ Iso.hom (Iso.refl g)

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h i : a ⟶ b
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
α : g ≅ h
⊢ (f ◁ᵢ α).hom = (f ◁ᵢ α).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h i j : b ⟶ c
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ≫ i ⟶ f ≫ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (f ◁ᵢ α).hom ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h i : c ⟶ d
η : h ⟶ i
η₁ : g ≫ h ⟶ g ≫ i
η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i
η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i
η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ≫ g) ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ 𝟙 a ≫ g
η₂ : 𝟙 a ≫ f ⟶ 𝟙 a ≫ g
e_η₁ : η ≫ (λ_ g).inv = η₁
e_η₂ : (λ_ f).hom ≫ η₁ = η₂
⊢ 𝟙 a ◁ η = η₂

Tactic:
simp [e_η₁, e_η₂]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η η' : g ⟶ h
θ : f ≫ g ⟶ f ≫ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
simp [e_η, e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η η' : f ⟶ g
θ : f ≫ h ⟶ g ≫ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
simp [e_η, e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
α : f ≅ g
h : b ⟶ c
⊢ α.hom ▷ h = α.hom ▷ h

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ η ▷ h = Iso.hom (Iso.refl (f ≫ h)) ≫ η ▷ h ≫ Iso.hom (Iso.refl (g ≫ h))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g h i : a ⟶ b
j : b ⟶ c
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ≫ j ⟶ i ≫ j
η₁ : g ≫ j ⟶ h ≫ j
η₂ : g ≫ j ⟶ i ≫ j
η₃ : f ≫ j ⟶ i ≫ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ▷ᵢ j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
simp_all
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₁ : (Iso.hom (Iso.refl h) ≫ η ≫ Iso.hom (Iso.refl i)) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (α ▷ᵢ k).hom ≫ η₄ = η₅
⊢ η ▷ k = η₁

Tactic:
simp at e_η₁ e_η₅
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f f' : a ⟶ b
g : b ⟶ c
h : c ⟶ d
η : f ⟶ f'
η₁ : f ≫ g ⟶ f' ≫ g
η₂ : (f ≫ g) ≫ h ⟶ (f' ≫ g) ≫ h
η₃ : (f ≫ g) ≫ h ⟶ f' ≫ g ≫ h
η₄ : f ≫ g ≫ h ⟶ f' ≫ g ≫ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ≫ h) = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
η₁ : f ⟶ g ≫ 𝟙 b
η₂ : f ≫ 𝟙 b ⟶ g ≫ 𝟙 b
e_η₁ : η ≫ (ρ_ g).inv = η₁
e_η₂ : (ρ_ f).hom ≫ η₁ = η₂
⊢ η ▷ 𝟙 b = η₂

Tactic:
simp [e_η₁, e_η₂]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e : B
p : a ⟶ b
f : b ⟶ c
g : c ⟶ d
h : d ⟶ e
pf : a ⟶ c
pfg : a ⟶ d
pfgh : a ⟶ e
η_f : p ≫ f ≅ pf
η_g : pf ≫ g ≅ pfg
η_h : 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.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ Iso.refl f ≪≫ η_f).hom = η_f.hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
rw : p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ p ◁ θ ≪≫ η_h
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
rw [← ih_η, ← ih_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ (p ◁ (η ≪≫ θ) ≪≫ η_h).hom = (p ◁ η ≪≫ p ◁ θ ≪≫ η_h).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ p ◁ θ ≪≫ η_h

Tactic:
apply Iso.ext (by simp)

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : 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.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : 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.Bicategory.whisker_exchange_assoc
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f : b ⟶ c
g h : c ⟶ d
pf : a ⟶ c
pfg : a ⟶ d
η : g ≅ h
η_f : p ≫ f ≅ pf
η_fg : pf ≫ g ≅ pfg
η_fh : pf ≫ h ≅ pfg
ih_η : pf ◁ η ≪≫ η_fh = η_fg
⊢ p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)

Tactic:
apply Iso.ext (by simp [← whisker_exchange_assoc])

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : 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.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
p : a ⟶ b
f g : b ⟶ c
h : c ⟶ d
pf : a ⟶ c
pfh : a ⟶ d
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_fh : pf ≫ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
apply Iso.ext (by simp)

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
rw : p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
⊢ p ◁ η.symm ≪≫ η_f = η_g

Tactic:
rw [← ih]
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
p : a ⟶ b
f g : b ⟶ c
pf : a ⟶ c
η : f ≅ g
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g

Tactic:
apply Iso.ext (by simp)

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
w : η.hom = θ.hom
⊢ η = θ

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

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

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom

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

Premises used: congrArg, CategoryTheory.Iso.hom