awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
obtain :
  ∀ (τ₁ : 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)),
    ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
      ∀ (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)
⊢ ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (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)

Tactic:
obtain ⟨τ₁, h₁⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.toAlgHom

Premises used: Ideal.Quotient.exists_algHom_fixedPoint_quotient_under, AlgEquiv.toAlgHom
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
obtain :
  ∀ (τ₂ : 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)),
    ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
      ∀ (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)
⊢ ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (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)

Tactic:
obtain ⟨τ₂, h₂⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.symm.toAlgHom

Premises used: Ideal.Quotient.exists_algHom_fixedPoint_quotient_under, AlgEquiv.toAlgHom, AlgEquiv.symm
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
⊢ ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (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)

Tactic:
⟨{ __ := τ₁, invFun := τ₂, left_inv := ?_, right_inv := ?_ }, h₁⟩

Premises used: RingHom.map_add', AlgHom.commutes', Equiv.mk, AlgEquiv.mk, OneHom.toFun, AlgHom.toRingHom, Exists.intro, MonoidHom.toOneHom, MonoidHom.map_mul', RingHom.toMonoidHom, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
refine_1 :
  Function.LeftInverse (⇑τ₂ : (a : B ⧸ Q) → B ⧸ Q) (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
refine_2 :
  Function.RightInverse (⇑τ₂ : (a : B ⧸ Q) → B ⧸ Q) (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
⊢ ∃ (τ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (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)

Tactic:
refine ⟨{ __ := τ₁, invFun := τ₂, left_inv := ?_, right_inv := ?_ }, h₁⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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
refine_1 :
  ∀ (x : B),
    Eq (α := B ⧸ Q)
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
          ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
        B ⧸ Q)
      ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)
⊢ (τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun x) = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
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
refine_1 :
  ∀ (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 (α := B ⧸ Q)
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
          ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
        B ⧸ Q)
      ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)
⊢ Eq (α := B ⧸ Q)
    ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
        ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
      B ⧸ Q)
    ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)

Tactic:
obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₁ (Ideal.Quotient.mk Q x))

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
refine_1 :
  Eq.{u_3 + 1} (α := k)
    ((f : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
            ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
          B ⧸ Q) :
      k)
    ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Eq (α := B ⧸ Q)
    ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
        ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
      B ⧸ Q)
    ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)

Tactic:
apply hf
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
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)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Eq.{u_3 + 1} (α := k)
    ((f : (a : B ⧸ Q) → k)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q)
            ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((mk Q : (a : B) → B ⧸ Q) x)) :
          B ⧸ Q) :
      k)
    ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
dsimp [f] at h₁ h₂ ⊢
-- Module: Mathlib.RingTheory.Invariant.Basic
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)

Tactic:
.trans ?_ (σ.symm_apply_apply _)

Premises used: AlgEquiv.symm_apply_apply, Eq.trans
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) : 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)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
refine .trans ?_ (σ.symm_apply_apply _)
-- Module: Mathlib.RingTheory.Invariant.Basic
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)
refine_1₂ 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)
⊢ 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)

Tactic:
rw [← h₁, ← e, h₂]
-- Module: Mathlib.RingTheory.Invariant.Basic
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
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
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) x) = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl