awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : IsUnit p
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have pos : ∀ (hp : Monic.{u} (R := R) 1) (hn : natDegree.{u} (R := R) 1 = n) (hpu : IsUnit.{u} (M := R[X]) 1),
  ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) 1).Splits
Tactic: obtain rfl := hp.eq_one_of_isUnit hpu
Cleared hypotheses: p, hp, hn, hpu
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have neg : ∀ (q : (AdjoinRoot p)[X])
  (hq :
    Polynomial.map (algebraMap R (AdjoinRoot p)) p =
      HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
          ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
        q),
  ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
Tactic: obtain ⟨q, hq⟩ : X - C (AdjoinRoot.root p) ∣ p.map (algebraMap _ _) := by
    simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have hqm : q.Monic
Tactic: have hqm : q.Monic := .of_mul_monic_left (monic_X_sub_C (.root _)) (hq ▸ hp.map _)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have this : Free R (AdjoinRoot p)
Tactic: have := hp.free_adjoinRoot
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this : Free R (AdjoinRoot p)
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have this₁ : Module.Finite R (AdjoinRoot p)
Tactic: have := hp.finite_adjoinRoot
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this : Module.Finite R (AdjoinRoot p)
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have this₁ : Nontrivial.{u} (AdjoinRoot p)
Tactic: have : Nontrivial (AdjoinRoot p) := Ideal.Quotient.nontrivial_iff.mpr (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
⊢ q.natDegree < n
have rw : q.natDegree <
  (HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X])).natDegree +
    q.natDegree
Tactic: rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have neg : ∀ (S : Type u) (w : CommRing S) (w_1 : Algebra (AdjoinRoot p) S),
  Module.Finite (AdjoinRoot p) S →
    Free (AdjoinRoot p) S →
      Nontrivial S →
        ∀ (hS : (Polynomial.map (algebraMap (AdjoinRoot p) S) q).Splits),
          ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
            (Polynomial.map (algebraMap R S) p).Splits
Tactic: obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
S : Type u
w : CommRing S
w_1 : Algebra (AdjoinRoot p) S
w_2 : Module.Finite (AdjoinRoot p) S
w_3 : Free (AdjoinRoot p) S
w_4 : Nontrivial S
hS : Splits (Polynomial.map (algebraMap (AdjoinRoot p) S) q)
algInst : Algebra R S :=
  RingHom.toAlgebra
    (@RingHom.comp _ (AdjoinRoot p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (AdjoinRoot p) S)
      (algebraMap R (AdjoinRoot p)))
scalarTowerInst : IsScalarTower R (AdjoinRoot p) S := ⋯
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have neg : Splits (Polynomial.map (algebraMap R S) p)
Tactic: refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) (hn : p.natDegree = m),
      ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
        (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq :
  Polynomial.map (algebraMap R (AdjoinRoot p)) p =
    HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X]) *
      q
hqm : q.Monic
this_1 : Free R (AdjoinRoot p)
this_2 : Module.Finite R (AdjoinRoot p)
this : Nontrivial.{u} (AdjoinRoot p)
S : Type u
w : CommRing S
w_1 : Algebra (AdjoinRoot p) S
w_2 : Module.Finite (AdjoinRoot p) S
w_3 : Free (AdjoinRoot p) S
w_4 : Nontrivial S
hS : Splits (Polynomial.map (algebraMap (AdjoinRoot p) S) q)
algInst : Algebra R S :=
  RingHom.toAlgebra
    (@RingHom.comp _ (AdjoinRoot p) _ _ Semiring.toNonAssocSemiring _ (algebraMap (AdjoinRoot p) S)
      (algebraMap R (AdjoinRoot p)))
scalarTowerInst : IsScalarTower R (AdjoinRoot p) S := ⋯
⊢ Splits (Polynomial.map (algebraMap R S) p)
have neg : (HMul.hMul (α := S[X])
    (Polynomial.map (algebraMap (AdjoinRoot p) S)
      (HSub.hSub (α := (AdjoinRoot p)[X]) (β := (AdjoinRoot p)[X]) X
        ((C : (a : AdjoinRoot p) → (AdjoinRoot p)[X]) (AdjoinRoot.root p) : (AdjoinRoot p)[X])))
    (Polynomial.map (algebraMap (AdjoinRoot p) S) q)).Splits
Tactic: rw [IsScalarTower.algebraMap_eq R (AdjoinRoot p), ← Polynomial.map_map, hq, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
⊢ ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
have induction : ∀ (x : ℕ) (hn : p.natDegree = x),
  ∃ (S : Type u) (x : CommRing S) (x_1 : Algebra R S) (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S),
    (Polynomial.map (algebraMap R S) p).Splits
Tactic: induction hn : p.natDegree using Nat.strong_induction_on generalizing R with | h n IH =>
  by_cases hpu : IsUnit p
  · obtain rfl := hp.eq_one_of_isUnit hpu
    exact ⟨R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, by simp⟩
  obtain ⟨q, hq⟩ : X - C (AdjoinRoot.root p) ∣ p.map (algebraMap _ _) := by
    simp [dvd_iff_isRoot, -AdjoinRoot.algebraMap_eq]
  have hqm : q.Monic := .of_mul_monic_left (monic_X_sub_C (.root _)) (hq ▸ hp.map _)
  have := hp.free_adjoinRoot
  have := hp.finite_adjoinRoot
  have : Nontrivial (AdjoinRoot p) := Ideal.Quotient.nontrivial_iff.mpr (by simpa)
  obtain ⟨S, _, _, _, _, _, hS⟩ := IH _
    (by rw [← hn, ← hp.natDegree_map (algebraMap R (AdjoinRoot p)), hq,
      Monic.natDegree_mul (monic_X_sub_C _) hqm]; simp) hqm rfl
  algebraize [(algebraMap (AdjoinRoot p) S).comp (algebraMap R (AdjoinRoot p))]
  refine ⟨S, ‹_›, ‹_›, .trans (AdjoinRoot p) _, .trans (S := AdjoinRoot p), ‹_›, ?_⟩
  rw [IsScalarTower.algebraMap_eq R (AdjoinRoot p), ← Polynomial.map_map, hq, Polynomial.map_mul]
  exact .mul (by simp) hS
-- 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
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2
have rw : Function.Injective (α := ι' × ι →₀ R) (β := A)
  (⇑((↑R :
            {S : Type u_2} →
              {M : Type (max u_6 u_2)} →
                {M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (linearCombination S c) ∘ₗ
        mapRange.linearMap (linearCombination R b) ∘ₗ (↑(curryLinearEquiv R) : (ι' × ι →₀ R) →ₗ[R] ι' →₀ ι →₀ R)) :
    (a : ι' × ι →₀ R) → A)
Tactic: rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
-- 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
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2
have rw : LinearIndependent R (M := A) fun (p : ι' × ι) ↦ b p.2 • c p.1
Tactic: classical
  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
  simpa using Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
-- 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
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
rw : LinearIndependent R (M := A) fun (p : ι' × ι) ↦ b p.2 • c p.1
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2
have rw₁ : Function.Injective (α := ι' × ι →₀ R) (β := A)
  (⇑(linearCombination R fun (p : ι' × ι) ↦ b p.2 • c p.1) : (a : ι' × ι →₀ R) → A)
Tactic: classical
  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
  simpa using Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
-- 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
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
rw : LinearIndependent R (M := A) fun (p : ι' × ι) ↦ b p.2 • c p.1
rw₁ :
  Function.Injective (α := ι' × ι →₀ R) (β := A)
    (⇑(linearCombination R fun (p : ι' × ι) ↦ b p.2 • c p.1) : (a : ι' × ι →₀ R) → A)
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2
have rw₂ : Function.Injective (α := ι' × ι →₀ R) (β := A)
  (⇑((↑R :
            {S : Type u_2} →
              {M : Type (max u_6 u_2)} →
                {M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (linearCombination S c) ∘ₗ
        mapRange.linearMap (linearCombination R b) ∘ₗ (↑(curryLinearEquiv R) : (ι' × ι →₀ R) →ₗ[R] ι' →₀ ι →₀ R)) :
    (a : ι' × ι →₀ R) → A)
Tactic: classical
  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
  simpa using Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
-- 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: obtain ⟨i, j⟩ := ij
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
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)
have rw : 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: rw [Basis.apply_eq_iff]
-- 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 : ι'
⊢ 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)
have h : ∀ (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: ext ⟨i', j'⟩
-- 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' : ι'
⊢ 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)
have h : 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: rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
-- 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' : ι'
⊢ 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)
have h : 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: dsimp only
-- 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' : ι'
⊢ 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 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)
Tactic: split_ifs with hi