awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ.symm : (a : k) → k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) : k) :
      k)
have refine_1 : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
    k)
  ((σ.symm : (a : k) → k)
      ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) : k) :
    k)
Tactic: rw [← h₁, ← e, h₂]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_1 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ.symm : (a : k) → k)
        ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) :
          k) :
      k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ.symm : (a : k) → k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) : k) :
      k)
have refine_1₁ : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y) : B ⧸ Q) : k)
  ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
Tactic: rw [← h₁, ← e, h₂]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_1 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ.symm : (a : k) → k)
        ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) :
          k) :
      k)
refine_1₁ :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y) : B ⧸ Q) : k)
    ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ.symm : (a : k) → k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) : k) :
      k)
have refine_1₂ : Eq (α := k)
  ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
  ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
Tactic: rw [← h₁, ← e, h₂]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x : B ⧸ Q
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x) = x
have refine_2 : ∀ (x : B),
  (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x : B
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x
have refine_2 : ∀ (y : B)
  (e :
    Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q)
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)),
  (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x
Tactic: obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₂ (Ideal.Quotient.mk Q x))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x
have refine_2 : Eq.{u_3 + 1} (α := k)
  ((f : (a : B ⧸ Q) → k)
      ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x))) :
    k)
  ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ Eq.{u_3 + 1} (α := k)
    ((f : (a : B ⧸ Q) → k)
        ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
          ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x))) :
      k)
    ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have refine_2 : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
      ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
    k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
Tactic: dsimp [f] at h₁ h₂ ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have refine_2 : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
      ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
    k)
  ((σ : (a : k) → k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) : k) :
    k)
Tactic: refine .trans ?_ (σ.apply_symm_apply _)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) :
          k) :
      k)
have refine_2 : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
      ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
    k)
  ((σ : (a : k) → k)
      ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) : k) :
    k)
Tactic: rw [← h₂, ← e, h₁]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) :
          k) :
      k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) :
          k) :
      k)
have refine_2₁ : Eq.{u_3 + 1} (α := k)
  ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y) : B ⧸ Q) : k)
  ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
Tactic: rw [← h₂, ← e, h₁]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgEquiv.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (x : B ⧸ Q),
    Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) :
          k) :
      k)
refine_2₁ :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y) : B ⧸ Q) : k)
    ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) :
          k) :
      k)
have refine_2₂ : Eq (α := k) ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
  ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
Tactic: rw [← h₂, ← e, h₁]