awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdjoinRoot
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 := ⋯
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
⊢ Splits (Polynomial.map (algebraMap R S) p)

Tactic:
rw [IsScalarTower.algebraMap_eq R (AdjoinRoot p), ← Polynomial.map_map, hq, Polynomial.map_mul]

Premises used: Polynomial.map_mul, AdjoinRoot, IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.RingTheory.AdjoinRoot
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 (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])))

Tactic:
simp
-- Module: Mathlib.RingTheory.AdjoinRoot
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 := ⋯
⊢ (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:
exact .mul (by simp) hS
-- Module: Mathlib.RingTheory.AdjoinRoot
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hp : p.Monic
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
⊢ ∃ (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

Premises used: Polynomial.C, Polynomial.map_mul, AdjoinRoot, Algebra.algebraMap, IsUnit, IsScalarTower.algebraMap_eq, AdjoinRoot.root, Polynomial.map, Polynomial.natDegree, Polynomial.map_map, Polynomial.X, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
ι : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
c : R
x : M
⊢ HSMul.hSMul.{u_3, u_6, u_6} (α := A) ((RingEquiv.ofBijective (algebraMap R A) h : (a : R) → A) c : A) x = c • x

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
A : Type u_3
ι : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
m : M
⊢ Eq (α := ι →₀ A) ((repr (algebraMapCoeffs A b h) : (a : M) → ι →₀ A) m : ι →₀ A)
    (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m) : ι →₀ A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
A : Type u_3
ι : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
i : ι
⊢ Eq.{u_6 + 1} (α := M) ((algebraMapCoeffs A b h : (a : ι) → M) i : M) ((b : (a : ι) → M) i : M)

Tactic:
b.mapCoeffs_apply _ _ _

Premises used: Module.Basis.mapCoeffs_apply
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
A : Type u_3
ι : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ Eq (α := (a : ι) → M) (⇑(algebraMapCoeffs A b h) : (a : ι) → M) (⇑b : (a : ι) → M)

Tactic:
b.coe_mapCoeffs _ _

Premises used: Module.Basis.coe_mapCoeffs
-- Module: Mathlib.RingTheory.AlgebraTower
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 :
  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)
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2

Tactic:
rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]

Premises used: Finsupp.linearCombination_smul, Equiv.prodComm, linearIndependent_equiv', LinearIndependent
-- Module: Mathlib.RingTheory.AlgebraTower
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
⊢ 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:
simpa using Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)

Premises used: map_zero, Finsupp.mapRange_injective, Function.Injective.comp, Equiv.injective
-- Module: Mathlib.RingTheory.AlgebraTower
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)
rw₂ rw₃ 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)
⊢ LinearIndependent R (M := A) fun (p : ι × ι') ↦ b p.1 • c p.2

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 _)

Premises used: Finsupp.linearCombination_smul, Equiv.prodComm, linearIndependent_equiv', map_zero, Finsupp.mapRange_injective, Function.Injective.comp, LinearIndependent, Equiv.injective
-- Module: Mathlib.RingTheory.AlgebraTower
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
inst_7 : Nonempty ι
b : Basis ι S A
⊢ IsScalarTower R S S

Tactic:
(b.repr.symm.comp <| lsingle <| Classical.arbitrary ι).isScalarTower_of_injective R
    (b.repr.symm.injective.comp <| single_injective _)

Premises used: Finsupp.single_injective, LinearEquiv.symm, LinearMap.isScalarTower_of_injective, Module.Basis.repr, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, Classical.arbitrary, LinearEquiv.injective, Finsupp.lsingle
-- Module: Mathlib.RingTheory.AlgebraTower
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 : Basis ι S A
⊢ IsScalarTower R S (ι →₀ S)

Tactic:
b.repr.symm.isScalarTower_of_injective R b.repr.symm.injective

Premises used: LinearEquiv.symm, LinearMap.isScalarTower_of_injective, Module.Basis.repr, LinearEquiv.toLinearMap, LinearEquiv.injective
-- Module: Mathlib.RingTheory.AlgebraTower
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.2) : ι →₀ R) :
          (a : ι) → R)
        ij.1 :
      R)

Tactic:
simp [smulTower, Finsupp.uncurry_apply]

Premises used: Finsupp.uncurry_apply, Module.Basis.smulTower
-- Module: Mathlib.RingTheory.AlgebraTower
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
i : ι
j : ι'
⊢ Eq.{u_1 + 1} (α := R)
    ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R) x : ι × ι' →₀ R) : (a : ι × ι') → R) (i, j) : R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) j) : ι →₀ R) :
          (a : ι) → R)
        i :
      R)

Tactic:
b.smulTower_repr c x (i, j)

Premises used: Prod.mk, Module.Basis.smulTower_repr
-- Module: Mathlib.RingTheory.AlgebraTower
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)

Tactic:
obtain ⟨i, j⟩ := ij
-- Module: Mathlib.RingTheory.AlgebraTower
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 : ι'
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)
⊢ (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:
rw [Basis.apply_eq_iff]

Premises used: Module.Basis.apply_eq_iff
-- Module: Mathlib.RingTheory.AlgebraTower
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 : ι'
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)
⊢ 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:
ext ⟨i', j'⟩
-- Module: Mathlib.RingTheory.AlgebraTower
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' : ι'
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)
⊢ 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:
rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]

Premises used: Finsupp.smul_apply, Finsupp.single_apply, Module.Basis.smulTower_repr, Module.Basis.repr_self, map_smul
-- Module: Mathlib.RingTheory.AlgebraTower
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' : ι'
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)
⊢ 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:
dsimp only
-- Module: Mathlib.RingTheory.AlgebraTower
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)
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)
⊢ 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:
split_ifs with hi
-- Module: Mathlib.RingTheory.AlgebraTower
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' : ι'
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:
simp [hi, Finsupp.single_apply]

Premises used: Finsupp.single_apply
-- Module: Mathlib.RingTheory.AlgebraTower
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' : ι'
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:
simp [hi]