awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial A →ₐ[A] k) :
          (a : Polynomial A) → k)
        P :
      k)
    (0 : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have this₁ : Eq.{u_3 + 1} (α := k)
  (((Polynomial.aeval
            ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
          Polynomial B →ₐ[B] k) :
        (a : Polynomial B) → k)
      (MulSemiringAction.charpoly G x) :
    k)
  (0 : k)
Tactic: rw [← Polynomial.aeval_map_algebraMap B, ← Polynomial.coe_mapRingHom, hp] at this
Cleared hypotheses: this
-- 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_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P_1) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this_2 : IsScalarTower A B k
P : Polynomial A
hp :
  Eq.{u_2 + 1} (α := Polynomial B)
    (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
          (a : Polynomial A) → Polynomial B)
        P :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
this_3 : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
this :
  Eq.{u_3 + 1} (α := k)
    (((Polynomial.aeval
              ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)) :
            Polynomial B →ₐ[B] k) :
          (a : Polynomial B) → k)
        (MulSemiringAction.charpoly G x) :
      k)
    (0 : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have intro : ∀ (τ : G)
  (hτ :
    Eq (α := k) ((σ : (a : k) → k) ((algebraMap B k : (a : B) → k) x : k) : k)
      ((algebraMap B k : (a : B) → k) (τ • x) : k)),
  Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
Tactic: obtain ⟨τ, hτ⟩ : ∃ τ : G, σ (algebraMap _ _ x) = algebraMap _ _ (τ • x) := by
    simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using this
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
⊢ ∃ (τ : 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)
have hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
Tactic: have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _
-- 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)
⊢ ∃ (τ : 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)
have 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)
Tactic: obtain ⟨τ₁, h₁⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.toAlgHom
-- 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)
⊢ ∃ (τ : 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)
have 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)
Tactic: obtain ⟨τ₂, h₂⟩ := Ideal.Quotient.exists_algHom_fixedPoint_quotient_under G P Q σ.symm.toAlgHom
-- 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)
⊢ ∃ (τ : 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)
have refine_1 : Function.LeftInverse (⇑τ₂ : (a : B ⧸ Q) → B ⧸ Q) (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
Tactic: refine ⟨{ __ := τ₁, invFun := τ₂, left_inv := ?_, right_inv := ?_ }, 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)
refine_1 :
  Function.LeftInverse (⇑τ₂ : (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)
have refine_2 : Function.RightInverse (⇑τ₂ : (a : B ⧸ Q) → B ⧸ Q) (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
Tactic: refine ⟨{ __ := τ₁, invFun := τ₂, left_inv := ?_, right_inv := ?_ }, 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
⊢ (τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun x) = x
have 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)
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
⊢ 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)
have 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)
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)
⊢ 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)
have 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)
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)
        ((τ₂ : (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)
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)
  ((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_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)
Tactic: refine .trans ?_ (σ.symm_apply_apply _)