awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b = a

Tactic:
EuclideanDomain.quotient_mul_add_remainder_eq _ _

Premises used: EuclideanDomain.quotient_mul_add_remainder_eq
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
⊢ a % b + b * (a / b) = a

Tactic:
(add_comm _ _).trans (div_add_mod _ _)

Premises used: EuclideanDomain.div_add_mod, add_comm, Eq.trans
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
rw : m % k + k * (m / k) = m
⊢ m % k + m / k * k = m

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m

Tactic:
mod_add_div _ _

Premises used: EuclideanDomain.mod_add_div
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m

Tactic:
exact mod_add_div _ _

Premises used: EuclideanDomain.mod_add_div
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
rw : k * (m / k) + m % k = m
⊢ m / k * k + m % k = m

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m

Tactic:
div_add_mod _ _

Premises used: EuclideanDomain.div_add_mod
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m

Tactic:
exact div_add_mod _ _

Premises used: EuclideanDomain.div_add_mod
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
⊢ ∀ (a : R) {b : R}, b ≠ 0 → a % b ≺ b

Tactic:
EuclideanDomain.remainder_lt

Premises used: EuclideanDomain.remainder_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a ≠ 0
rw : ¬b * a ≺ b
⊢ ¬a * b ≺ b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Tactic:
mul_left_not_lt b h

Premises used: EuclideanDomain.mul_left_not_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Tactic:
exact mul_left_not_lt b h

Premises used: EuclideanDomain.mul_left_not_lt
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a : R
⊢ a % 0 = a

Tactic:
simpa only [zero_mul, zero_add] using div_add_mod a 0

Premises used: MulZeroClass.zero_mul, EuclideanDomain.div_add_mod, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1

Tactic:
simpa only [one_mul] using mul_left_not_lt 1 h

Premises used: EuclideanDomain.mul_left_not_lt, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
a : R
⊢ a / 0 = 0

Tactic:
EuclideanDomain.quotient_zero a

Premises used: EuclideanDomain.quotient_zero
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
if a0 : a = 0 then
    a0.symm ▸ H0 b
  else
    have _ := mod_lt b a0
    H1 _ _ a0 (GCD.induction (b % a) a H0 H1)

Premises used: EuclideanDomain.mod_lt, Eq.rec, dite, HMod.hMod, Eq.symm
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
exact if a0 : a = 0 then
    a0.symm ▸ H0 b
  else
    have _ := mod_lt b a0
    H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
⊢ P a b

Tactic:
classical
  exact if a0 : a = 0 then
    a0.symm ▸ H0 b
  else
    have _ := mod_lt b a0
    H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
rw :
  (if a0 : Eq.{u + 1} (α := R) 0 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a
⊢ gcd 0 a = a

Tactic:
rw [gcd]

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ (if a0 : Eq.{u + 1} (α := R) 0 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a

Tactic:
if_pos rfl

Premises used: if_pos, dite, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
a : R
⊢ (if a0 : Eq.{u + 1} (α := R) 0 0 then a
    else
      have x := ⋯;
      gcd (a % 0) 0) =
    a

Tactic:
exact if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s t r' s' t' : R
unfold :
  (if _hr : Eq.{u + 1} (α := R) 0 0 then (r', s', t')
    else
      have q := r' / 0;
      have x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
unfold xgcdAux

Premises used: EuclideanDomain.xgcdAux
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : Eq.{u + 1} (α := R) 0 0 then (r', s', t')
    else
      have q := r' / 0;
      have x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')

Tactic:
if_pos rfl

Premises used: if_pos, dite, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : Eq.{u + 1} (α := R) 0 0 then (r', s', t')
    else
      have q := r' / 0;
      have x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')

Tactic:
exact if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
lhs : xgcdAux r s t r' s' t'
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
lhs
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
rw :
  if _hr : r = 0 then (r', s', t')
  else
    have q := r' / r;
    have x := ⋯;
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
| xgcdAux r s t r' s' t'

Tactic:
rw [xgcdAux]

Premises used: EuclideanDomain.xgcdAux
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
rw :
  if _hr : r = 0 then (r', s', t')
  else
    have q := r' / r;
    have x := ⋯;
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
lhs
    rw [xgcdAux]

Premises used: EuclideanDomain.xgcdAux
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
conv :
  (if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      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
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
conv =>
    lhs
    rw [xgcdAux]

Premises used: EuclideanDomain.xgcdAux
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      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:
if_neg h

Premises used: dite, if_neg
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      have q := r' / r;
      have x := ⋯;
      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:
exact if_neg h

Premises used: if_neg
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
rw : (xgcdAux 0 1 0 s 0 1).snd.fst = 0
rw₁ rw₂ : Eq (α := R) (Prod.fst (β := R) (Prod.snd (s, 0, 1))) 0
⊢ (xgcd 0 s).fst = 0

Tactic:
rw [xgcd, xgcd_zero_left]

Premises used: EuclideanDomain.xgcd_zero_left, EuclideanDomain.xgcd
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
s : R
rw : (xgcdAux 0 1 0 s 0 1).snd.snd = 1
rw₁ rw₂ : Eq (α := R) (Prod.snd (α := R) (Prod.snd (s, 0, 1))) 1
⊢ (xgcd 0 s).snd = 1

Tactic:
rw [xgcd, xgcd_zero_left]

Premises used: EuclideanDomain.xgcd_zero_left, EuclideanDomain.xgcd
-- Module: Mathlib.Algebra.EuclideanDomain.Defs
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : DecidableEq R
x y : R
⊢ xgcd x y = (gcdA x y, gcdB x y)

Tactic:
rfl

Premises used: EuclideanDomain.gcdB, EuclideanDomain.gcdA, EuclideanDomain.xgcd, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
a b : K
pos : ∀ (h : b = 0), b * (a / b) + (a - a * b / b) = a
neg : ∀ (h : ¬b = 0), b * (a / b) + (a - a * b / b) = a
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
by_cases h : b = 0
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
a b : K
h : b = 0
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
simp [h, mul_div_cancel₀]

Premises used: mul_div_cancel₀
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
a b : K
h : ¬b = 0
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
simp [h, mul_div_cancel₀]

Premises used: mul_div_cancel₀
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
a b : K
hnb : b ≠ 0
⊢ a - a * b / b = 0 ∧ b ≠ 0

Tactic:
simp [hnb]
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
a b : K
⊢ a % b = a - a * b / b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
unfold :
  (if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a) =
    if a = 0 then b else a
⊢ EuclideanDomain.gcd a b = if a = 0 then b else a

Tactic:
unfold EuclideanDomain.gcd

Premises used: EuclideanDomain.gcd
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
pos : a = 0 → b = b
neg :
  ∀ (h : ¬a = 0),
    (have x := ⋯;
      EuclideanDomain.gcd (b % a) a) =
      a
⊢ (if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a) =
    if a = 0 then b else a

Tactic:
split_ifs
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
h : a = 0
⊢ b = b

Tactic:
simp [*, Field.mod_eq]

Premises used: Field.mod_eq
-- Module: Mathlib.Algebra.EuclideanDomain.Field
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
a b : K
h : ¬a = 0
⊢ (have x := ⋯;
    EuclideanDomain.gcd (b % a) a) =
    a

Tactic:
simp [*, Field.mod_eq]

Premises used: Field.mod_eq
-- Module: Mathlib.Algebra.EuclideanDomain.Field
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
rw₁ rw₂ : b = b
⊢ EuclideanDomain.gcd 0 b = b

Tactic:
rw [Field.gcd_eq, if_pos rfl]

Premises used: if_pos, Field.gcd_eq, rfl
-- Module: Mathlib.Algebra.EuclideanDomain.Field
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
rw₁ rw₂ : a = a
⊢ EuclideanDomain.gcd a b = a

Tactic:
rw [Field.gcd_eq, if_neg ha]

Premises used: if_neg, Field.gcd_eq
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : b ≠ 0
rw : a % b < |b|
⊢ LT.lt (α := ℤ) (↑(a % b).natAbs : ℤ) (↑b.natAbs : ℤ)

Tactic:
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]

Premises used: Int.natAbs_of_nonneg, Int.emod_nonneg, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|

Tactic:
Int.emod_lt_abs _ b0

Premises used: Int.emod_lt_abs
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|

Tactic:
exact Int.emod_lt_abs _ b0

Premises used: Int.emod_lt_abs
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : b ≠ 0
rw : a.natAbs * 1 ≤ a.natAbs * b.natAbs
⊢ a.natAbs ≤ (a * b).natAbs

Tactic:
rw [← mul_one a.natAbs, Int.natAbs_mul]

Premises used: Int.natAbs_mul, Int.natAbs, mul_one
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ 0 < b.natAbs

Tactic:
rw [← Int.natAbs_pos] at b0

Premises used: Int.natAbs_pos
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : 0 < b.natAbs
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs

Tactic:
Nat.mul_le_mul_left _ b0

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Algebra.EuclideanDomain.Int
Goal:
a b : ℤ
b0 : 0 < b.natAbs
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs

Tactic:
exact Nat.mul_le_mul_left _ b0

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
h : MulExact f g
x : M
⊢ g (f x) = 1

Tactic:
(h _).mpr <| Set.mem_range_self _

Premises used: Set.mem_range_self, Iff.mpr
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
h : MulExact f g
⊢ g ∘ f = 1

Tactic:
funext h.apply_apply_eq_one

Premises used: funext, Function.MulExact.apply_apply_eq_one
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
h1 : g ∘ f = 1
h2 : ∀ (x : N), g x = 1 → x ∈ Set.range f
⊢ MulExact f g

Tactic:
fun y => Iff.intro (h2 y) <|
    Exists.rec ((forall_apply_eq_imp_iff (p := (g · = 1))).mpr (congrFun h1) y)

Premises used: Function.MulExact, Iff.intro, Exists.rec
-- Module: Mathlib.Algebra.Exact
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

Tactic:
⟨fun H => mulExact x |>.mp <| inj <| h0 ▸ H, ?_⟩

Premises used: Eq.rec, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Exact
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
refine : x ∈ Set.range f → (g' ∘ g) x = 1
⊢ (g' ∘ g) x = 1 ↔ x ∈ Set.range f

Tactic:
refine ⟨fun H => mulExact x |>.mp <| inj <| h0 ▸ H, ?_⟩
-- Module: Mathlib.Algebra.Exact
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
rw₂ rw₃ : Eq.{u_7 + 1} (α := P') 1 1
⊢ (g' ∘ g) x = 1

Tactic:
rw [Function.comp_apply, mulExact x |>.mpr H, h0]

Premises used: Iff.mpr, Function.comp_apply
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
hc : g ∘ f = 1
hr : ∀ (y : N), g y = 1 → y ∈ Set.range f
⊢ MulExact f g

Tactic:
fun y ↦ ⟨hr y, fun ⟨x, hx⟩ ↦ hx ▸ congrFun hc x⟩

Premises used: Eq.rec, Function.MulExact, _private.0.Function.MulExact.of_comp_eq_one_of_ker_in_range.match_1, congrFun, Iff.intro, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Exact
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 }
⊢ Eq.{u_6 + 1} (α := P) (↑1 : P) 1

Tactic:
have : ((1 : Set.range g) : P) = 1 := rfl
-- Module: Mathlib.Algebra.Exact
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_1 : One (↑(Set.range g) : Type u_6) := { one := Subtype.mk (p := fun (x : P) ↦ x ∈ Set.range g) 1 hg }
this : Eq.{u_6 + 1} (α := P) (↑1 : P) 1
⊢ MulExact f g ↔
    MulExact (M := { x : N // x ∈ Set.range f }) (Subtype.val (p := fun (x : N) ↦ x ∈ Set.range f))
      (Set.rangeFactorization g)

Tactic:
simp [MulExact, Subtype.ext_iff, this]

Premises used: Function.MulExact, Subtype.ext_iff
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst : One P
h : MulExact f g
hg : 1 ∈ Set.range g
⊢ MulExact (M := { x : N // x ∈ Set.range f }) (Subtype.val (p := fun (x : N) ↦ x ∈ Set.range f))
    (Set.rangeFactorization g)

Tactic:
(iff_rangeFactorization hg).1 h

Premises used: Function.MulExact.iff_rangeFactorization, Iff.mp
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
⊢ MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P) ↔ g.ker = f.range

Tactic:
Iff.symm SetLike.ext_iff

Premises used: SetLike.ext_iff, Iff.symm
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
h1 : g.comp f = 1
h2 : g.ker ≤ f.range
⊢ MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
MulExact.of_comp_of_mem_range (congrArg DFunLike.coe h1) h2

Premises used: congrArg, DFunLike.coe, Function.MulExact.of_comp_of_mem_range
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
h1 : g.comp f = 1
h2 : ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (1 : P) → x ∈ f.range
⊢ MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
mulExact_of_comp_eq_one_of_ker_le_range h1 h2

Premises used: MonoidHom.mulExact_of_comp_eq_one_of_ker_le_range
-- Module: Mathlib.Algebra.Exact
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₃)
⊢ ∀ (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₁₂
-- Module: Mathlib.Algebra.Exact
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₂)
⊢ ∀ (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₂₃
-- Module: Mathlib.Algebra.Exact
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₃)
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₃)
⊢ 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
-- Module: Mathlib.Algebra.Exact
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₂
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₂)
⊢ 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₂

Tactic:
obtain ⟨x₂, rfl⟩ := h₂.2 y₂

Premises used: And.right, rfl