awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
I : Type u_1
x : I → M₂
hx : Membership.mem (γ := Submodule R (I → M₂)) (Submodule.pi (φ := fun (x : I) ↦ M₂) Set.univ fun (x : I) ↦ f.range) x
⊢ x ∈ (f.compLeft I).range
have choose : ∀ (y : (i : I) → Membership.mem (γ := Set I) Set.univ i → M)
  (hy : ∀ (i : I) (a : Membership.mem (γ := Set I) Set.univ i), (f : (a : M) → M₂) (y i a) = x i),
  x ∈ (f.compLeft I).range
Tactic: choose y hy using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 : Semiring R
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R (χ i)
e : (i : ι) → LinearEquiv.{u, u, u_1, u_2} (RingHom.id R) (φ i) (ψ i)
c : R
f : (i : ι) → φ i
⊢ (fun (i : ι) ↦ (e i : (a : φ i) → ψ i) ((c • f) i)) =
    HSMul.hSMul (α := R) (β := (i : ι) → ψ i) ((RingHom.id R : (a : R) → R) c : R) fun (i : ι) ↦
      (e i : (a : φ i) → ψ i) (f i)
have h : ∀ (x : ι),
  (e x : (a : φ x) → ψ x) ((c • f) x) =
    HSMul.hSMul (α := R) (β := (i : ι) → ψ i) ((RingHom.id R : (a : R) → R) c : R)
      (fun (i : ι) ↦ (e i : (a : φ i) → ψ i) (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : 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 : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
f g : α ⊕ β → M
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (f + g) =
    (Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g
have fst : ∀ (x : α),
  ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).1 x =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : 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 : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
f g : α ⊕ β → M
fst :
  ∀ (x : α),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).1 x =
      ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).1 x
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (f + g) =
    (Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g
have snd : ∀ (x : β),
  ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).2 x =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).2 x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : 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 : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
r : R
f : α ⊕ β → M
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (r • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)
have fst : ∀ (x : α),
  ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).1 x =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : 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 : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
r : R
f : α ⊕ β → M
fst :
  ∀ (x : α),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).1 x =
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).1 x
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (r • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)
have snd : ∀ (x : β),
  ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).2 x =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).2 x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x ↔
    ∀ (k : ι'), x (Sum.inr k) = 0
have refine_1 : ∀
  (hx :
    Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x)
  (k : ι'), x (Sum.inr k) = 0
Tactic: refine ⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
refine_1 :
  ∀
    (hx :
      Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x)
    (k : ι'), x (Sum.inr k) = 0
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x ↔
    ∀ (k : ι'), x (Sum.inr k) = 0
have refine_2 : ∀ (hx : ∀ (k : ι'), x (Sum.inr k) = 0),
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
Tactic: refine ⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x_1 : ι ⊕ ι' → R
k : ι'
x : ι ⊕ ι' → R
h : Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1) x
⊢ x (Sum.inr k) = 0
have refine_1 : ∀ (i : ι),
  Eq.{u + 1} (α := R)
    ((fun (i : ι) ↦ (single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1 : (j : ι ⊕ ι') → R)) i (Sum.inr k)) 0
Tactic: obtain ⟨i, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
k : ι'
⊢ x (Sum.inr k) = 0
have refine_1 : ∀ (x : ι ⊕ ι' → R)
  (h :
    Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
      x),
  x (Sum.inr k) = 0
Tactic: induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
k : ι'
refine_1 :
  ∀ (x : ι ⊕ ι' → R)
    (h :
      Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
        x),
    x (Sum.inr k) = 0
⊢ x (Sum.inr k) = 0
have refine_1₁ : Eq.{u + 1} (α := R) (0 (Sum.inr k)) 0
Tactic: induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
k : ι'
refine_1 :
  ∀ (x : ι ⊕ ι' → R)
    (h :
      Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
        x),
    x (Sum.inr k) = 0
refine_1₁ : Eq.{u + 1} (α := R) (0 (Sum.inr k)) 0
⊢ x (Sum.inr k) = 0
have refine_1₂ : ∀ (u v : ι ⊕ ι' → R),
  Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u →
    Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) v →
      ∀ (hu : u (Sum.inr k) = 0) (hv : v (Sum.inr k) = 0), (u + v) (Sum.inr k) = 0
Tactic: induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
k : ι'
refine_1 :
  ∀ (x : ι ⊕ ι' → R)
    (h :
      Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
        x),
    x (Sum.inr k) = 0
refine_1₁ : Eq.{u + 1} (α := R) (0 (Sum.inr k)) 0
refine_1₂ :
  ∀ (u v : ι ⊕ ι' → R),
    Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u →
      Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
          (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) v →
        ∀ (hu : u (Sum.inr k) = 0) (hv : v (Sum.inr k) = 0), (u + v) (Sum.inr k) = 0
⊢ x (Sum.inr k) = 0
have refine_1₃ : ∀ (t : R) (u : ι ⊕ ι' → R),
  Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u →
    ∀ (hu : u (Sum.inr k) = 0), (t • u) (Sum.inr k) = 0
Tactic: induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
have refine_2 : ∀ (this : Fintype ι),
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this_1 : Fintype ι
this :
  x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
have rw : Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
  (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
  (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
have refine_2 : x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
Tactic: suffices x = ∑ i : ι, x (Sum.inl i) • Pi.single (M := fun _ ↦ R) (Sum.inl i) (1 : R) by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
have refine_2 : ∀ (i : ι),
  x (Sum.inl i) =
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
      (Sum.inl i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
refine_2 :
  ∀ (i : ι),
    x (Sum.inl i) =
      (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
        (Sum.inl i)
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
have refine_2₁ : ∀ (i : ι'),
  x (Sum.inr i) =
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
      (Sum.inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ motive' ((i : ι) → M i)
have intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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 ι
⊢ motive' ((i : ι) → M i)
have 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)
Tactic: revert M
Cleared hypotheses: M, inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
have 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)
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 ↦ ?_) ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ motive' ((i : ι) → M i)
have intro : ∀ (val : Fintype ι), 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
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)
⊢ motive' ((i : ι) → M i)
have 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)
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)
Cleared hypotheses: M, inst_2, inst_3, h