mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑0), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (0 x✝) a✝

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑0), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ = (0 x✝) a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² + x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : End (End R M) M
x✝ : ι →₀ M
a✝ : ι
⊢ ({ toFun := ⇑(mapRange.addMonoidHom ↑(x✝² + x✝¹)), map_add' := ⋯, map_smul' := ⋯ } x✝) a✝ =
    (({ toFun := ⇑(mapRange.addMonoidHom ↑x✝²), map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := ⇑(mapRange.addMonoidHom ↑x✝¹), map_add' := ⋯, map_smul' := ⋯ })
        x✝)
      a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (f (g • single i m)) i

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
f : End (End R (ι →₀ M)) (ι →₀ M)
g✝ : End R M
m : M
g : (ι →₀ M) →ₗ[R] ι →₀ M := mapRange.linearMap g✝
⊢ (f (single i (g✝ • m))) i = (f (g • single i m)) i
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ l a✝ = 0 a✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ l a✝ = 0 a✝
Module: Mathlib.LinearAlgebra.Finsupp.Defs

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x✝¹ : End (End R M) M
x✝ : M
⊢ ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ })
        ((↑↑(ringHomEndFinsupp ι)).toFun x✝¹))
      x✝ =
    x✝¹ x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
ι : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
x✝¹ : End (End R M) M
x✝ : M
⊢ ((fun f ↦ { toFun := fun m ↦ (f (single i m)) i, map_add' := ⋯, map_smul' := ⋯ })
        ((↑↑(ringHomEndFinsupp ι)).toFun x✝¹))
      x✝ =
    x✝¹ x✝
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: case e_g
α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ (fun a b ↦ f (single a (r • b))) = fun a b ↦ r • f (single a b)

Tactic:
;

Goal state after:
case e_g
α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ (fun a b ↦ f (single a (r • b))) = fun a b ↦ r • f (single a b)
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: case e_g
α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m✝ : ι →₀ M
i : ι
m : M
⊢ f (single i (r • m)) = r • f (single i m)

Tactic:
;

Goal state after:
case e_g
α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m✝ : ι →₀ M
i : ι
m : M
⊢ f (single i (r • m)) = r • f (single i m)
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMul R M
inst✝¹ : SMulZeroClass R N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
i : ι
⊢ (f (r • m)) i = (r • f m) i

Tactic:
;

Goal state after:
α : 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✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMul R M
inst✝¹ : SMulZeroClass R N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι →₀ N
r : R
m : M
i : ι
⊢ (f (r • m)) i = (r • f m) i
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
⊢ supported M R (bif true then s else t) ⊓ supported M R (bif false then s else t) = supported M R s ⊓ supported M R t
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
S : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
x✝ : M
⊢ ((lsum S) f ∘ₛₗ lsingle i) x✝ = (f i) x✝

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
S : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
f : α → M →ₛₗ[σ] N
i : α
x✝ : M
⊢ ((lsum S) f ∘ₛₗ lsingle i) x✝ = (f i) x✝
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
i : ι
n : ↥N
⊢ (mulLeftMap N m ∘ₗ lsingle i) n = (N.mulRightMap m ∘ₗ lsingle i) n

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
i : ι
n : ↥N
⊢ (mulLeftMap N m ∘ₗ lsingle i) n = (N.mulRightMap m ∘ₗ lsingle i) n
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case inr.refine_1
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ Function.invFunOn f s c ∈ s

Tactic:
exact Function.invFunOn_mem (by simpa using hl hc)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

pp: case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
;

Goal state after:
case pos
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

case neg
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : ¬HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
⊢ l = 0

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
⊢ l = 0
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g

Tactic:
;

Goal state after:
case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: case ofRepr.ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }

Tactic:
;

Goal state after:
case ofRepr.ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
x✝ : Fin n
⊢ x✝ ∈ ↑(s.attachFin h) ↔ x✝ ∈ Fin.val ⁻¹' ↑s

Tactic:
;

Goal state after:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
x✝ : Fin n
⊢ x✝ ∈ ↑(s.attachFin h) ↔ x✝ ∈ Fin.val ⁻¹' ↑s
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ image Fin.val (s.attachFin h) = s

Tactic:
by
  apply coe_injective
  rw [coe_image, coe_attachFin, Set.image_preimage_eq_iff]
  exact fun m hm ↦ ⟨⟨m, h m hm⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n x✝ : ℕ
⊢ x✝ ∈ range val ↔ x✝ ∈ Iio n

Tactic:
;

Goal state after:
n x✝ : ℕ
⊢ x✝ ∈ range val ↔ x✝ ∈ Iio n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Ici ↑i ∩ range val = Ico (↑i) n

Tactic:
range_val,

Goal state after:
n : ℕ
i : Fin n
⊢ Ici ↑i ∩ Iio n = Ico (↑i) n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Ioi ↑i ∩ range val = Ioo (↑i) n

Tactic:
range_val,

Goal state after:
n : ℕ
i : Fin n
⊢ Ioi ↑i ∩ Iio n = Ioo (↑i) n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iio ↑i ∩ range val = Iio ↑i

Tactic:
range_val,

Goal state after:
n : ℕ
i : Fin n
⊢ Iio ↑i ∩ Iio n = Iio ↑i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Icc ↑i ↑j ∩ range val = Icc ↑i ↑j

Tactic:
range_val,

Goal state after:
n : ℕ
i j : Fin n
⊢ Icc ↑i ↑j ∩ Iio n = Icc ↑i ↑j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ico ↑i ↑j ∩ range val = Ico ↑i ↑j

Tactic:
range_val,

Goal state after:
n : ℕ
i j : Fin n
⊢ Ico ↑i ↑j ∩ Iio n = Ico ↑i ↑j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ∩ range val = Ioc ↑i ↑j

Tactic:
range_val,

Goal state after:
n : ℕ
i j : Fin n
⊢ Ioc ↑i ↑j ∩ Iio n = Ioc ↑i ↑j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ Ioo ↑i ↑j ∩ range val = Ioo ↑i ↑j

Tactic:
range_val,

Goal state after:
n : ℕ
i j : Fin n
⊢ Ioo ↑i ↑j ∩ Iio n = Ioo ↑i ↑j
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
K : Type u_5
M : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h : (fun b i ↦ b.repr.symm (single i 1)) f = (fun b i ↦ b.repr.symm (single i 1)) g
a✝ : ι
⊢ (↑f.repr.symm ∘ₗ lsingle a✝) 1 = (↑g.repr.symm ∘ₗ lsingle a✝) 1

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
K : Type u_5
M : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h : (fun b i ↦ b.repr.symm (single i 1)) f = (fun b i ↦ b.repr.symm (single i 1)) g
a✝ : ι
⊢ (↑f.repr.symm ∘ₗ lsingle a✝) 1 = (↑g.repr.symm ∘ₗ lsingle a✝) 1
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x✝ ∈ Ici i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ici (natAdd m i) ↔ x✝ ∈ Ici i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x✝ ∈ Ioi i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioi (natAdd m i) ↔ x✝ ∈ Ioi i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x✝ ∈ Iic i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iic (natAdd m i) ↔ x✝ ∈ Iic i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x✝ ∈ Iio i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Iio (natAdd m i) ↔ x✝ ∈ Iio i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Icc i j

Tactic:
;

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Icc i j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ico i j

Tactic:
;

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ico (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ico i j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioc i j

Tactic:
;

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioc (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioc i j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioo i j

Tactic:
;

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ natAdd m ⁻¹' Ioo (natAdd m i) (natAdd m j) ↔ x✝ ∈ Ioo i j
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' uIoo (natAdd m i) (natAdd m j) = uIoo i j

Tactic:
simp [uIoo, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a ↦ a • (v ∘ Option.some) i

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r ↦ r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a ↦ a • (v ∘ Option.some) i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
x✝ : M
a✝ : ι
⊢ ((ofEquivFun v.equivFun).repr x✝) a✝ = (v.repr x✝) a✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
v : Basis ι R M
x✝ : M
a✝ : ι
⊢ ((ofEquivFun v.equivFun).repr x✝) a✝ = (v.repr x✝) a✝
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' uIoo i j = uIoo (natAdd m i) (natAdd m j)

Tactic:
simp [uIoo, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ici (i.addNat m) ↔ x✝ ∈ Ici i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ici (i.addNat m) ↔ x✝ ∈ Ici i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) ↔ x✝ ∈ Ioi i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) ↔ x✝ ∈ Ioi i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Iic (i.addNat m) ↔ x✝ ∈ Iic i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Iic (i.addNat m) ↔ x✝ ∈ Iic i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Iio (i.addNat m) ↔ x✝ ∈ Iio i

Tactic:
;

Goal state after:
n m : ℕ
i x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Iio (i.addNat m) ↔ x✝ ∈ Iio i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_9
β : Type u_10
A : α → M
B : β → α →₀ R
f : β →₀ R
⊢ (linearCombination R A) ((linearCombination R B) f) = (linearCombination R fun b ↦ (linearCombination R A) (B b)) f

Tactic:
by
  classical
  simp only [linearCombination_apply]
  induction f using induction_linear with
  | zero => simp only [sum_zero_index]
  | add f₁ f₂ h₁ h₂ => simp [sum_add_index, h₁, h₂, add_smul]
  | single => simp [sum_single_index, sum_smul_index, smul_sum, mul_smul]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) ↔ x✝ ∈ Icc i j

Tactic:
;

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Icc (i.addNat m) (j.addNat m) ↔ x✝ ∈ Icc i j
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
a✝ : α × α'
⊢ ((linearCombination R fun i ↦ w i.2 • v i.1) ∘ₗ lsingle a✝) 1 =
    ((↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(curryLinearEquiv R)) ∘ₗ lsingle a✝)
      1

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
a✝ : α × α'
⊢ ((linearCombination R fun i ↦ w i.2 • v i.1) ∘ₗ lsingle a✝) 1 =
    ((↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(curryLinearEquiv R)) ∘ₗ lsingle a✝)
      1