awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
P Q : Ideal B
inst_14 : P.IsPrime
inst_15 : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
B' : (G : Type u) → [inst_16 : Monoid G] → [inst_17 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
        Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
          HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
            (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (x :
            { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
              Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
                HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
                  (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) }) ↦
        Subtype.mk (p := fun (g : G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) ↦
          Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
            HSMul.hSMul (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) g
              (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P))
          ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
            (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
this : ∀ (N : OpenNormalSubgroup G), Nonempty.{u + 1} (F.obj N)
⊢ ∃ (g : G), Q = g • P
have obtain : ∀ (s : (j : OpenNormalSubgroup G) → F.obj j) (hs : s ∈ F.sections), ∃ (g : G), Q = g • P
Tactic: obtain ⟨s, hs⟩ := nonempty_sections_of_finite_cofiltered_system F
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    x
⊢ HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          x :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q
have h : LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
  (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
Tactic: have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 :=
    fun x hx n ↦ hx ⟨_, e n.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    x
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
⊢ HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          x :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q
have obtain : ∀ (x : G)
  (hx :
    Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
      (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
      (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))),
  HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q
Tactic: obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
x : G
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
⊢ HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q
have hx₁ : Eq (α := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
  (comap (Subalgebra.inclusion h)
    (HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)))
  (comap (Subalgebra.inclusion h)
    (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
Tactic: replace hx := congr(Ideal.comap (Subalgebra.inclusion h) $hx)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
P_1 : Ideal A
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
P : Ideal A
Q : Ideal B
inst_13 : Q.IsPrime
inst_14 : Q.LiesOver P
inst_15 : Algebra.IsInvariant A B G
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N : OpenNormalSubgroup G
⊢ Nonempty.{u + 1} (Functor.obj (stabilizerHomSurjectiveAuxFunctor P Q σ) N)
have this : IsScalarTower.{u_1, u_2, u_2} (A ⧸ P)
  (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
    Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
  (B ⧸ Q)
Tactic: have : IsScalarTower (A ⧸ P) (FixedPoints.subalgebra A B N.1.1 ⧸
    Q.under (FixedPoints.subalgebra A B N.1.1)) (B ⧸ Q) := IsScalarTower.of_algebraMap_eq
    (Quotient.ind fun x ↦ rfl)
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) p ↔ f ∣ p
have rw : Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) p ↔ f ∣ p
Tactic: rw [h.ker_map, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
rw : Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) p ↔ f ∣ p
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) p ↔ f ∣ p
have rw₁ : f ∣ p ↔ f ∣ p
Tactic: rw [h.ker_map, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ aeval h.root = h.map
have hX : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) X : S) ((h.map : (a : R[X]) → S) X : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ Eq (α := Subalgebra R S) R[h.root] ⊤
have rw : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑h.map : (a : R[X]) → S)
Tactic: rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, aeval_root_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : ∀ (x : R[X]), Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
⊢ h = h'
have mk : ∀ (map : R[X] →ₐ[R] S)
  (map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S))
  (ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f}))
  (eq :
    ∀ (x : R[X]),
      Eq.{v + 1} (α := S)
        (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
            x :
          S)
        ((h'.map : (a : R[X]) → S) x : S)),
  { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } = h'
Tactic: cases h
Cleared hypotheses: h, eq
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h' : IsAdjoinRoot S f
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      ((h'.map : (a : R[X]) → S) x : S)
⊢ { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } = h'
have mk : ∀ (map_1 : R[X] →ₐ[R] S)
  (map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S))
  (ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f}))
  (eq :
    ∀ (x : R[X]),
      Eq.{v + 1} (α := S)
        (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
            x :
          S)
        (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
              (a : R[X]) → S)
            x :
          S)),
  { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } =
    { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 }
Tactic: cases h'
Cleared hypotheses: h', eq
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
map : R[X] →ₐ[R] S
map_surjective : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map : (a : R[X]) → S)
ker_map : Eq (α := Ideal R[X]) (RingHom.ker map) (Ideal.span {f})
map_1 : R[X] →ₐ[R] S
map_surjective_1 : Function.Surjective.{u + 1, v + 1} (α := R[X]) (β := S) (⇑map_1 : (a : R[X]) → S)
ker_map_1 : Eq (α := Ideal R[X]) (RingHom.ker map_1) (Ideal.span {f})
eq :
  ∀ (x : R[X]),
    Eq.{v + 1} (α := S)
      (({ map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f }.map : (a : R[X]) → S)
          x :
        S)
      (({ map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 : IsAdjoinRoot S f }.map :
            (a : R[X]) → S)
          x :
        S)
⊢ { map := map, map_surjective := map_surjective, ker_map := ker_map : IsAdjoinRoot S f } =
    { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 }
have mk : map = map_1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
have rw : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
Tactic: rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
rw : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
have rw₁ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((aeval h'.root : (a : R[X]) → S) x : S)
Tactic: rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
rw : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
rw₁ : Eq.{v + 1} (α := S) ((aeval h.root : (a : R[X]) → S) x : S) ((aeval h'.root : (a : R[X]) → S) x : S)
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) x : S) ((h'.map : (a : R[X]) → S) x : S)
have rw₂ : Eq.{v + 1} (α := S) ((aeval h'.root : (a : R[X]) → S) x : S) ((aeval h'.root : (a : R[X]) → S) x : S)
Tactic: rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : AdjoinRoot f
⊢ Eq.{v + 1} (α := S) ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S) a : S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
have rw : Eq.{v + 1} (α := S)
  ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
      ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f)
          (sorry.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
        AdjoinRoot f) :
    S)
  ((h.map : (a : R[X]) → S) (sorry.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
    S)
Tactic: rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : AdjoinRoot f
rw :
  Eq.{v + 1} (α := S)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
        ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f)
            (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
          AdjoinRoot f) :
      S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
⊢ Eq.{v + 1} (α := S) ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S) a : S)
    ((h.map : (a : R[X]) → S)
        (⋯.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
      S)
have rw₁ : Eq.{v + 1} (α := S)
  ((h.map : (a : R[X]) → S) (sorry.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
    S)
  ((h.map : (a : R[X]) → S) (sorry.choose (p := fun (a_1 : R[X]) ↦ (AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) a_1 = a)) :
    S)
Tactic: rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : S
⊢ Eq.{u + 1} (α := AdjoinRoot f) ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) a : AdjoinRoot f)
    ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
have rw : a =
  (h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
    ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
Tactic: rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : S
rw :
  a =
    (h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
      ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
⊢ Eq.{u + 1} (α := AdjoinRoot f) ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) a : AdjoinRoot f)
    ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
have rw₁ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr a) : S)
  ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
      ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f) :
    S)
Tactic: rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
a : S
rw :
  a =
    (h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
      ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
rw₁ :
  Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr a) : S)
    ((h.adjoinRootAlgEquiv : (a : AdjoinRoot f) → S)
        ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f) :
      S)
⊢ Eq.{u + 1} (α := AdjoinRoot f) ((h.adjoinRootAlgEquiv.symm : (a : S) → AdjoinRoot f) a : AdjoinRoot f)
    ((AdjoinRoot.mk f : (a : R[X]) → AdjoinRoot f) (h.repr a) : AdjoinRoot f)
have rw₂ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr a) : S) ((h.map : (a : R[X]) → S) (h.repr a) : S)
Tactic: rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
⊢ (↑(h.algEquiv h') : S →ₐ[R] T).comp h.map = h'.map
have hX : Eq.{u_1 + 1} (α := T) (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) X : T)
  ((h'.map : (a : R[X]) → T) X : T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ Eq.{u_1 + 1} (α := T) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
    ((h'.map : (a : R[X]) → T) z : T)
have rw : Eq.{u_1 + 1} (α := T) ((h.algEquiv h' : (a : S) → T) ((h.map : (a : R[X]) → S) z : S) : T)
  (((↑(h.algEquiv h') : S →ₐ[R] T).comp h.map : (a : R[X]) → T) z : T)
Tactic: rw [← h.algEquiv_map h']
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ h.algEquiv h = AlgEquiv.refl
have h₁ : ∀ (a : S), Eq (α := S) ((h.algEquiv h : (a : S) → S) a : S) ((AlgEquiv.refl : (a : S) → S) a : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
h'' : IsAdjoinRoot U f
⊢ (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''
have h₁ : ∀ (a : S),
  Eq.{u_2 + 1} (α := U) (((h.algEquiv h').trans (h'.algEquiv h'') : (a : S) → U) a : U)
    ((h.algEquiv h'' : (a : S) → U) a : U)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
e : S ≃ₐ[R] T
⊢ Eq (α := Ideal R[X]) (RingHom.ker ((↑e : S →ₐ[R] T).comp h.map)) (Ideal.span {f})
have h₁ : ∀ (x : R[X]),
  Membership.mem (γ := Ideal R[X]) (RingHom.ker ((↑e : S →ₐ[R] T).comp h.map)) x ↔
    Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst_3 : Ring T
inst_4 : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst_5 : Ring U
inst_6 : Algebra R U
e : T ≃ₐ[R] U
⊢ h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e
have h₁ : ∀ (a : S),
  Eq.{u_2 + 1} (α := U) ((h.algEquiv (h'.ofAlgEquiv e) : (a : S) → U) a : U)
    (((h.algEquiv h').trans e : (a : S) → U) a : U)
Tactic: ext a