awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 * e2) = t1 * t2
have rw₅ : n2 * t1 * 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 * e2) = t1 * t2
have rw₆ : t1 * n2 * 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 * e2) = t1 * t2
have rw₇ : t1 * (n2 * 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 * e2) = t1 * t2
have rw₈ : t1 * t2 = t1 * t2
Tactic: rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
      ← mul_assoc n2, mul_comm n2, mul_assoc, h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1
have rw : n1 * n2 * (e1 / e2) = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₁ : n1 * (n2 * (e1 / e2)) = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₂ : n1 * (e1 * (n2 / e2)) = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₃ : n1 * (e1 * 1) = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₄ : n1 * e1 * 1 = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₅ : t1 * 1 = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₆ : 1 * t1 = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * (e1 / e2) = t1
have rw₇ : t1 = t1
Tactic: rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
⊢ e * n = e'
have rwa : ∀ (h : e * n = e') (h2 : n ≠ 0), e * n = e'
Tactic: rwa [mul_comm] at h
Cleared hypotheses: h, h2
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ k * e1 ^ e2 = l * t1 ^ e2
have rw : l * n ^ e2 * e1 ^ e2 = l * t1 ^ e2
Tactic: rw [← h2, ← h1, mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * e1 ^ e2 = l * t1 ^ e2
have rw₁ : l * n ^ e2 * e1 ^ e2 = l * (n * e1) ^ e2
Tactic: rw [← h2, ← h1, mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * e1 ^ e2 = l * t1 ^ e2
have rw₂ : l * n ^ e2 * e1 ^ e2 = l * (n ^ e2 * e1 ^ e2)
Tactic: rw [← h2, ← h1, mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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)
⊢ k * e1 ^ e2 = l * t1 ^ e2
have rw₃ : l * (n ^ e2 * e1 ^ e2) = l * (n ^ e2 * e1 ^ e2)
Tactic: rw [← h2, ← h1, mul_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ k * e⁻¹ = n
have rw : k / e = n
Tactic: rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
Goal:
α : Type u_1
inst : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
rw : k / e = n
⊢ k * e⁻¹ = n
have rw₁ : n * e / e = n
Tactic: rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ k * e⁻¹ = n
have rw₂ : n = n
Tactic: rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
have rw : 0 < ad * bd
Tactic: rw [mul_lt_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_lt_mul_iff_right₀]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
have rw₁ : 0 < 1 / gcd
Tactic: rw [mul_lt_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_lt_mul_iff_right₀]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
have rw : 0 < ad * bd
Tactic: rw [mul_le_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_le_mul_iff_right₀]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
have rw₁ : 0 < 1 / gcd
Tactic: rw [mul_le_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_le_mul_iff_right₀]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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'))
have rw : 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
have rw₂ : 1 / gcd * (bd * a') = 1 / gcd * (ad * 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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'))
have rw : 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.Tactic.CancelDenoms.Core (goal)
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')
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
have rw₂ : 1 / gcd * (bd * a') = 1 / gcd * (ad * 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]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.BicategoricalComp (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ⊗≫ θ = η ≫ θ
have dsimp : η ≫ 𝟙 g ≫ θ = η ≫ θ
Tactic: dsimp [bicategoricalComp]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.Normalize (hypothesis)
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 ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅
have e_η₆ : η ▷ k = η₁
Tactic: simp at e_η₁ e_η₅
Cleared hypotheses: e_η₁
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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 = η_f
have rw : p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ p ◁ θ ≪≫ η_h
Tactic: rw [← ih_η, ← ih_θ]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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 η_fg
have rw : p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
Tactic: rw [← ih_η]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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 η_f η_fh
have rw : p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh
Tactic: rw [← ih_η]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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 ≪≫ η_f = η_g
have rw : p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
Tactic: rw [← ih]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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
⊢ η = θ
have w : η.hom = θ.hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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 = θ.hom
have simp : η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).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_θ)]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (goal)
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
simp : η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom
⊢ η.hom = θ.hom
have simp₁ : (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).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_θ)]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Elementwise (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_1 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
have rw : Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
  ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.IsoReassoc (goal)
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
⊢ f ≪≫ h = g ≪≫ h
have rw : g ≪≫ h = g ≪≫ h
Tactic: rw [w]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.Normalize (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j k : C
α : g ≅ tensorObj.{v, u} (𝒞 := inst) f h
η : h ⟶ i
ηs : tensorObj.{v, u} (𝒞 := inst) f i ⟶ j
η₁ : tensorObj.{v, u} (𝒞 := inst) h k ⟶ tensorObj.{v, u} (𝒞 := inst) i k
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k)
ηs₁ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f i) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
ηs₂ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₃ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₄ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₅ : tensorObj.{v, u} (𝒞 := inst) g k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
e_η₁ : (Iso.hom (Iso.refl h) ≫ η ≫ Iso.hom (Iso.refl i)) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : Iso.inv (α_ f i k) ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : Iso.hom (α_ f h k) ≫ η₃ = η₄
e_η₅ : Iso.hom (α ▷ᵢ k) ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅
have e_η₆ : η ▷ k = η₁
Tactic: simp at e_η₁ e_η₅
Cleared hypotheses: e_η₁
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.Normalize (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : tensorObj.{v, u} (𝒞 := inst) g f' ⟶ tensorObj.{v, u} (𝒞 := inst) h g'
η₁ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h g')
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
η₃ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
e_ηθ : η ⊗ₘ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ Iso.inv (α_ f h g') = η₂
e_η₃ : Iso.hom (α_ f g f') ≫ η₂ = η₃
⊢ f ◁ η ⊗ₘ θ = η₃
have simp : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g')
  (f ◁ η ⊗ₘ θ) (Iso.hom (α_ f g f') ≫ f ◁ (η ⊗ₘ θ) ≫ Iso.inv (α_ f h g'))
Tactic: simp only [← e_ηθ, ← e_η₁, ← e_η₂, ← e_η₃]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.Normalize (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) h f
ηθ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) h f) g'
ηθ₁ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
ηθ₂ :
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g') = ηθ
e_ηθ₁ : ηθ ≫ Iso.hom (α_ h f g') = ηθ₁
e_ηθ₂ : Iso.inv (α_ g f f') ≫ ηθ₁ = ηθ₂
⊢ η ⊗ₘ f ◁ θ = ηθ₂
have simp : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g'))
  (η ⊗ₘ f ◁ θ)
  (Iso.inv (α_ g f f') ≫ (η ▷ f ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g')) ≫ Iso.hom (α_ h f g'))
Tactic: simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
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 = normalizeIsoComp η_f η_fg
have rw : p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
Tactic: rw [← ih_η]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
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 = normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)
have w : (p ◁ f ◁ η ≪≫ normalizeIsoComp η_f η_fh).hom = (normalizeIsoComp η_f (pf ◁ η ≪≫ η_fh)).hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
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 = normalizeIsoComp η_f η_fh
have rw : p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh
Tactic: rw [← ih_η]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
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 = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh
have w : (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
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 ◁ (η ⊗ᵢ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
have rw : p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
Tactic: rw [tensorIso_def]