awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
intro :
  ∀ (val : Fintype ι),
    ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
      ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
intro :
  ∀ (bM : Basis ι R M) (bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N) (f : Fin (Fintype.card ι) ↪ ι)
    (a : Fin (Fintype.card ι) → R)
    (snf :
      ∀ (i : Fin (Fintype.card ι)),
        (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
          HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)),
    ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
      ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)

Tactic:
let ⟨bM, bN, f, a, snf⟩ := N.smithNormalFormOfRankEq b h
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf :
  ∀ (i : Fin (Fintype.card ι)),
    (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective (⇑f : (a : Fin (Fintype.card ι)) → ι) ⋯
⊢ ∀ (i : ι),
    (f : (a : Fin (Fintype.card ι)) → ι) ((e.symm : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) = i

Tactic:
have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf :
  ∀ (i : Fin (Fintype.card ι)),
    (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective (⇑f : (a : Fin (Fintype.card ι)) → ι) ⋯
fe :
  ∀ (i : ι),
    (f : (a : Fin (Fintype.card ι)) → ι) ((e.symm : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) = i
i : ι
⊢ (↑((bN.reindex e : (a : ι) → ↥N) i) : M) =
    HSMul.hSMul (β := M) ((a ∘ (⇑e.symm : (a : ι) → Fin (Fintype.card ι))) i) ((bM : (a : ι) → M) i : M)

Tactic:
simp only [snf, fe,
          Basis.coe_reindex, (· ∘ ·)]

Premises used: Function.comp, Module.Basis.coe_reindex
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
val : Fintype ι
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin (Fintype.card ι)) R ↥N
f : Fin (Fintype.card ι) ↪ ι
a : Fin (Fintype.card ι) → R
snf :
  ∀ (i : Fin (Fintype.card ι)),
    (↑((bN : (a : Fin (Fintype.card ι)) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin (Fintype.card ι)) → ι) i : ι) : M)
e : Fin (Fintype.card ι) ≃ ι := Equiv.ofBijective (⇑f : (a : Fin (Fintype.card ι)) → ι) ⋯
fe :
  ∀ (i : ι),
    (f : (a : Fin (Fintype.card ι)) → ι) ((e.symm : (a : ι) → Fin (Fintype.card ι)) i : Fin (Fintype.card ι)) = i
⊢ ∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis.{u_1, u_2, u_3} ι R ↥N),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((b' : (a : ι) → M) i : M)

Tactic:
exact
    ⟨bM, a ∘ e.symm, bN.reindex e, fun i ↦ by
      simp only [snf, fe,
          Basis.coe_reindex, (· ∘ ·)]⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
⊢ ∀ (i : ι),
    (↑((smithNormalFormBotBasis b h : (a : ι) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (smithNormalFormCoeffs b h i) ((smithNormalFormTopBasis b h : (a : ι) → M) i : M)

Tactic:
(exists_smith_normal_form_of_rank_eq b h).choose_spec.choose_spec.choose_spec

Premises used: Exists.choose_spec, Submodule.exists_smith_normal_form_of_rank_eq, Submodule.smithNormalFormCoeffs
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
apply : Eq.{u_3 + 1} (α := ↥N) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i : ↥N) (0 : ↥N)
⊢ False

Tactic:
apply Basis.ne_zero (smithNormalFormBotBasis b h) i

Premises used: Module.Basis.ne_zero, Submodule.smithNormalFormBotBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
⊢ Eq.{u_3 + 1} (α := ↥N) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i : ↥N) (0 : ↥N)

Tactic:
Subtype.coe_injective ?_

Premises used: Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
refine :
  Eq.{u_3 + 1} (α := M) ((fun (a : ↥N) ↦ (↑a : M)) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i))
    ((fun (a : ↥N) ↦ (↑a : M)) 0)
⊢ Eq.{u_3 + 1} (α := ↥N) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i : ↥N) (0 : ↥N)

Tactic:
refine Subtype.coe_injective ?_

Premises used: Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
N : Submodule R M
inst_5 : Finite ι
b : Basis ι R M
h : finrank.{u_2, u_3} R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
⊢ Eq.{u_3 + 1} (α := M) ((fun (a : ↥N) ↦ (↑a : M)) ((smithNormalFormBotBasis b h : (a : ι) → ↥N) i))
    ((fun (a : ↥N) ↦ (↑a : M)) 0)

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
obtain :
  ∀ (fst : ℕ) (bS : Basis ι R S) (bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)) (f : Fin fst ↪ ι)
    (a : Fin fst → R),
    (∀ (i : Fin fst),
        (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
          HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)) →
      finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S

Tactic:
obtain ⟨_, bS, bI, _, _, _⟩ := (I.restrictScalars R).smithNormalForm b

Premises used: Submodule.restrictScalars, Submodule.smithNormalForm
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
intro : ∀ (val : Fintype ι), finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
val : Fintype ι
intro : Fintype.card (Fin fst) = Fintype.card ι
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S

Tactic:
rw [Module.finrank_eq_card_basis bS, Module.finrank_eq_card_basis bI]

Premises used: Module.finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
val : Fintype ι
⊢ Fintype.card (Fin fst) = Fintype.card ι

Tactic:
Ideal.rank_eq bS hI (bI.map ((restrictScalarsEquiv R S S I).restrictScalars R))

Premises used: LinearEquiv.restrictScalars, Module.Basis.map, Ideal.rank_eq, Submodule.restrictScalarsEquiv
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
val : Fintype ι
⊢ Fintype.card (Fin fst) = Fintype.card ι

Tactic:
exact Ideal.rank_eq bS hI (bI.map ((restrictScalarsEquiv R S S I).restrictScalars R))

Premises used: LinearEquiv.restrictScalars, Module.Basis.map, Ideal.rank_eq, Submodule.restrictScalarsEquiv
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ ∃ (b' : Basis ι R S) (a : ι → R) (ab' : Basis.{u_1, u_2, u_4} ι R ↥I),
    ∀ (i : ι), (↑((ab' : (a : ι) → ↥I) i) : S) = HSMul.hSMul (β := S) (a i) ((b' : (a : ι) → S) i : S)

Tactic:
Submodule.exists_smith_normal_form_of_rank_eq b (finrank_eq_finrank b I hI)

Premises used: Ideal.finrank_eq_finrank, Set.Mem, Submodule.restrictScalars, Submodule.exists_smith_normal_form_of_rank_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
⊢ ∀ (i : ι),
    (↑((selfBasis b I hI : (a : ι) → ↥I) i) : S) =
      HSMul.hSMul (β := S) (smithCoeffs b I hI i) ((ringBasis b I hI : (a : ι) → S) i : S)

Tactic:
(Ideal.exists_smith_normal_form b I hI).choose_spec.choose_spec.choose_spec

Premises used: Ideal.exists_smith_normal_form, Exists.choose_spec, Ideal.smithCoeffs
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
apply : Eq.{u_4 + 1} (α := ↥I) ((selfBasis b I hI : (a : ι) → ↥I) i : ↥I) (0 : ↥I)
⊢ False

Tactic:
apply Basis.ne_zero (Ideal.selfBasis b I hI) i

Premises used: Module.Basis.ne_zero, Ideal.selfBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ Eq.{u_4 + 1} (α := ↥I) ((selfBasis b I hI : (a : ι) → ↥I) i : ↥I) (0 : ↥I)

Tactic:
Subtype.coe_injective ?_

Premises used: Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
refine :
  Eq.{u_4 + 1} (α := S) ((fun (a : ↥I) ↦ (↑a : S)) ((selfBasis b I hI : (a : ι) → ↥I) i)) ((fun (a : ↥I) ↦ (↑a : S)) 0)
⊢ Eq.{u_4 + 1} (α := ↥I) ((selfBasis b I hI : (a : ι) → ↥I) i : ↥I) (0 : ↥I)

Tactic:
refine Subtype.coe_injective ?_

Premises used: Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ Eq.{u_4 + 1} (α := S) ((fun (a : ↥I) ↦ (↑a : S)) ((selfBasis b I hI : (a : ι) → ↥I) i)) ((fun (a : ↥I) ↦ (↑a : S)) 0)

Tactic:
simp [hi]
-- Module: Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ StrongRankCondition R

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
⊢ motive 0

Tactic:
zero
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
⊢ motive 0

Tactic:
exact zero
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
i : ι
x : M i
⊢ motive ((of M i : (a : M i) → ⨁ (i : ι), M i) x)

Tactic:
lof _ _
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
i : ι
x : M i
⊢ motive ((of M i : (a : M i) → ⨁ (i : ι), M i) x)

Tactic:
exact lof _ _
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
x y : ⨁ (i : ι), M i
hx : motive x
hy : motive y
⊢ motive (x + y)

Tactic:
add x y hx hy
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
x y : ⨁ (i : ι), M i
hx : motive x
hy : motive y
⊢ motive (x + y)

Tactic:
exact add x y hx hy
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
x : ⨁ (i : ι), M i
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
zero₁ : motive 0
of : ∀ (i : ι) (x : M i), motive ((DirectSum.of M i : (a : M i) → ⨁ (i : ι), M i) x)
add₁ : ∀ (x y : ⨁ (i : ι), M i) (hx : motive x) (hy : motive y), motive (x + y)
⊢ motive x

Tactic:
induction x using DirectSum.induction_on with
  | zero => exact zero
  | of => exact lof _ _
  | add x y hx hy => exact add x y hx hy

Premises used: DirectSum.of
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : A
h_rel : rel x y
w :
  Function.onFun (α := B) rel ((⇑f.symm : (a : B) → A) : (a : B) → A)
    (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) x : B) (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) y : B)
⊢ Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B) :
          (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        x :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B) :
          (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        y :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))

Tactic:
apply RingQuot.mkAlgHom_rel

Premises used: RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : A
h_rel : rel x y
⊢ Function.onFun (α := B) rel ((⇑f.symm : (a : B) → A) : (a : B) → A)
    (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) x : B) (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) y : B)

Tactic:
simpa [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : B
h : (rel on (⇑f.symm : (a : B) → A)) x y
w : rel (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) x) (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) y)
⊢ Eq (α := RingQuot rel)
    ((AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A) : (a : B) → RingQuot rel) x : RingQuot rel)
    ((AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A) : (a : B) → RingQuot rel) y : RingQuot rel)

Tactic:
apply RingQuot.mkAlgHom_rel

Premises used: RingQuot.mkAlgHom_rel
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : B
h : (rel on (⇑f.symm : (a : B) → A)) x y
⊢ rel (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) x) (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) y)

Tactic:
simpa