awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
pos :
  ∀ (hi : j = j'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 1) : ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) (if j = j' then 1 else 0)) :
            ι →₀ R) :
          (a : ι) → R)
        i' :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
have neg : ∀ (hi : ¬j = j'),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 0) : ι →₀ R) : (a : ι) → R)
        i' :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have obtain : ∀ (i : ι) (j : ι'),
  (b.smulTower c : (a : ι × ι') → A) (i, j) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have obtain₁ : ∀ (i : ι) (j : ι'),
  Eq (α := ι × ι' →₀ R)
    ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
          ((c : (a : ι') → A) (i, j).2 : A)) :
      ι × ι' →₀ R)
    (single (i, j) 1 : ι × ι' →₀ R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have h : ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
  Eq.{u_1 + 1} (α := R)
    ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                ((c : (a : ι') → A) (i, j).2 : A)) :
            ι × ι' →₀ R) :
          (a : ι × ι') → R)
        (i', j') :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
h :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
                (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                  ((c : (a : ι') → A) (i, j).2 : A)) :
              ι × ι' →₀ R) :
            (a : ι × ι') → R)
          (i', j') :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have h₁ : ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R)
              (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) (i, j).1 : S)
                (if (i, j).2 = (i', j').2 then 1 else 0)) :
            ι →₀ R) :
          (a : ι) → R)
        (i', j').1 :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
h :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
                (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                  ((c : (a : ι') → A) (i, j).2 : A)) :
              ι × ι' →₀ R) :
            (a : ι × ι') → R)
          (i', j') :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₁ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) (i, j).1 : S)
                  (if (i, j).2 = (i', j').2 then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          (i', j').1 :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have h₂ : ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) (if j = j' then 1 else 0)) :
            ι →₀ R) :
          (a : ι) → R)
        i' :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
h :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
                (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                  ((c : (a : ι') → A) (i, j).2 : A)) :
              ι × ι' →₀ R) :
            (a : ι × ι') → R)
          (i', j') :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₁ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) (i, j).1 : S)
                  (if (i, j).2 = (i', j').2 then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          (i', j').1 :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₂ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) (if j = j' then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have pos : ∀ (i : ι) (j : ι') (i' : ι) (j' : ι') (hi : j = j'),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 1) : ι →₀ R) : (a : ι) → R)
        i' :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
h :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
                (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                  ((c : (a : ι') → A) (i, j).2 : A)) :
              ι × ι' →₀ R) :
            (a : ι × ι') → R)
          (i', j') :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₁ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) (i, j).1 : S)
                  (if (i, j).2 = (i', j').2 then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          (i', j').1 :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₂ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) (if j = j' then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
pos :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι') (hi : j = j'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 1) : ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)
have neg : ∀ (i : ι) (j : ι') (i' : ι) (j' : ι') (hi : ¬j = j'),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 0) : ι →₀ R) : (a : ι) → R)
        i' :
      R)
    ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
Tactic: classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ Eq.{u_1 + 1} (α := R) ((((repr (b.smulTower' c) : (a : A) → ι' × ι →₀ R) x : ι' × ι →₀ R) : (a : ι' × ι) → R) ij : R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) ij.1) : ι →₀ R) :
          (a : ι) → R)
        ij.2 :
      R)
have rw : Eq.{u_1 + 1} (α := R)
  (((b.repr : (a : S) → ι →₀ R)
          ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S)
            (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2) :
        (a : ι) → R)
      (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 :
    R)
  ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) ij.1) : ι →₀ R) :
        (a : ι) → R)
      ij.2 :
    R)
Tactic: rw [smulTower', repr_reindex_apply, smulTower_repr]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower' c : (a : ι' × ι) → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.2 : S) ((c : (a : ι') → A) ij.1 : A)
have rw : HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A)
    ((b : (a : ι) → S) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 : S)
    ((c : (a : ι') → A) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2 : A) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.2 : S) ((c : (a : ι') → A) ij.1 : A)
Tactic: rw [smulTower', reindex_apply, smulTower_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 f : C →ₐ[A] D
⊢ (fun (fg : (f : B →ₐ[A] D) × (C →ₐ[B] D)) ↦
        let x := fg.fst (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D).toAlgebra;
        (AlgHom.restrictScalars A (fg.snd (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)) : C →ₐ[A] D))
      ((fun (f : C →ₐ[A] D) ↦
          (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D) (AlgHom.restrictDomain B f) (AlgHom.extendScalars B f) :
            (f : B →ₐ[A] D) × (C →ₐ[B] D)))
        f) =
    f
have dsimp : AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 f : C →ₐ[A] D
⊢ AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f
have H : ∀ (x : C),
  Eq.{u_6 + 1} (α := D) ((AlgHom.restrictScalars A (AlgHom.extendScalars B f) : (a : C) → D) x : D)
    ((f : (a : C) → D) x : D)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraTower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 : C →ₐ[A] D
f : B → D
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one' : OneHom B D }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom B D }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom B D }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun 0 = 0
map_add' :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
g : C → D
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun 0 = 0
map_add'_1 :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun y
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
⊢ f = fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x)
have h : ∀ (x : B), f x = g ((algebraMap B C : (a : B) → C) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsAlgebraic R a
⊢ Nontrivial R
have contrapose! : ∀ (h : Subsingleton R), ¬IsAlgebraic R a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
H : IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
⊢ IsAlgebraic R r
have obtain : ∀ (p : R[X]) (h1 : p ≠ 0)
  (h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)),
  IsAlgebraic R r
Tactic: obtain ⟨p, h1, h2⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
⊢ p = 0
have rwa : ∀ (h : p.leadingCoeff * f.leadingCoeff ^ p.natDegree = 0), p = 0
Tactic: rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
rwa : ∀ (h : p.leadingCoeff * f.leadingCoeff ^ p.natDegree = 0), p = 0
⊢ p = 0
have rwa₁ : ∀ (h : p.leadingCoeff = 0), p = 0
Tactic: rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
rwa : ∀ (h : p.leadingCoeff * f.leadingCoeff ^ p.natDegree = 0), p = 0
rwa₁ : ∀ (h : p.leadingCoeff = 0), p = 0
⊢ p = 0
have rwa₂ : ∀ (h : p = 0), p = 0
Tactic: rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
Cleared hypotheses: h