mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n)) = ↑f n

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) (Quotient.out (↑f n)) = ↑f n
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
hx : (ofPowSMul I M n) x = 0
⊢ x = 0

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I ↥(I ^ n • ⊤)
hx : (ofPowSMul I M n) x = 0
⊢ x = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝)) = (coeff n✝) x✝

Tactic:
;

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (toAdicCompletionInv σ R ((↑↑(toAdicCompletion σ R).toRingHom).toFun x✝)) = (coeff n✝) x✝
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
x✝ : R
n✝ : ℕ
⊢ ↑(((↑(ofAlgEquiv I)).comp (liftRingHom I f ⋯)) x✝) n✝ = ↑((AdicCompletion.liftRingHom I f ⋯) x✝) n✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
x✝ : R
n✝ : ℕ
⊢ ↑(((↑(ofAlgEquiv I)).comp (liftRingHom I f ⋯)) x✝) n✝ = ↑((AdicCompletion.liftRingHom I f ⋯) x✝) n✝
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x✝ : R
⊢ ((Ideal.Quotient.mk (I ^ n)).comp (liftRingHom I f ⋯)) x✝ = (f n) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
n : ℕ
x✝ : R
⊢ ((Ideal.Quotient.mk (I ^ n)).comp (liftRingHom I f ⋯)) x✝ = (f n) x✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
n✝ : ℕ
⊢ ↑((↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝)) n✝ = ↑x✝ n✝

Tactic:
;

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
n✝ : ℕ
⊢ ↑((↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝)) n✝ = ↑x✝ n✝
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
n✝ : ℕ
⊢ ↑((↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝)) n✝ = ↑x✝ n✝

Tactic:
simpa using! mk_truncTotal_toAdicCompletionInv

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
this :
  (ConcreteCategory.hom ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B

Tactic:
;

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
this :
  (ConcreteCategory.hom ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) i = ↑x i
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x✝ : R
⊢ ((factorPow I hle).comp ((factorPow I ⋯).comp (f n✝))) x✝ = ((factorPow I ⋯).comp (f m✝)) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x✝ : R
⊢ ((factorPow I hle).comp ((factorPow I ⋯).comp (f n✝))) x✝ = ((factorPow I ⋯).comp (f m✝)) x✝
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
n : ℕ
x✝ : R
⊢ ((Ideal.Quotient.mk (I ^ a n)).comp (liftRingHom I ha f ⋯)) x✝ = (f n) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
n : ℕ
x✝ : R
⊢ ((Ideal.Quotient.mk (I ^ a n)).comp (liftRingHom I ha f ⋯)) x✝ = (f n) x✝
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : ↑x n = 0
⊢ (ofPowSMul I M n) (ofValEqZero I hx) = x

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hx : ↑x n = 0
⊢ (ofPowSMul I M n) (ofValEqZero I hx) = x
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⋯
⊢ ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⋯
⊢ ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
⊢ x ∈ RingHom.ker (evalOneₐ I).toRingHom ↔ x ∈ (eval I R 1).ker

Tactic:
have eq : I ^ 1 * ⊤ = I := by simp
    have : Function.Injective (Ideal.Quotient.factor ((le_of_eq eq))) := by
      simpa [RingHom.injective_iff_ker_eq_bot, Ideal.Quotient.factor_ker]
        using Ideal.map_mk_eq_bot_of_le (le_of_eq eq.symm)
    simpa [← factorₐ_evalₐ_one, ← factor_eval_eq_evalₐ] using map_eq_zero_iff _ this

Goal state after:
Module: Mathlib.RingTheory.Artinian.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsIntegral R A
x✝ : A
⊢ x✝ ∈ IsUnit.submonoid A ↔ x✝ ∈ A⁰
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ ⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv ∘ X =
    ⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ∘ MvPolynomial.X

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ ⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv ∘ X =
    ⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ∘ MvPolynomial.X
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ (TensorProduct.map (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x)
        (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x))
      (comul a) =
    (TensorProduct.map (lsingle x) (lsingle x)) (comul a)

Tactic:
;

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ (TensorProduct.map (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x)
        (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x))
      (comul a) =
    (TensorProduct.map (lsingle x) (lsingle x)) (comul a)
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R 0
⊢ False

Tactic:
;

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : Nontrivial R
ha : IsGroupLikeElem R 0
⊢ False
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ (TensorProduct.map ↑f ↑f) (a ⊗ₜ[R] a) = f a ⊗ₜ[R] f a

Tactic:
;

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ (TensorProduct.map ↑f ↑f) (a ⊗ₜ[R] a) = f a ⊗ₜ[R] f a
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ ∀ ⦃a₂ : GroupLike R A⦄, ↑{ val := a, isGroupLikeElem_val := ha } = ↑a₂ → { val := a, isGroupLikeElem_val := ha } = a₂

Tactic:
;

Goal state after:
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ ∀ ⦃a₂ : GroupLike R A⦄, ↑{ val := a, isGroupLikeElem_val := ha } = ↑a₂ → { val := a, isGroupLikeElem_val := ha } = a₂
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ d • ∑ x ∈ s, c x • x ⊗ₜ[R] x = d • comul (∑ a ∈ s, c a • a)

Tactic:
;

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ d • ∑ x ∈ s, c x • x ⊗ₜ[R] x = d • comul (∑ a ∈ s, c a • a)
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
i : ι × κ
⊢ ((Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i) 1 =
    ((TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
          ↑(finsuppTensorFinsupp' R ι κ).symm) ∘ₗ
        Finsupp.lsingle i)
      1

Tactic:
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map LinearMap.id I.mkQ ∘ₗ ↑(TensorProduct.lid R C).symm = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

Tactic:
;

Goal state after:
case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map LinearMap.id I.mkQ ∘ₗ ↑(TensorProduct.lid R C).symm = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
CoassocSimps.map_counit_comp_comul_right

Goal state after:
case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ LinearMap.id ∘ₗ ↑(TensorProduct.rid R C).symm = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ LinearMap.id ∘ₗ ↑(TensorProduct.rid R C).symm = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
;

Goal state after:
case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ LinearMap.id ∘ₗ ↑(TensorProduct.rid R C).symm = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ Bialgebra R (A ⧸ I)

Tactic:
refine .ofAlgHom (comulAlgHom I) (counitAlgHom I) ?_ ?_ ?_ <;>
    refine Ideal.Quotient.algHom_ext R (AlgHom.toLinearMap_injective ?_)

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((↑(Algebra.TensorProduct.assoc R R R (A ⧸ I) (A ⧸ I) (A ⧸ I))).comp
            ((Algebra.TensorProduct.map (comulAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I))).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (comulAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (counitAlgHom I) (AlgHom.id R (A ⧸ I))).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap

case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ (((Algebra.TensorProduct.map (AlgHom.id R (A ⧸ I)) (counitAlgHom I)).comp (comulAlgHom I)).comp
        (Ideal.Quotient.mkₐ R I)).toLinearMap =
    ((↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).comp (Ideal.Quotient.mkₐ R I)).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map LinearMap.id ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
      ↑(TensorProduct.lid R A).symm =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
;

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map LinearMap.id ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
      ↑(TensorProduct.lid R A).symm =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) counit ∘ₗ comul =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
CoassocSimps.map_counit_comp_comul_right

Goal state after:
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R A).symm =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R A).symm =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
;

Goal state after:
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R A).symm =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (↑((Algebra.TensorProduct.map algebraMapInv (AlgHom.id R (SymmetricAlgebra R M))).comp
            (lift
              ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
                (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))) ∘ₗ
        ι R M)
      x =
    (↑↑(Algebra.TensorProduct.lid R (SymmetricAlgebra R M)).symm ∘ₗ ι R M) x

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (↑((Algebra.TensorProduct.map algebraMapInv (AlgHom.id R (SymmetricAlgebra R M))).comp
            (lift
              ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
                (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))) ∘ₗ
        ι R M)
      x =
    (↑↑(Algebra.TensorProduct.lid R (SymmetricAlgebra R M)).symm ∘ₗ ι R M) x
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (↑((Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv).comp
            (lift
              ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
                (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))) ∘ₗ
        ι R M)
      x =
    (↑↑(Algebra.TensorProduct.rid R R (SymmetricAlgebra R M)).symm ∘ₗ ι R M) x

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (↑((Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv).comp
            (lift
              ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
                (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))) ∘ₗ
        ι R M)
      x =
    (↑↑(Algebra.TensorProduct.rid R R (SymmetricAlgebra R M)).symm ∘ₗ ι R M) x
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I) =
    (FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I)

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I) =
    (FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I)