awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : y ≠ 0
a : R
ha : x = y * a
⊢ x / y = z ↔ x = y * z
have rw : a = z ↔ y * a = y * z
Tactic: rw [ha, mul_div_cancel_left₀ _ h1]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x = y / z ↔ z * x = y
have rw : y / z = x ↔ z * x = y
Tactic: rw [eq_comm, div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : y / z = x ↔ z * x = y
⊢ x = y / z ↔ z * x = y
have rw₁ : y = z * x ↔ z * x = y
Tactic: rw [eq_comm, div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
rw : y / z = x ↔ z * x = y
rw₁ : y = z * x ↔ z * x = y
⊢ x = y / z ↔ z * x = y
have rw₂ : z * x = y ↔ z * x = y
Tactic: rw [eq_comm, div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x / y = z / t ↔ t * x = y * z
have rw : t ∣ y * z
Tactic: rw [div_eq_iff_eq_mul_of_dvd _ _ _ h1 h3, ← mul_div_assoc _ h4,
    eq_div_iff_mul_eq_of_dvd _ _ _ h2]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ t ∣ y * z
have obtain : ∀ (a : R) (ha : z = t * a), t ∣ y * z
Tactic: obtain ⟨a, ha⟩ := h4
Cleared hypotheses: h4
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
⊢ t ∣ y * z
have h : y * z = t * (y * a)
Tactic: use y * a
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
⊢ y * z = t * (y * a)
have h : y * (t * a) = t * (y * a)
Tactic: rw [ha, mul_comm, mul_assoc, mul_comm y a]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
h : y * (t * a) = t * (y * a)
⊢ y * z = t * (y * a)
have h₁ : t * a * y = t * (y * a)
Tactic: rw [ha, mul_comm, mul_assoc, mul_comm y a]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
h : y * (t * a) = t * (y * a)
h₁ : t * a * y = t * (y * a)
⊢ y * z = t * (y * a)
have h₂ : t * (a * y) = t * (y * a)
Tactic: rw [ha, mul_comm, mul_assoc, mul_comm y a]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
a : R
ha : z = t * a
h : y * (t * a) = t * (y * a)
h₁ : t * a * y = t * (y * a)
h₂ : t * (a * y) = t * (y * a)
⊢ y * z = t * (y * a)
have h₃ : t * (a * y) = t * (a * y)
Tactic: rw [ha, mul_comm, mul_assoc, mul_comm y a]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
⊢ HAdd.hAdd (β := S)
      (HMul.hMul (β := S) b
        ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S))
      ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S) =
    a
have a₁ : Eq.{u_1 + 1} (α := R)
  ((e : (a : S) → R)
      (HAdd.hAdd (β := S)
        (HMul.hMul (β := S) b
          ((e.symm : (a : R) → S) (HDiv.hDiv (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
            S))
        ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) :
          S)) :
    R)
  ((e : (a : S) → R) a : R)
Tactic: apply e.injective
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ EuclideanDomain.r.{u_1} (R := R)
    ((e : (a : S) → R)
        ((e.symm : (a : R) → S) (HMod.hMod (α := R) (β := R) ((e : (a : S) → R) a : R) ((e : (a : S) → R) b : R)) : S) :
      R)
    ((e : (a : S) → R) b : R)
have hb' : Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)
Tactic: have hb' : e b ≠ 0 := by simpa using hb
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ ¬EuclideanDomain.r.{u_1} (R := R) ((e : (a : S) → R) (a * b) : R) ((e : (a : S) → R) a : R)
have hb' : Ne.{u_1 + 1} (α := R) ((e : (a : S) → R) b : R) (0 : R)
Tactic: have hb' : e b ≠ 0 := by simpa using hb
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m
have rw : m % k + k * (m / k) = m
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m
have rw : k * (m / k) + m % k = m
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b
have rw : ¬b * a ≺ b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ gcd 0 a = a
have rw : (if a0 : Eq.{u + 1} (α := R) 0 0 then a
  else
    have x := sorry;
    gcd (a % 0) 0) =
  a
Tactic: rw [gcd]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')
have unfold : (if _hr : Eq.{u + 1} (α := R) 0 0 then (r', s', t')
  else
    have q := r' / 0;
    have x := sorry;
    xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
  (r', s', t')
Tactic: unfold xgcdAux
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
have lhs : xgcdAux r s t r' s' t'
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t'
have rw : if _hr : r = 0 then (r', s', t')
else
  have q := r' / r;
  have x := sorry;
  xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
Tactic: rw [xgcdAux]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
have rw : if _hr : r = 0 then (r', s', t')
else
  have q := r' / r;
  have x := sorry;
  xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
Tactic: lhs
    rw [xgcdAux]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
have conv : (if _hr : r = 0 then (r', s', t')
  else
    have q := r' / r;
    have x := sorry;
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
  xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
Tactic: conv =>
    lhs
    rw [xgcdAux]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0
have rw : (xgcdAux 0 1 0 s 0 1).snd.fst = 0
Tactic: rw [xgcd, xgcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
rw : (xgcdAux 0 1 0 s 0 1).snd.fst = 0
⊢ (xgcd 0 s).fst = 0
have rw₁ : Eq (α := R) (Prod.fst (β := R) (Prod.snd (s, 0, 1))) 0
Tactic: rw [xgcd, xgcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
have rw : (xgcdAux 0 1 0 s 0 1).snd.snd = 1
Tactic: rw [xgcd, xgcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Defs (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
rw : (xgcdAux 0 1 0 s 0 1).snd.snd = 1
⊢ (xgcd 0 s).snd = 1
have rw₁ : Eq (α := R) (Prod.snd (α := R) (Prod.snd (s, 0, 1))) 1
Tactic: rw [xgcd, xgcd_zero_left]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
a b : K
⊢ b * (a / b) + (a - a * b / b) = a
have pos : ∀ (h : b = 0), b * (a / b) + (a - a * b / b) = a
Tactic: by_cases h : b = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
a b : K
pos : ∀ (h : b = 0), b * (a / b) + (a - a * b / b) = a
⊢ b * (a / b) + (a - a * b / b) = a
have neg : ∀ (h : ¬b = 0), b * (a / b) + (a - a * b / b) = a
Tactic: by_cases h : b = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
⊢ EuclideanDomain.gcd a b = if a = 0 then b else a
have unfold : (if a0 : a = 0 then b
  else
    have x := sorry;
    EuclideanDomain.gcd (b % a) a) =
  if a = 0 then b else a
Tactic: unfold EuclideanDomain.gcd
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a) =
    if a = 0 then b else a
have pos : a = 0 → b = b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
pos : a = 0 → b = b
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a) =
    if a = 0 then b else a
have neg : ∀ (h : ¬a = 0),
  (have x := sorry;
    EuclideanDomain.gcd (b % a) a) =
    a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
b : K
⊢ EuclideanDomain.gcd 0 b = b
have rw : (if Eq.{u_1 + 1} (α := K) 0 0 then b else 0) = b
Tactic: rw [Field.gcd_eq, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
b : K
rw : (if Eq.{u_1 + 1} (α := K) 0 0 then b else 0) = b
⊢ EuclideanDomain.gcd 0 b = b
have rw₁ : b = b
Tactic: rw [Field.gcd_eq, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a : K
ha : a ≠ 0
b : K
⊢ EuclideanDomain.gcd a b = a
have rw : (if a = 0 then b else a) = a
Tactic: rw [Field.gcd_eq, if_neg ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Field (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a : K
ha : a ≠ 0
b : K
rw : (if a = 0 then b else a) = a
⊢ EuclideanDomain.gcd a b = a
have rw₁ : a = a
Tactic: rw [Field.gcd_eq, if_neg ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Int (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ LT.lt (α := ℤ) (↑(a % b).natAbs : ℤ) (↑b.natAbs : ℤ)
have rw : a % b < |b|
Tactic: rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Int (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs ≤ (a * b).natAbs
have rw : a.natAbs * 1 ≤ a.natAbs * b.natAbs
Tactic: rw [← mul_one a.natAbs, Int.natAbs_mul]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Int (hypothesis)
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs
have b0₁ : 0 < b.natAbs
Tactic: rw [← Int.natAbs_pos] at b0
Cleared hypotheses: b0
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst : One P
inst_1 : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
⊢ (g' ∘ g) x = 1 ↔ x ∈ Set.range f
have refine : x ∈ Set.range f → (g' ∘ g) x = 1
Tactic: refine ⟨fun H => mulExact x |>.mp <| inj <| h0 ▸ H, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst : One P
inst_1 : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
⊢ (g' ∘ g) x = 1
have rw : g' (g x) = 1
Tactic: rw [Function.comp_apply, mulExact x |>.mpr H, h0]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst : One P
inst_1 : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
rw : g' (g x) = 1
rw₁ : g' 1 = 1
⊢ (g' ∘ g) x = 1
have rw₂ : Eq.{u_7 + 1} (α := P') 1 1
Tactic: rw [Function.comp_apply, mulExact x |>.mpr H, h0]
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
hg : 1 ∈ Set.range g
this : One (↑(Set.range g) : Type u_6) := { one := Subtype.mk (p := fun (x : P) ↦ x ∈ Set.range g) 1 hg }
⊢ MulExact f g ↔
    MulExact (M := { x : N // x ∈ Set.range f }) (Subtype.val (p := fun (x : N) ↦ x ∈ Set.range f))
      (Set.rangeFactorization g)
have this₁ : Eq.{u_6 + 1} (α := P) (↑1 : P) 1
Tactic: have : ((1 : Set.range g) : P) = 1 := rfl
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₁₂ : f'.comp τ₁ = τ₂.comp f
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
⊢ MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) ↔
    MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
have comm₁₃ : ∀ (x : M₁), Eq.{u_12 + 1} (α := N₂) ((f'.comp τ₁ : (a : M₁) → N₂) x : N₂) ((τ₂.comp f : (a : M₁) → N₂) x : N₂)
Tactic: replace comm₁₂ := DFunLike.congr_fun comm₁₂
Cleared hypotheses: comm₁₂
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ : ∀ (x : M₁), Eq.{u_12 + 1} (α := N₂) ((f'.comp τ₁ : (a : M₁) → N₂) x : N₂) ((τ₂.comp f : (a : M₁) → N₂) x : N₂)
⊢ MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) ↔
    MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
have comm₂₄ : ∀ (x : M₂), Eq.{u_13 + 1} (α := N₃) ((g'.comp τ₂ : (a : M₂) → N₃) x : N₃) ((τ₃.comp g : (a : M₂) → N₃) x : N₃)
Tactic: replace comm₂₃ := DFunLike.congr_fun comm₂₃
Cleared hypotheses: comm₂₃
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
⊢ MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) ↔
    MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
have mp : MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) →
  MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
mp :
  MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) →
    MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
⊢ MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃) ↔
    MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
have mpr : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃) →
  MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
y₂ : N₂
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) y₂ : N₃) (1 : N₃) ↔
    Membership.mem (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂)) y₂
have mp : ∀ (x₂ : M₂),
  Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃) ↔
    Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
      ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
Tactic: obtain ⟨x₂, rfl⟩ := h₂.2 y₂
Cleared hypotheses: y₂
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
x₂ : M₂
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃) ↔
    Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
      ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
have mp : Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃) →
  Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
    ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
x₂ : M₂
mp :
  Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃) →
    Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
      ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃) ↔
    Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
      ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
have mp₁ : Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
    ((τ₂ : (a : M₂) → N₂) x₂ : N₂) →
  Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)
Tactic: constructor