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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support).val =
    Multiset.map p.coeff p.support.val

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ (X ^ 0).content = 1

Tactic:
simp

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

Goal state before:
pp: case h.right
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b

Tactic:
simp

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

Goal state before:
pp: case heval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ ∀ (i : ι), eval (f i) (p - q) = 0

pp: case hcard
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ (p - q).natDegree < Fintype.card ι

Tactic:
· simpa [sub_eq_zero]

Goal state after:
case hcard
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p q : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = eval (f i) q
hcard : max p.natDegree q.natDegree < Fintype.card ι
⊢ (p - q).natDegree < Fintype.card ι
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
⊢ Fintype { x // x ∣ y }

Tactic:
haveI : Nontrivial M := ⟨⟨y, 0, hy⟩⟩
  haveI : StrongNormalizationMonoid M := UniqueFactorizationMonoid.strongNormalizationMonoid
  haveI := Classical.decEq M
  haveI := Classical.decEq (Associates M)
  -- We'll show `fun (u : Mˣ) (f ⊆ factors y) ↦ u * Π f` is injective
  -- and has image exactly the divisors of `y`.
  refine
    Fintype.subtype
      (((normalizedFactors y).powerset.toFinset ×ˢ (Finset.univ : Finset Mˣ)).image fun s =>
        (s.snd : M) * s.fst.prod)
      fun x => ?_
  simp only [Finset.mem_image, Finset.mem_product, Finset.mem_univ, and_true,
    Multiset.mem_toFinset, Multiset.mem_powerset]
  constructor
  · rintro ⟨s, hs, rfl⟩
    rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul,
      ← (prod_normalizedFactors hy).dvd_iff_dvd_right]
    exact Multiset.prod_dvd_prod_of_le hs
  · rintro (h : x ∣ y)
    have hx : x ≠ 0 := by
      refine mt (fun hx => ?_) hy
      rwa [hx, zero_dvd_iff] at h
    obtain ⟨u, hu⟩ := prod_normalizedFactors hx
    refine ⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩
    exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
b : FactorSet α
⊢ ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : DecidableEq (Associates α)
a : FactorSet α
⊢ a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤

Tactic:
simp

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

Goal state before:
pp: case zero.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q✝ : R[X]
a✝ : Nontrivial R
q : R[X]
⊢ Associated (0 * q).content (content 0 * q.content)

Tactic:
simp

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

Goal state before:
pp: case zero.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q : R[X]
a✝ : Nontrivial R
p : R[X]
⊢ Associated (p * 0).content (p.content * content 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
b : FactorSet α
⊢ (⊤ + b).prod = ⊤.prod * b.prod

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : FactorSet α
⊢ (a + ⊤).prod = a.prod * ⊤.prod

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : ↑(rootMultiplicity t p)! * eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False

Tactic:
mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (roots 0).card + natDegree 0 = natDegree 0 ∧ roots 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : FactorSet α
x✝ : a ≤ ⊤
⊢ a.prod ≤ ⊤.prod

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h✝ : p ≠ 0
h : ∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t
⊢ 1 ≤ 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
⊢ ↑{ val := C ↑(normUnit (leadingCoeff 0)), inv := C ↑(normUnit (leadingCoeff 0))⁻¹, val_inv := ⋯, inv_val := ⋯ } = ↑1

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
⊢ ↑{ val := C ↑(normUnit (leadingCoeff 1)), inv := C ↑(normUnit (leadingCoeff 1))⁻¹, val_inv := ⋯, inv_val := ⋯ } = ↑1

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C (↑w * ↑w⁻¹) * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = p * C (p.coeff 0)⁻¹

Tactic:
by
        conv in p => rw [eq_C_of_degree_le_zero this]
        rw [← C_mul, mul_inv_cancel₀ hc, C_1]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (Associates.mk 0).factors.prod = Associates.mk 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
⊢ Multiset.filter (fun x ↦ x ∈ f.range) (map f p).roots = Multiset.map (⇑f) p.roots

Tactic:
ext b

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
b : B
⊢ count b (Multiset.filter (fun x ↦ x ∈ f.range) (map f p).roots) = count b (Multiset.map (⇑f) p.roots)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq : q ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).degree = q.degree

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : (Associates.mk a).factors ⊓ (Associates.mk b).factors = 0
⊢ ((Associates.mk a).factors ⊓ (Associates.mk b).factors).prod = 1

Tactic:
hf

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : (Associates.mk a).factors ⊓ (Associates.mk b).factors = 0
⊢ FactorSet.prod 0 = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ Quot.out (Associates.mk 0 ⊔ Associates.mk a) = 0

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ Quot.out (Associates.mk a ⊔ Associates.mk 0) = 0

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a : α
⊢ (⊤ ⊔ Associates.mk a).out = 0

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a : α
⊢ (Associates.mk a ⊔ ⊤).out = 0

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : ¬n = 0
⊢ 1 / 0 = 0

Tactic:
simp

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
w : Multiset (MvPolynomial (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial (↥s) D)ˣ
hw : w.prod * ↑u = a'
⊢ (rename Subtype.val) (w.prod * ↑u) = (rename Subtype.val) a'

Tactic:
hw

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
w : Multiset (MvPolynomial (↥s) D)
h : ∀ b ∈ w, Prime b
u : (MvPolynomial (↥s) D)ˣ
hw : w.prod * ↑u = a'
⊢ (rename Subtype.val) a' = (rename Subtype.val) a'
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ ∃ r, r.IsPrimitive ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s

Tactic:
by
  classical
    have h : ∃ (n : ℕ) (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r :=
      ⟨(p * q).natDegree, p * q, rfl, hp.mul hq, dvd_mul_right _ _, dvd_mul_left _ _⟩
    rcases Nat.find_spec h with ⟨r, rdeg, rprim, pr, qr⟩
    refine ⟨r, rprim, fun s => ⟨?_, fun rs => ⟨pr.trans rs, qr.trans rs⟩⟩⟩
    suffices hs : ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s from
      hs s.natDegree s rfl
    clear s
    by_contra! con
    rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩
    have s0 : s ≠ 0 := by
      contrapose rs
      simp [rs]
    have hs :=
      Nat.find_min' h
        ⟨_, s.natDegree_primPart, s.isPrimitive_primPart, (hp.dvd_primPart_iff_dvd s0).2 ps,
          (hq.dvd_primPart_iff_dvd s0).2 qs⟩
    rw [← rdeg] at hs
    by_cases! sC : s.natDegree ≤ 0
    · rw [eq_C_of_natDegree_le_zero (le_trans hs sC), isPrimitive_iff_content_eq_one, content_C,
        normalize_eq_one] at rprim
      rw [eq_C_of_natDegree_le_zero (le_trans hs sC), ← dvd_content_iff_C_dvd] at rs
      apply rs rprim.dvd
    have hcancel := natDegree_cancelLeads_lt_of_natDegree_le_natDegree hs sC
    rw [sdeg] at hcancel
    apply Nat.find_min con hcancel
    refine
      ⟨_, rfl, ⟨dvd_cancelLeads_of_dvd_of_dvd pr ps, dvd_cancelLeads_of_dvd_of_dvd qr qs⟩,
        fun rcs => rs ?_⟩
    rw [← rprim.dvd_primPart_iff_dvd s0]
    rw [cancelLeads, tsub_eq_zero_iff_le.mpr hs, pow_zero, mul_one] at rcs
    have h :=
      dvd_add rcs (Dvd.intro_left (C (leadingCoeff s) * X ^ (natDegree s - natDegree r)) rfl)
    nontriviality R
    have hC0 := rprim.ne_zero
    rw [Ne, ← leadingCoeff_eq_zero, ← C_eq_zero] at hC0
    rw [sub_add_cancel, ← rprim.dvd_primPart_iff_dvd (mul_ne_zero hC0 s0)] at h
    refine h.trans (Associated.dvd ?_)
    grw [associated_primPart_mul (mul_ne_zero hC0 s0)]
    exact associated_unit_mul_left _ _ (isUnit_primPart_C _)

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{v, u} (max #R ℵ₀) * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ max (lift.{v, u} #R) ℵ₀ ≤ ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ {x | IsAlgebraic R x}.Countable

Tactic:
rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]
  apply (cardinalMk_lift_le_max R A).trans
  simp

Goal state after:
Module: Mathlib.Algebra.Azumaya.Defs

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (Algebra.moduleAux (r • ab)) a = r • (Algebra.moduleAux ab) a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
x✝ : R
⊢ (algebraMap R A) x✝ = (⇑(aeval a) ∘ ⇑C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ ↑((aeval ⟨s, ⋯⟩).toRingHom r) = ↑⟨(aeval s) r, ht⟩

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ (algEquivOfTranscendental R s h) X = ⟨s, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
f : R[X]
⊢ (algEquivOfTranscendental R s h).toEquiv ((algEquivOfTranscendental R s h).symm ((aeval ⟨s, ⋯⟩) f)) =
    (algEquivOfTranscendental R s h).toEquiv f

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ (algEquivOfTranscendental R s h).toEquiv ((algEquivOfTranscendental R s h).symm ⟨s, ⋯⟩) =
    (algEquivOfTranscendental R s h).toEquiv X

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (G i✝) M).compr₂ₛₗ
          ((toDirectLimit f M ∘ₗ fromDirectLimit f M) ∘ₗ
            of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝ =
    (((mk R (G i✝) M).compr₂ₛₗ
          (LinearMap.id ∘ₗ of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ (fromDirectLimit f M ∘ₗ toDirectLimit f M) ∘ₗ of R ι G f i✝) x✝¹) x✝ =
    (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ LinearMap.id ∘ₗ of R ι G f i✝) x✝¹) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x : G i ⊗[R] M
⊢ (directLimitLeft f M) ((LinearMap.rTensor M (of R ι G f i)) 0) =
    (of R ι (fun i ↦ G i ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
F : DirectLimit G f →ₗ[R] P
i j : ι
hij : i ≤ j
x : G i
⊢ (F ∘ₗ of R ι G f j) ((f i j hij) x) = (F ∘ₗ of R ι G f i) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (fun i ↦ F ∘ₗ of R ι G f i) ⋯ ∘ₗ of R ι G f i✝) x✝ = (F ∘ₗ of R ι G f i✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i j : ι
hij : i ≤ j
x : G i
⊢ (of R ι G f j) ((f i j hij) x) = (of R ι G f i) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (of R ι G f) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ (map (fun x ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (G i)
inst✝⁵ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁴ : DecidableEq ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i✝ : ι
x✝ : G i✝
⊢ ((map g₂ hg₂ ∘ₗ map g₁ hg₁) ∘ₗ of R ι G f i✝) x✝ = (map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i✝) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ piLTProj h ((equiv ⟨↑x✝, ?hj⟩) ((fun l ↦ (equiv l).symm (↑t l)) x✝)) = piLTProj h (↑t x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case hj
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ ↑x✝ ∈ Iio i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯) ∘ₗ Module.of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ Module.of R ι G f i✝) x✝

Tactic:
simp

Goal state after: