awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
⊢ IsPeriodicPt (fun (x : M ≃ₗ[R] M) ↦ e * x) k 1
have h : ∀ (m : M), Eq (α := M) (((fun (x : M ≃ₗ[R] M) ↦ e * x)^[k] 1 : (a : M) → M) m : M) ((1 : (a : M) → M) m : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
m : M
⊢ Eq (α := M) (((fun (x : M ≃ₗ[R] M) ↦ e * x)^[k] 1 : (a : M) → M) m : M) ((1 : (a : M) → M) m : M)
have hm : Membership.mem (γ := Submodule R M) (span R Φ) m
Tactic: have hm : m ∈ span R Φ := hΦ₂ ▸ Submodule.mem_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
⊢ Eq (α := M) (((fun (x : M ≃ₗ[R] M) ↦ e * x)^[k] 1 : (a : M) → M) m : M) ((1 : (a : M) → M) m : M)
have h : (e ^ k : (a : M) → M) m = m
Tactic: simp only [mul_left_iterate, mul_one, LinearEquiv.coe_one, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
⊢ (e ^ k : (a : M) → M) m = m
have h : ∀ (x : M) (hx : x ∈ Φ), (e ^ k : (a : M) → M) x = x
Tactic: refine Submodule.span_induction (fun x hx ↦ ?_) (by simp)
    (fun x y _ _ hx hy ↦ by simp [map_add, hx, hy]) (fun t x _ hx ↦ by simp [hx]) hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
⊢ (e ^ k : (a : M) → M) x = x
have h : (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ sorry)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
Tactic: rw [LinearEquiv.pow_apply, ← he.1.coe_iterate_restrict ⟨x, hx⟩ k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
hk : IsPeriodicPt (fun (x : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2)) ↦ e' * x) k 1
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have hk₁ : e' ^ k = 1
Tactic: replace hk : (e') ^ k = 1 := by simpa [IsPeriodicPt, IsFixedPt] using hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk : e' ^ k = 1
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have hk₁ : Eq (α := (↑Φ : Type u_2))
  ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
  ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
Tactic: replace hk := Equiv.congr_fun hk ⟨x, hx⟩
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk :
  Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have h : ∀
  (hk :
    (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
      id (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)),
  (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ sorry)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
Tactic: rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk :
  Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
h :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        id (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have h₁ : ∀
  (hk :
    (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
      Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx),
  (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ sorry)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
Tactic: rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk :
  Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
h :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        id (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₁ :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have h₂ : ∀
  (hk :
    (↑((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) =
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : M)),
  (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ sorry)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
Tactic: rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.FiniteSpan (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
e : M ≃ₗ[R] M
he : BijOn (⇑e : (a : M) → M) Φ Φ
e' : (↑Φ : Type u_2) ≃ (↑Φ : Type u_2) := BijOn.equiv (s := Φ) (t := Φ) (⇑e : (a : M) → M) he
this : Finite.{u_2 + 1} (↑Φ : Type u_2)
k : ℕ
hk₀ : k > 0
m : M
hm : Membership.mem (γ := Submodule R M) (span R Φ) m
x : M
hx : x ∈ Φ
hk :
  Eq (α := (↑Φ : Type u_2))
    ((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
    ((1 : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : (↑Φ : Type u_2))
h :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        id (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₁ :
  ∀
    (hk :
      (e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) =
        Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
h₂ :
  ∀
    (hk :
      (↑((e' ^ k : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2)) (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) =
        (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : M)),
    (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
⊢ (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ ⋯)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
have h₃ : ∀
  (hk :
    (↑((⇑e' : (a : (↑Φ : Type u_2)) → (↑Φ : Type u_2))^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) =
      (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx) : M)),
  (↑((MapsTo.restrict (⇑e : (a : M) → M) Φ Φ sorry)^[k] (Subtype.mk (p := fun (x : M) ↦ x ∈ Φ) x hx)) : M) = x
Tactic: rwa [Equiv.Perm.coe_one, id_eq, Subtype.ext_iff, Equiv.Perm.coe_pow] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (lapply a ∘ₗ lsingle a) LinearMap.id
have h : ∀ (x : M), Eq (α := M) ((lapply a ∘ₗ lsingle a : (a : M) → M) x : M) ((LinearMap.id : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a a' : α
h : a ≠ a'
⊢ Eq.{u_2 + 1} (α := M →ₗ[R] M) (lapply a ∘ₗ lsingle a') 0
have h₁ : ∀ (x : M), Eq (α := M) ((lapply a ∘ₗ lsingle a' : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
x y : β →₀ M
⊢ comapDomain f (x + y) ⋯ = comapDomain f x ⋯ + comapDomain f y ⋯
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := M) ((comapDomain f (x + y) sorry : (a : α) → M) a : M)
    ((comapDomain f x sorry + comapDomain f y sorry : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
β : Type u_9
f : α → β
hf : Function.Injective f
c : R
x : β →₀ M
⊢ comapDomain f (c • x) ⋯ = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (comapDomain f x ⋯)
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := M) ((comapDomain f (c • x) sorry : (a : α) → M) a : M)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (comapDomain f x sorry) : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
α_1 : Type u_1
M_1 : Type u_2
N : Type u_3
P : Type u_4
R_1 : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst : Semiring R_1
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : Semiring S
inst_4 : AddCommMonoid M_1
inst_5 : Module R_1 M_1
inst_6 : AddCommMonoid N
inst_7 : Module R₂ N
inst_8 : AddCommMonoid P
inst_9 : Module R₃ P
σ₁₂ : R_1 →+* R₂
σ₂₁ : R₂ →+* R_1
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R_1 →+* R₃
σ₃₁ : R₃ →+* R_1
inst_10 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_11 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
α : Type u_9
β : Type u_10
R : Type u_11
M : Type u_12
inst_12 : Semiring R
inst_13 : AddCommMonoid M
inst_14 : Module R M
c : R
f : α × β →₀ M
⊢ Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (c • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) f)
have h : ∀ (a : α) (a_1 : β),
  Eq.{u_12 + 1} (α := M)
    ((((Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (c • f) : (a : α) → β →₀ M) a : β →₀ M) : (a : β) → M) a_1 : M)
    ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) f) :
                (a : α) → β →₀ M)
              a :
            β →₀ M) :
          (a : β) → M)
        a_1 :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x_1 x_2 : ι →₀ M
h :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M)
h' :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_2 : ι →₀ M)
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • (x_1 + x_2)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
have rw : (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1 + g • x_2) =
  HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
    ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
Tactic: rw [smul_add, map_add, h, h', map_add, smul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x_1 x_2 : ι →₀ M
h :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M)
h' :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_2 : ι →₀ M)
rw :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1 + g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • (x_1 + x_2)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
have rw₁ : HAdd.hAdd (α := ι →₀ M) (β := ι →₀ M) ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) : ι →₀ M)
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) : ι →₀ M) =
  HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
    ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
Tactic: rw [smul_add, map_add, h, h', map_add, smul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x_1 x_2 : ι →₀ M
h :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M)
h' :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_2 : ι →₀ M)
rw :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1 + g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
rw₁ :
  HAdd.hAdd (α := ι →₀ M) (β := ι →₀ M)
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) : ι →₀ M)
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) : ι →₀ M) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • (x_1 + x_2)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
have rw₂ : HAdd.hAdd (β := ι →₀ M)
    (HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M))
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) : ι →₀ M) =
  HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
    ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
Tactic: rw [smul_add, map_add, h, h', map_add, smul_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x : ι →₀ M
i : ι
m : M
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M)
have h : ∀ (j : ι),
  Eq.{u_6 + 1} (α := M)
    ((((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (HSMul.hSMul (β := ι →₀ M) g (single i m)) :
            ι →₀ M) :
          (a : ι) → M)
        j :
      M)
    ((HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
            ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
            ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (single i m) : ι →₀ M) :
          (a : ι) → M)
        j :
      M)
Tactic: ext j