awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h :
  ∃ (x : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x_1 : Kˣ), spanSingleton R⁰ (↑x_1 : K) = (↑x : FractionalIdeal R⁰ K)) ∧
      ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
              MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
          x =
        I
u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K)
hu :
  ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
          MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
      u =
    I
⊢ Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰
      (↑(((Units.map (↑(RingEquiv.toRingHom (IsFractionRing.ringEquivOfRingEquiv f)) : K →* L) :
                MonoidHom.{u_2, u_4} Kˣ Lˣ) :
              (a : Kˣ) → Lˣ)
            v) :
        L))
    (↑(((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
              MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
          u) :
      FractionalIdeal S⁰ L)
have h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
  (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
    FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
  (((ringEquivOfRingEquiv K L f :
          RingEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)) :
        (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
      (spanSingleton R⁰ (↑v : K)) :
    FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
Tactic: simp only [RingEquiv.toRingHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe,
      Units.coe_mapEquiv, ← huv, RingEquiv.coe_toMulEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h :
  ∃ (x : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x_1 : Kˣ), spanSingleton R⁰ (↑x_1 : K) = (↑x : FractionalIdeal R⁰ K)) ∧
      ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
              MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
          x =
        I
u : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ (↑v : K) = (↑u : FractionalIdeal R⁰ K)
hu :
  ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
          MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
      u =
    I
⊢ Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
    (((ringEquivOfRingEquiv K L f :
            RingEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
              (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)) :
          (a : FractionalIdeal R⁰ K) → FractionalIdeal S⁰ L)
        (spanSingleton R⁰ (↑v : K)) :
      FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
have h : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
  (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
    FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
  (spanSingleton S⁰ ((IsFractionRing.ringEquivOfRingEquiv f : (a : K) → L) (↑v : K)) :
    FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)
Tactic: rw [FractionalIdeal.ringEquivOfRingEquiv_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ ∃ (x : (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ),
    (∃ (x_1 : Kˣ), spanSingleton R⁰ (↑x_1 : K) = (↑x : FractionalIdeal R⁰ K)) ∧
      ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
              MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
                (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
            (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
          x =
        I
have h : (∃ (x : Kˣ),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
      (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
              (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)) ∧
  ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
          MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
        (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
      ((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
          (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I) =
    I
Tactic: use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ (∃ (x : Kˣ),
      Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
        (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
                (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
              I) :
          FractionalIdeal R⁰ K)) ∧
    ((Units.mapEquiv (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_2, u_4} (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)ˣ
              (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ) :
          (a : (FractionalIdeal R⁰ K)ˣ) → (FractionalIdeal S⁰ L)ˣ)
        ((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) =
      I
have h : ∃ (x : Kˣ),
  Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) :
      FractionalIdeal R⁰ K)
Tactic: refine ⟨?_, by simp [← Units.val_inj]⟩
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ ∃ (x : Kˣ),
    Eq (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (spanSingleton R⁰ (↑x : K))
      (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
              (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
            I) :
        FractionalIdeal R⁰ K)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (spanSingleton R⁰
    (↑(((Units.map (↑(RingEquiv.toRingHom (RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f))) : L →* K) :
              MonoidHom.{u_4, u_2} Lˣ Kˣ) :
            (a : Lˣ) → Kˣ)
          u) :
      K))
  (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
          (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
        I) :
    FractionalIdeal R⁰ K)
Tactic: use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
        (L := L)).symm.toRingHom u
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰
      (↑(((Units.map (↑(RingEquiv.toRingHom (RingEquiv.symm (IsFractionRing.ringEquivOfRingEquiv f))) : L →* K) :
                MonoidHom.{u_4, u_2} Lˣ Kˣ) :
              (a : Lˣ) → Kˣ)
            u) :
        K))
    (↑((Units.mapEquiv (RingEquiv.toMulEquiv (RingEquiv.symm (ringEquivOfRingEquiv K L f))) :
            (a : (FractionalIdeal S⁰ L)ˣ) → (FractionalIdeal R⁰ K)ˣ)
          I) :
      FractionalIdeal R⁰ K)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (spanSingleton R⁰ ((IsFractionRing.ringEquivOfRingEquiv f.symm : (a : L) → K) (↑u : L)) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
          MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
        (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
      (↑I : FractionalIdeal S⁰ L) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe,
        Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe,
        RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.ClassGroup (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
S : Type u_3
L : Type u_4
inst_5 : CommRing S
inst_6 : IsDomain S
inst_7 : Field L
inst_8 : Algebra S L
inst_9 : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L)ˣ
h : ∃ (x : Lˣ), spanSingleton S⁰ (↑x : L) = (↑I : FractionalIdeal S⁰ L)
u : Lˣ
hu : spanSingleton S⁰ (↑u : L) = (↑I : FractionalIdeal S⁰ L)
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((IsFractionRing.ringEquivOfRingEquiv f.symm : (a : L) → K) (↑u : L)) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
            MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
          (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
        (↑I : FractionalIdeal S⁰ L) :
      FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (((RingEquiv.symm (ringEquivOfRingEquiv K L f) :
          RingEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
        (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
      (↑I : FractionalIdeal S⁰ L) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (((MulEquiv.symm (↑(ringEquivOfRingEquiv K L f) : FractionalIdeal R⁰ K ≃* FractionalIdeal S⁰ L) :
          MulEquiv.{u_4, u_2} (FractionalIdeal.{u_3, u_4} (R := S) S⁰ L) (FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)) :
        (a : FractionalIdeal S⁰ L) → FractionalIdeal R⁰ K)
      (↑I : FractionalIdeal S⁰ L) :
    FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq (α := A ⊗[R] A ⊗[R] A)
    ((LinearEquiv.symm (TensorProduct.assoc R A A A) : (a : A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] A)
        ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] A ⊗[R] A)
    ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a) : A ⊗[R] A ⊗[R] A)
have rw : Eq (α := A ⊗[R] (A ⊗[R] A))
  ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
    A ⊗[R] (A ⊗[R] A))
  ((TensorProduct.assoc R A A A : (a : A ⊗[R] A ⊗[R] A) → A ⊗[R] (A ⊗[R] A))
      ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a)) :
    A ⊗[R] (A ⊗[R] A))
Tactic: rw [(TensorProduct.assoc R A A A).symm_apply_eq, coassoc_apply a]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
rw :
  Eq (α := A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
      A ⊗[R] (A ⊗[R] A))
    ((TensorProduct.assoc R A A A : (a : A ⊗[R] A ⊗[R] A) → A ⊗[R] (A ⊗[R] A))
        ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] (A ⊗[R] A))
⊢ Eq (α := A ⊗[R] A ⊗[R] A)
    ((LinearEquiv.symm (TensorProduct.assoc R A A A) : (a : A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] A)
        ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a)) :
      A ⊗[R] A ⊗[R] A)
    ((LinearMap.rTensor A comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) a) : A ⊗[R] A ⊗[R] A)
have rw₁ : Eq (α := A ⊗[R] (A ⊗[R] A))
  ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
    A ⊗[R] (A ⊗[R] A))
  ((LinearMap.lTensor A comul : (a : A ⊗[R] A) → A ⊗[R] (A ⊗[R] A)) ((comul : (a : A) → A ⊗[R] A) a) :
    A ⊗[R] (A ⊗[R] A))
Tactic: rw [(TensorProduct.assoc R A A A).symm_apply_eq, coassoc_apply a]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
⊢ Eq (α := R ⊗[R] B)
    (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] (f : (a : A) → B) (repr.right i) : R ⊗[R] B)
    (1 ⊗ₜ[R] (f : (a : A) → B) a : R ⊗[R] B)
have this : Eq (α := R ⊗[R] A) (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) (1 ⊗ₜ[R] a)
Tactic: have := sum_counit_tmul_eq repr
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this : Eq (α := R ⊗[R] A) (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) (1 ⊗ₜ[R] a)
⊢ Eq (α := R ⊗[R] B)
    (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] (f : (a : A) → B) (repr.right i) : R ⊗[R] B)
    (1 ⊗ₜ[R] (f : (a : A) → B) a : R ⊗[R] B)
have this₁ : Eq (α := R ⊗[R] B)
  ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : R ⊗[R] A) → R ⊗[R] B)
      (∑ i ∈ repr.index, (counit : (a : A) → R) (repr.left i) ⊗ₜ[R] repr.right i) :
    R ⊗[R] B)
  ((LinearMap.lTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : R ⊗[R] A) → R ⊗[R] B)
      (1 ⊗ₜ[R] a) :
    R ⊗[R] B)
Tactic: apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
⊢ Eq (α := B ⊗[R] R)
    (∑ i ∈ repr.index, (f : (a : A) → B) (repr.left i) ⊗ₜ[R] (counit : (a : A) → R) (repr.right i) : B ⊗[R] R)
    ((f : (a : A) → B) a ⊗ₜ[R] 1 : B ⊗[R] R)
have this : Eq (α := A ⊗[R] R) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) (a ⊗ₜ[R] 1)
Tactic: have := sum_tmul_counit_eq repr
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f : F
a : A
repr : Repr.{u, v, u_3} R a
this : Eq (α := A ⊗[R] R) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) (a ⊗ₜ[R] 1)
⊢ Eq (α := B ⊗[R] R)
    (∑ i ∈ repr.index, (f : (a : A) → B) (repr.left i) ⊗ₜ[R] (counit : (a : A) → R) (repr.right i) : B ⊗[R] R)
    ((f : (a : A) → B) a ⊗ₜ[R] 1 : B ⊗[R] R)
have this₁ : Eq (α := B ⊗[R] R)
  ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : A ⊗[R] R) → B ⊗[R] R)
      (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] (counit : (a : A) → R) (repr.right i)) :
    B ⊗[R] R)
  ((LinearMap.rTensor R (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : A ⊗[R] R) → B ⊗[R] R)
      (a ⊗ₜ[R] 1) :
    B ⊗[R] R)
Tactic: apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f g h : F
a : A
repr : Repr.{u, v, u_3} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_4} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_5} R (repr.right i)
⊢ Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₂ i).index,
        (f : (a : A) → B) (repr.left i) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₂ i).left j) ⊗ₜ[R] (h : (a : A) → B) ((a₂ i).right j)))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₁ i).index,
        (f : (a : A) → B) ((a₁ i).left j) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₁ i).right j) ⊗ₜ[R] (h : (a : A) → B) (repr.right i)))
have this : Eq.{v + 1} (α := A ⊗[R] (A ⊗[R] A))
  (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i))
  (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))
Tactic: have := sum_tmul_tmul_eq repr a₁ a₂
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
B : Type u_1
inst_4 : AddCommMonoid B
inst_5 : Module R B
F : Type u_2
inst_6 : FunLike F A B
inst_7 : LinearMapClass F R A B
f g h : F
a : A
repr : Repr.{u, v, u_3} R a
a₁ : (i : repr.ι) → Repr.{u, v, u_4} R (repr.left i)
a₂ : (i : repr.ι) → Repr.{u, v, u_5} R (repr.right i)
this :
  Eq.{v + 1} (α := A ⊗[R] (A ⊗[R] A))
    (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i))
    (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j))
⊢ Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₂ i).index,
        (f : (a : A) → B) (repr.left i) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₂ i).left j) ⊗ₜ[R] (h : (a : A) → B) ((a₂ i).right j)))
    (∑ i ∈ repr.index,
      ∑ j ∈ (a₁ i).index,
        (f : (a : A) → B) ((a₁ i).left j) ⊗ₜ[R]
          ((g : (a : A) → B) ((a₁ i).right j) ⊗ₜ[R] (h : (a : A) → B) (repr.right i)))
have this₁ : Eq.{u_1 + 1} (α := B ⊗[R] (B ⊗[R] B))
  ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
        (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
      (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
    (∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i)))
  ((TensorProduct.map (↑f : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
        (TensorProduct.map (↑g : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
          (↑h : [inst_8 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)) :
      (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
    (∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)))
Tactic: apply_fun TensorProduct.map (f : A →ₗ[R] B)
    (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) LinearMap.id
have this : Eq (α := A →ₗ[R] R ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
  ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
Tactic: have := rTensor_counit_comp_comul (R := R) (A := A)
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] R ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) LinearMap.id
have this₁ : Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ LinearMap.rTensor A counit ∘ₗ comul)
  (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
Tactic: apply_fun (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ ·) at this
Cleared hypotheses: this