awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
rw :
  dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₁ :
  dp S n
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) (β := N) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₂ :
  HSMul.hSMul (β := DividedPowerAlgebra S N) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₃ :
  HSMul.hSMul (α := S) (β := DividedPowerAlgebra S N) ((algebraMap R S : (a : R) → S) (r ^ n) : S)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₄ rw₅ :
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)

Tactic:
rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]

Premises used: algebra_compatible_smul, algebraMap_smul, map_pow, LinearMap.map_smul, DividedPowerAlgebra.dp_smul, DFunLike.coe
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
rw :
  Eq (α := DividedPowerAlgebra S N)
    ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) ⋯ ⋯ ⋯ ⋯ :
          (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
rw₁ rw₂ :
  Eq (α := DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)

Tactic:
rw [map, lift'_apply]

Premises used: DividedPowerAlgebra.lift'_apply, DividedPowerAlgebra.map
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
a : M
rw :
  Eq (α := DividedPowerAlgebra S N)
    ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) ⋯ ⋯ ⋯ ⋯ :
          (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        (dp R n a) :
      DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₁ rw₂ :
  Eq (α := DividedPowerAlgebra S N) (dp S (n, a).1 ((f : (a : M) → N) (n, a).2) : DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N) (dp R n a) : DividedPowerAlgebra S N)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)

Tactic:
rw [map, lift'_apply_dp]

Premises used: DividedPowerAlgebra.map, DividedPowerAlgebra.lift'_apply_dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
m : M
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((embed R M : (a : M) → DividedPowerAlgebra R M) m) :
      DividedPowerAlgebra S N)
    ((embed S N : (a : N) → DividedPowerAlgebra S N) ((f : (a : M) → N) m) : DividedPowerAlgebra S N)

Tactic:
simp [embed_def, map_apply_dp]

Premises used: DividedPowerAlgebra.map_apply_dp, DividedPowerAlgebra.embed_def
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
h :
  ∀ (x : M),
    Eq (α := DividedPowerAlgebra S N)
      ((AlgHom.toLinearMap (map S f) ∘ₗ embed R M : (a : M) → DividedPowerAlgebra S N) x : DividedPowerAlgebra S N)
      (((↑R :
                  {S : Type u_3} →
                    {M : Type u_4} →
                      {M₂ : Type (max u_3 u_4)} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (embed S N) ∘ₗ
              f :
            (a : M) → DividedPowerAlgebra S N)
          x :
        DividedPowerAlgebra S N)
⊢ Eq (α := M →ₗ[R] DividedPowerAlgebra S N) (AlgHom.toLinearMap (map S f) ∘ₗ embed R M)
    ((↑R :
          {S : Type u_3} →
            {M : Type u_4} →
              {M₂ : Type (max u_3 u_4)} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (embed S N) ∘ₗ
      f)

Tactic:
ext
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
x : M
⊢ Eq (α := DividedPowerAlgebra S N)
    ((AlgHom.toLinearMap (map S f) ∘ₗ embed R M : (a : M) → DividedPowerAlgebra S N) x : DividedPowerAlgebra S N)
    (((↑R :
                {S : Type u_3} →
                  {M : Type u_4} →
                    {M₂ : Type (max u_3 u_4)} →
                      [inst : Semiring R] →
                        [inst_9 : Semiring S] →
                          [inst_10 : AddCommMonoid M] →
                            [inst_11 : AddCommMonoid M₂] →
                              [inst_12 : Module R M] →
                                [inst_13 : Module R M₂] →
                                  [inst_14 : Module S M] →
                                    [inst_15 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (embed S N) ∘ₗ
            f :
          (a : M) → DividedPowerAlgebra S N)
        x :
      DividedPowerAlgebra S N)

Tactic:
simp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw :
  Set.range X ⊆
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
⊢ Function.Surjective (α := DividedPowerAlgebra R M) (β := DividedPowerAlgebra R N)
    (⇑(map R f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R N)

Tactic:
rw [← AlgHom.range_eq_top, ← Algebra.map_top (map R f), eq_top_iff,
    ← (AlgHom.range_eq_top (mkAlgHom R (Rel R N))).mpr mkAlgHom_surjective,
    ← Algebra.map_top, (Subalgebra.gc_map_comap _).le_iff_le, ← MvPolynomial.adjoin_range_X,
    Algebra.adjoin_le_iff]

Premises used: Iff.mpr, eq_top_iff, GaloisConnection.le_iff_le, MvPolynomial.adjoin_range_X, Subalgebra.gc_map_comap, DividedPowerAlgebra.Rel, RingQuot.mkAlgHom, AlgHom.range_eq_top, DividedPowerAlgebra.mkAlgHom_surjective, DividedPowerAlgebra.map, Algebra.adjoin_le_iff, Algebra.map_top
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
a : MvPolynomial.{u_4, u_1} (ℕ × N) R
simp :
  (∃ (a_1 : ℕ) (b : N), X (a_1, b) = a) →
    a ∈
      (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
            (Subalgebra.map (map R f) ⊤)) :
        Set (MvPolynomial (ℕ × N) R))
⊢ Membership.mem (γ := Set (MvPolynomial.{u_4, u_1} (ℕ × N) R)) (Set.range X) a →
    a ∈
      (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
            (Subalgebra.map (map R f) ⊤)) :
        Set (MvPolynomial (ℕ × N) R))

Tactic:
simp only [Set.mem_range, Prod.exists]

Premises used: Set.mem_range, Prod.exists
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
m : N
obtain :
  ∀ (l : M),
    Membership.mem (α := MvPolynomial.{u_4, u_1} (ℕ × N) R)
      (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
            (Subalgebra.map (map R f) ⊤)) :
        Set (MvPolynomial (ℕ × N) R))
      (X (n, (f : (a : M) → N) l) : MvPolynomial.{u_4, u_1} (ℕ × N) R)
⊢ X (n, m) ∈
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))

Tactic:
obtain ⟨l, rfl⟩ := hf m

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
simp :
  ∃ (y : DividedPowerAlgebra R M),
    Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) y :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
⊢ Membership.mem (α := MvPolynomial.{u_4, u_1} (ℕ × N) R)
    (↑(Subalgebra.comap (B := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N)) (mkAlgHom R (Rel R N))
          (Subalgebra.map (map R f) ⊤)) :
      Set (MvPolynomial (ℕ × N) R))
    (X (n, (f : (a : M) → N) l) : MvPolynomial.{u_4, u_1} (ℕ × N) R)

Tactic:
simp only [Algebra.map_top, Subalgebra.coe_comap, AlgHom.coe_range, Set.mem_preimage,
    Set.mem_range]

Premises used: Set.mem_range, AlgHom.coe_range, Subalgebra.coe_comap, Algebra.map_top, Set.mem_preimage
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
h :
  Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) (dp R n l) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
⊢ ∃ (y : DividedPowerAlgebra R M),
    Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) y :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
      ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
        RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))

Tactic:
use dp R n l

Premises used: DividedPowerAlgebra.dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
n : ℕ
l : M
h :
  Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    (dp R n ((f : (a : M) → N) l) : DividedPowerAlgebra R N)
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
h₁ h₂ :
  Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((map R f : (a : DividedPowerAlgebra R M) → RingQuot (Rel R N)) (dp R n l) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))
    ((mkAlgHom R (Rel R N) : (a : MvPolynomial (ℕ × N) R) → RingQuot (Rel R N)) (X (n, (f : (a : M) → N) l)) :
      RingQuot (R := MvPolynomial.{u_4, u_1} (ℕ × N) R) (Rel R N))

Tactic:
rw [map_apply_dp, dp]

Premises used: DividedPowerAlgebra.map_apply_dp, DividedPowerAlgebra.dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
rw :
  ∀ (n : ℕ) (m : M),
    Eq (α := DividedPowerAlgebra R P)
      ((map R (g ∘ₗ f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) : DividedPowerAlgebra R P)
      ((AlgHom.comp (map R g) (map R f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) :
        DividedPowerAlgebra R P)
⊢ Eq (α := DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra R P) (map R (g ∘ₗ f)) (AlgHom.comp (map R g) (map R f))

Tactic:
rw [algHom_ext_iff]

Premises used: DividedPowerAlgebra.algHom_ext_iff
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R P)
    ((map R (g ∘ₗ f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) : DividedPowerAlgebra R P)
    ((AlgHom.comp (map R g) (map R f) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R P) (dp R n m) :
      DividedPowerAlgebra R P)

Tactic:
simp [map_apply_dp]

Premises used: DividedPowerAlgebra.map_apply_dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  ∀ (n : ℕ) (m : M),
    Eq (α := DividedPowerAlgebra R M)
      ((map R LinearMap.id : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
        DividedPowerAlgebra R M)
      ((AlgHom.id R (DividedPowerAlgebra R M) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
        DividedPowerAlgebra R M)
⊢ Eq (α := DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra R M) (map R LinearMap.id)
    (AlgHom.id R (DividedPowerAlgebra R M))

Tactic:
rw [algHom_ext_iff]

Premises used: DividedPowerAlgebra.algHom_ext_iff
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M)
    ((map R LinearMap.id : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
      DividedPowerAlgebra R M)
    ((AlgHom.id R (DividedPowerAlgebra R M) : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra R M) (dp R n m) :
      DividedPowerAlgebra R M)

Tactic:
simp [map_apply_dp]

Premises used: DividedPowerAlgebra.map_apply_dp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
P : Type u_5
inst_9 : AddCommMonoid P
inst_10 : Module R P
g : M ≃ₗ[R] N
⊢ AlgHom.comp (map R (↑g : M →ₗ[R] N)) (map R (↑g.symm : N →ₗ[R] M)) = AlgHom.id R (DividedPowerAlgebra R N)

Tactic:
simp [← map_comp, map_id]

Premises used: DividedPowerAlgebra.map_id, DividedPowerAlgebra.map_comp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
P : Type u_5
inst_9 : AddCommMonoid P
inst_10 : Module R P
g : M ≃ₗ[R] N
⊢ AlgHom.comp (map R (↑g.symm : N →ₗ[R] M)) (map R (↑g : M →ₗ[R] N)) = AlgHom.id R (DividedPowerAlgebra R M)

Tactic:
simp [← map_comp, map_id]

Premises used: DividedPowerAlgebra.map_id, DividedPowerAlgebra.map_comp
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
g : M ≃ₗ[R] N
⊢ (mapEquiv g).symm = mapEquiv g.symm

Tactic:
rfl

Premises used: DividedPowerAlgebra.mapEquiv, AlgEquiv.symm, AlgEquiv.ofAlgHom, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
g : M ≃ₗ[R] N
⊢ (↑(mapEquiv g) : DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra R N) = map R (↑g : M →ₗ[R] N)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, DividedPowerAlgebra.lift', DividedPowerAlgebra.map, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
g : M ≃ₗ[R] N
⊢ (↑(mapEquiv g).symm : DividedPowerAlgebra R N →ₐ[R] DividedPowerAlgebra R M) = map R (↑g.symm : N →ₗ[R] M)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, DividedPowerAlgebra.lift', DividedPowerAlgebra.map, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := DividedPowerAlgebra R M ≃ₐ[R] DividedPowerAlgebra R M) (mapEquiv (LinearEquiv.refl R M)) AlgEquiv.refl

Tactic:
AlgEquiv.coe_algHom_injective map_id

Premises used: DividedPowerAlgebra.map_id, AlgEquiv.coe_algHom_injective
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
g : M ≃ₗ[R] N
h : N ≃ₗ[R] P
⊢ (mapEquiv g).trans (mapEquiv h) = mapEquiv (g ≪≫ₗ h)

Tactic:
AlgEquiv.coe_algHom_injective (map_comp _ _).symm

Premises used: AlgEquiv.coe_algHom_injective, DividedPowerAlgebra.map_comp, Eq.symm
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : a ∉ ⊥
⊢ ¬a = 0

Tactic:
simp only [mem_bot] at ha

Premises used: Ideal.mem_bot
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : ¬a = 0
hnc : ¬(a = 0 ∧ n = 0)
⊢ Eq.{u_1 + 1} (α := A) (if a = 0 ∧ n = 0 then 1 else 0) 0

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : ¬a = 0
⊢ ¬(a = 0 ∧ n = 0)

Tactic:
not_and_of_not_left (n = 0) ha

Premises used: not_and_of_not_left, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
ha : ¬a = 0
⊢ ¬(a = 0 ∧ n = 0)

Tactic:
exact not_and_of_not_left (n = 0) ha

Premises used: not_and_of_not_left, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
x : A
ha : Membership.mem (γ := Ideal A) ⊥ x
rw : Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ Eq (α := ℕ) 0 0 then 1 else 0) 1
⊢ Eq.{u_1 + 1} (α := A) (if x = 0 ∧ Eq (α := ℕ) 0 0 then 1 else 0) 1

Tactic:
rw [mem_bot.mp ha]

Premises used: Ideal.mem_bot, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
x : A
ha : Membership.mem (γ := Ideal A) ⊥ x
⊢ Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ Eq (α := ℕ) 0 0 then 1 else 0) 1

Tactic:
simp only [and_self, ite_true]

Premises used: and_self, ite_true
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
x : A
ha : Membership.mem (γ := Ideal A) ⊥ x
⊢ (if x = 0 ∧ Eq (α := ℕ) 1 0 then 1 else 0) = x

Tactic:
simp [mem_bot.mp ha]

Premises used: Ideal.mem_bot, Iff.mp