awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
val : Fintype ι
intro :
  ∀ (M : ι → Type u) [inst_4 : (i : ι) → AddCommMonoid (M i)] [inst_5 : (i : ι) → Module R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
revert M
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
⊢ ∀ (M : ι → Type u) [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)

Tactic:
Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
intro :
  ∀ (α : Type v) (x : Fintype α)
    (h :
      ∀ (M : α → Type u) [inst_2 : (i : α) → AddCommMonoid (M i)] [inst_3 : (i : α) → Module R (M i)]
        (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
    (M : Option α → Type u) (x : (i : Option α) → AddCommMonoid (M i)) (x_1 : (i : Option α) → Module R (M i))
    (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
⊢ ∀ (M : ι → Type u) [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)

Tactic:
refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
α : Type v
x : Fintype α
h :
  ∀ (M : α → Type u) [inst_2 : (i : α) → AddCommMonoid (M i)] [inst_3 : (i : α) → Module R (M i)]
    (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i)
M : Option α → Type u
x_1 : (i : Option α) → AddCommMonoid (M i)
x_2 : (i : Option α) → Module R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)

Tactic:
equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: LinearEquiv.symm, Option.some, LinearEquiv.piOptionEquivProd
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
    [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
α : Type v
x : Fintype α
h :
  ∀ (M : α → Type u) [inst_2 : (i : α) → AddCommMonoid (M i)] [inst_3 : (i : α) → Module R (M i)]
    (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i)
M : Option α → Type u
x_1 : (i : Option α) → AddCommMonoid (M i)
x_2 : (i : Option α) → Module R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)

Tactic:
exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: LinearEquiv.symm, Option.some, LinearEquiv.piOptionEquivProd
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
intro₁ :
  ∀ (val : Fintype ι) (M : ι → Type u) [inst_4 : (i : ι) → AddCommMonoid (M i)] [inst_5 : (i : ι) → Module R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
intro₂ :
  ∀ (val : Fintype ι) (α : Type v) (x : Fintype α)
    (h :
      ∀ (M : α → Type u) [inst_4 : (i : α) → AddCommMonoid (M i)] [inst_5 : (i : α) → Module R (M i)]
        (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
    (M : Option α → Type u) (x : (i : Option α) → AddCommMonoid (M i)) (x_1 : (i : Option α) → Module R (M i))
    (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: LinearEquiv.symm, nonempty_fintype, LinearEquiv.piOptionEquivProd
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] LinearMap.{u, u, w, y} (RingHom.id R) M₂ (Fin n → M₃)
x y : M
z : M₂
⊢ Eq.{y + 1} (α := Fin n.succ → M₃)
    ((vecCons ((f : (a : M) → M₂ →ₗ[R] M₃) (x + y)) ((g : (a : M) → M₂ →ₗ[R] Fin n → M₃) (x + y)) :
          (a : M₂) → Fin n.succ → M₃)
        z :
      Fin n.succ → M₃)
    ((HAdd.hAdd (α := LinearMap.{u, u, w, y} (RingHom.id R) M₂ (Fin n.succ → M₃))
            (vecCons ((f : (a : M) → M₂ →ₗ[R] M₃) x) ((g : (a : M) → M₂ →ₗ[R] Fin n → M₃) x))
            (vecCons ((f : (a : M) → M₂ →ₗ[R] M₃) y) ((g : (a : M) → M₂ →ₗ[R] Fin n → M₃) y)) :
          (a : M₂) → Fin n.succ → M₃)
        z :
      Fin n.succ → M₃)

Tactic:
simp only [f.map_add, g.map_add, LinearMap.add_apply, LinearMap.vecCons_apply,
        Matrix.cons_add_cons (f x z)]

Premises used: LinearMap.map_add, LinearMap.add_apply, LinearMap.vecCons_apply, Matrix.cons_add_cons, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
n : ℕ
f : M →ₗ[R] M₂ →ₗ[R] M₃
g : M →ₗ[R] LinearMap.{u, u, w, y} (RingHom.id R) M₂ (Fin n → M₃)
r : R
x : M
z : M₂
⊢ Eq.{y + 1} (α := Fin n.succ → M₃)
    ((vecCons ((f : (a : M) → M₂ →ₗ[R] M₃) (r • x)) ((g : (a : M) → M₂ →ₗ[R] Fin n → M₃) (r • x)) :
          (a : M₂) → Fin n.succ → M₃)
        z :
      Fin n.succ → M₃)
    ((HSMul.hSMul (α := R) (β := LinearMap.{u, u, w, y} (RingHom.id R) M₂ (Fin n.succ → M₃))
            ((RingHom.id R : (a : R) → R) r : R)
            (vecCons ((f : (a : M) → M₂ →ₗ[R] M₃) x) ((g : (a : M) → M₂ →ₗ[R] Fin n → M₃) x)) :
          (a : M₂) → Fin n.succ → M₃)
        z :
      Fin n.succ → M₃)

Tactic:
simp [Matrix.smul_cons r (f x z)]

Premises used: Matrix.smul_cons, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
val : Fintype ι
intro :
  ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
revert M
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)

Tactic:
Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
intro :
  ∀ (α : Type v) (x : Fintype α)
    (h :
      ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module.{u_1, u} R (M i)]
        (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
    (M : Option α → Type u) (x : (i : Option α) → AddCommGroup (M i)) (x_1 : (i : Option α) → Module.{u_1, u} R (M i))
    (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)

Tactic:
refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
α : Type v
x : Fintype α
h :
  ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i)
M : Option α → Type u
x_1 : (i : Option α) → AddCommGroup (M i)
x_2 : (i : Option α) → Module.{u_1, u} R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)

Tactic:
equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: LinearEquiv.symm, Option.some, LinearEquiv.piOptionEquivProd
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_2 : AddCommGroup N'] [inst_3 : Module R N]
    [inst_4 : Module R N'], motive N → motive' N' → motive' (N × N')
val : Fintype ι
α : Type v
x : Fintype α
h :
  ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_2 : (i : α) → Module.{u_1, u} R (M i)]
    (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i)
M : Option α → Type u
x_1 : (i : Option α) → AddCommGroup (M i)
x_2 : (i : Option α) → Module.{u_1, u} R (M i)
hn : ∀ (i : Option α), motive (M i)
⊢ motive' ((i : Option α) → M i)

Tactic:
exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: Option.some
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type v
inst : Finite ι
R : Type u_1
inst_1 : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N]
    [inst_6 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u_1, u} R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
intro₁ :
  ∀ (val : Fintype ι) (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)]
    [inst_4 : (i : ι) → Module.{u_1, u} R (M i)] (h : ∀ (i : ι), motive (M i)), motive' ((i : ι) → M i)
intro₂ :
  ∀ (val : Fintype ι) (α : Type v) (x : Fintype α)
    (h :
      ∀ (M : α → Type u) [inst : (i : α) → AddCommGroup (M i)] [inst_4 : (i : α) → Module.{u_1, u} R (M i)]
        (h : ∀ (i : α), motive (M i)), motive' ((i : α) → M i))
    (M : Option α → Type u) (x : (i : Option α) → AddCommGroup (M i)) (x_1 : (i : Option α) → Module.{u_1, u} R (M i))
    (hn : ∀ (i : Option α), motive (M i)), motive' ((i : Option α) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
classical
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Fintype ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
rw :
  Eq.{u_2 + 1} (α := R)
    ((((Basis.repr
                  (Basis.map Finsupp.basisSingleOne
                    (LinearEquiv.symm
                      (LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯)
                        (LinearEquiv.trans
                          (PiTensorProduct.congr (s := M) (t := fun (i : ι) ↦ Finsupp.{u_4, u_2} (κ i) R) fun (i : ι) ↦
                            (b i).repr)
                          (ofFinsuppEquiv (κ := κ) (M := fun (i : ι) ↦ R)))
                        (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i))
                          (↑(constantBaseRingEquiv ι R) : (⨂[R] (x : ι), R) ≃ₗ[R] R))))) :
                (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((tprod R (s := M) : (a : (i : ι) → M i) → ⨂[R] (i : ι), M i) x) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        p :
      R)
    (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (x i) : Finsupp.{u_4, u_2} (κ i) R) : (a : κ i) → R) (p i) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((piTensorProduct (M := M) (κ := κ) b).repr : (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((tprod R (s := M) : (a : (i : ι) → M i) → ⨂[R] (i : ι), M i) x) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        p :
      R)
    (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (x i) : Finsupp.{u_4, u_2} (κ i) R) : (a : κ i) → R) (p i) : R)

Tactic:
rw [piTensorProduct, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]

Premises used: Fintype.ofFinite, Basis.piTensorProduct, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : Fintype ι
b : (i : ι) → Basis.{u_4, u_2, u_3} (κ i) R (M i)
x : (i : ι) → M i
p : (i : ι) → κ i
⊢ Eq.{u_2 + 1} (α := R)
    ((((Basis.repr
                  (Basis.map Finsupp.basisSingleOne
                    (LinearEquiv.symm
                      (LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯)
                        (LinearEquiv.trans
                          (PiTensorProduct.congr (s := M) (t := fun (i : ι) ↦ Finsupp.{u_4, u_2} (κ i) R) fun (i : ι) ↦
                            (b i).repr)
                          (ofFinsuppEquiv (κ := κ) (M := fun (i : ι) ↦ R)))
                        (Finsupp.lcongr (Equiv.refl ((i : ι) → κ i))
                          (↑(constantBaseRingEquiv ι R) : (⨂[R] (x : ι), R) ≃ₗ[R] R))))) :
                (a : ⨂[R] (i : ι), M i) → ((i : ι) → κ i) →₀ R)
              ((tprod R (s := M) : (a : (i : ι) → M i) → ⨂[R] (i : ι), M i) x) :
            ((i : ι) → κ i) →₀ R) :
          (a : (i : ι) → κ i) → R)
        p :
      R)
    (∏ i : ι, ((((b i).repr : (a : M i) → κ i →₀ R) (x i) : Finsupp.{u_4, u_2} (κ i) R) : (a : κ i) → R) (p i) : R)

Tactic:
simp