mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

Tactic:
intro h

Goal state after:
case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0
⊢ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).content = p.content

Tactic:
rw [content, content, Finset.gcd_def, Finset.gcd_def]
  refine congr rfl ?_
  have h : (X * p).support = p.support.map ⟨Nat.succ, Nat.succ_injective⟩ := by
    ext a
    simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]
    rcases a with - | a
    · simp
    rw [mul_comm, coeff_mul_X]
    constructor
    · intro h
      use a
    · rintro ⟨b, ⟨h1, h2⟩⟩
      rw [← Nat.succ_injective h2]
      apply h1
  rw [h]
  simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) → p = 0

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
⊢ p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = 0 → ∀ x ∈ p.support, p.coeff x = 0

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ x ∈ p.support, p.coeff x = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ p.content
⊢ ∀ (i : ℕ), r ∣ p.coeff i
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
rcases h with ⟨b, rfl⟩

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (↑a + ↑b).prod = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
← FactorSet.coe_add,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ FactorSet.prod ↑(a + b) = FactorSet.prod ↑a * FactorSet.prod ↑b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
hfd : f ∣ derivative f * g
a : R
haf : f.IsRoot a
⊢ g.IsRoot a

Tactic:
by
  rcases hfd with ⟨r, hr⟩
  have hdf0 : derivative f ≠ 0 := by
    contrapose haf
    rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
    exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
  by_contra hg
  have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
  have hr' := congr_arg (rootMultiplicity a) hr
  have : IsDomain R := {}
  rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'
  lia

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q

Tactic:
· rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ (Multiset.map Subtype.val (factors' a0)).prod

Tactic:
apply Multiset.dvd_prod

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∈ Multiset.map Subtype.val (factors' a0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ 0 < p.count m.factors → p ≤ m

Tactic:
intro h

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ≤ m
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ p.count m.factors ≠ 0 → p ≤ m

Tactic:
rw [← pos_iff_ne_zero]
  intro h
  rw [← pow_one p]
  apply (prime_pow_dvd_iff_le h0 hp).2
  simpa only

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count (↑(factors' a0) + ↑(factors' b0)) = p.count ↑(factors' a0) + p.count ↑(factors' b0)

Tactic:
← FactorSet.coe_add,

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count ↑(factors' a0 + factors' b0) = p.count ↑(factors' a0) + p.count ↑(factors' b0)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p.count (a ^ k).factors = k * p.count a.factors

Tactic:
induction k with
  | zero => rw [pow_zero, factors_one, zero_mul, count_zero hp]
  | succ n h => rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]; ring

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑(f ≪≫ₗ g.symm) = ↑(f ≪≫ₗ g.symm) ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
← End.mul_eq_comp,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a * ↑(f ≪≫ₗ g.symm) = ↑(f ≪≫ₗ g.symm) * a) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ 0 ≠ 0 → (aeval x) 0 = 0 → (↑x)⁻¹ ∈ A

Tactic:
intro h

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
h : 0 ≠ 0
⊢ (aeval x) 0 = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x

Tactic:
refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩

Goal state after:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx : IsNilpotent x
hx' : nilpotencyClass x = 0
⊢ False
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Injective ⇑(rTensor M x✝¹.subtype)

Tactic:
rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv R P).symm

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Injective ⇑(rTensor M (↑(Shrink.linearEquiv R P).symm ∘ₗ x✝¹.subtype).range.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intro h

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : Mul C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MulHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ * DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
mul_def,

Goal state after:
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : Mul C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MulHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x * y⟩⟧ =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ * DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : (i : ι) → FunLike (H i) (G i) C
inst✝³ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → CommMagma (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧ * ⟦⟨i, x✝¹⟩⟧

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : (i : ι) → FunLike (H i) (G i) C
inst✝³ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → CommMagma (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹ * x✝⟩⟧ = ⟦⟨i, x✝ * x✝¹⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : (i : ι) → FunLike (H i) (G i) C
inst✝³ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧)

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : (i : ι) → FunLike (H i) (G i) C
inst✝³ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝² * x✝¹ * x✝⟩⟧ = ⟦⟨i, x✝² * (x✝¹ * x✝)⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, x✝¹⟩⟧

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star ⟦⟨i, x✝¹ * x✝⟩⟧ = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, x✝¹⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 1⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 1 * x✝⟩⟧ = ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ * ⟦⟨i, 1⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝ * 1⟩⟧ = ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⁻¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = 1

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⁻¹ * x✝⟩⟧ = 1
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : Nonempty ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, 0⟩⟧

Tactic:
mul_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : Nonempty ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0 * x✝⟩⟧ = ⟦⟨i, 0⟩⟧