mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : α → M →ₛₗ[σ] N
x : α
y : M
⊢ ((fun F x ↦ F ∘ₛₗ lsingle x) ((fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ }) F) x)
      y =
    (F x) y

Tactic:
simp

Goal state after:
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
inst✝¹ : Module S N
inst✝ : SMulCommClass R₂ S N
F : (α →₀ M) →ₛₗ[σ] N
x : α
y : M
⊢ ((fun F ↦ { toFun := fun d ↦ d.sum fun i ↦ ⇑(F i), map_add' := ⋯, map_smul' := ⋯ })
          ((fun F x ↦ F ∘ₛₗ lsingle x) F) ∘ₛₗ
        lsingle x)
      y =
    (F ∘ₛₗ lsingle x) y

Tactic:
simp

Goal state after:
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:
simp

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

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
e : α₁ ≃ α₂
i : α₁
m : M
⊢ (Finsupp.domLCongr e) (single i m) = single (e i) m

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
N : Type u_3
R : Type u_5
R₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R₂ N
σ : R →+* R₂
σ_inv : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ_inv
inst✝ : RingHomInvPair σ_inv σ
ι : Type u_9
κ : Type u_10
e₁ : ι ≃ κ
e₂ : M ≃ₛₗ[σ] N
k : κ
n : N
⊢ (lcongr e₁ e₂) ((lcongr e₁ e₂).symm (single k n)) = (lcongr e₁ e₂) (single (e₁.symm k) (e₂.symm n))

Tactic:
simp

Goal state after:
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 : Set α
i : ↑s
a : M
⊢ ↑((supportedEquivFinsupp s).symm (single i a)) = single (↑i) a

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → M
⊢ 0 • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), 0 • f i

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iic ↑i ⊆ range val

Tactic:
simp [range_val]

Goal state after:
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
b : Basis ι R M
v : ι →₀ R
⊢ b.repr.symm v = b.repr.symm (v.sum single)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
a✝ : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1 = (linearCombination R (v' ∘ f) ∘ₗ lsingle a✝) 1

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
e : ι ≃ ι'
i' : ι'
⊢ ((Finsupp.domLCongr e) (b.repr x)) i' = (b.repr x) (e.symm i')

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (s.mulIndicator f) ⊆ ↑t
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i

Tactic:
rw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (s.mulIndicator f) ⊆ ↑t
⊢ ∏ i ∈ t, s.mulIndicator f i = ∏ i ∈ t, f i
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:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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 : α → M
s : Set α
x : M
⊢ x ∈ map (linearCombination R v) (supported R R s) ↔ ∃ l ∈ supported R R s, (linearCombination R v) l = x

Tactic:
simp

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:
simp

Goal state after:
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 ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ ((ofEquivFun e).repr j) x✝ = e j x✝

Tactic:
Basis.ofEquivFun_repr_apply

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:
simp

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) ⁻¹' Ioi (i.addNat m) ↔ x✝ ∈ Ioi i

Tactic:
simp

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) ⁻¹' Iic (i.addNat m) ↔ x✝ ∈ Iic i

Tactic:
simp

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) ⁻¹' Iio (i.addNat m) ↔ x✝ ∈ Iio i

Tactic:
simp

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:
simp

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) ⁻¹' Ico (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ico i j

Tactic:
simp

Goal state after:
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:
simp

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) ⁻¹' Ioc (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ioc i j

Tactic:
simp

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) ⁻¹' Ioo (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ioo i j

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' uIcc (i.addNat m) (j.addNat m) = uIcc i j

Tactic:
simp [uIcc, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ici (i.addNat m) ⊆ range fun x ↦ x.addNat m

Tactic:
intro j

Goal state after:
n m : ℕ
i : Fin n
j : Fin (n + m)
⊢ j ∈ Ici (i.addNat m) → j ∈ range fun x ↦ x.addNat m
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' uIcc i j = uIcc (i.addNat m) (j.addNat m)

Tactic:
simp [uIcc, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ᶠ (a : α), g a

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)

Goal state after:
α : Type u_1
M : Type u_5
inst✝² : CommMonoid M
f g : α → M
inst✝¹ : PartialOrder M
inst✝ : MulLeftMono M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
i : ι
⊢ (b.mapCoeffs f h).repr (b i) = single i 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ᶠ (a : α), g a

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)

Goal state after:
α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
this : Fintype ↑(mulSupport f ∪ mulSupport g)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x✝ : M
i✝ : ι
a✝ : Nontrivial R
c : R
x : M
i : ι
⊢ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩ = (c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩) i

Tactic:
simp

Goal state after:
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'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
⊢ ∀ (a : M), a ∈ range ⇑b ↔ (Equiv.refl M) a ∈ Finset.image (⇑b) Finset.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
⊢ ∏ᶠ (i : α) (_ : i ∈ s), 1 = 1

Tactic:
simp

Goal state after:
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'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f g : ι → M'
i : ι
⊢ (linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ ↑b.repr) (b i) =
    (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr + linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ ↑b.repr)
      (b i)

Tactic:
simp

Goal state after:
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'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
c : S
f : ι → M'
i : ι
⊢ (linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ ↑b.repr) (b i) =
    ((RingHom.id S) c • linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) (b i)

Tactic:
simp

Goal state after:
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'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
x✝ : ι
⊢ (fun f i ↦ f (b i)) ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) f) x✝ = f x✝

Tactic:
simp

Goal state after:
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'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
b : Basis ι R M
inst✝³ : Module R M'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M →ₗ[R] M'
i : ι
⊢ ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) ((fun f i ↦ f (b i)) f)) (b i) = f (b i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
⊢ ∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ (b.equiv b (Equiv.refl ι)) (b i) = (LinearEquiv.refl R M) (b i)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Module R M'
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι'
⊢ (b.equiv b' e) ((b.equiv b' e).symm (b' i)) = (b.equiv b' e) ((b'.equiv b e.symm) (b' i))

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁶ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
inst✝² : Module R M'
M'' : Type u_13
b' : Basis ι' R M'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
ι'' : Type u_14
b'' : Basis ι'' R M''
e : ι ≃ ι'
e' : ι' ≃ ι''
i : ι
⊢ (b.equiv b' e ≪≫ₗ b'.equiv b'' e') (b i) = (b.equiv b'' (e.trans e')) (b i)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ (b.map (b.equiv b' e)) i = (b'.reindex e.symm) i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ b.map (b.equiv b' e) = b'.reindex e.symm

Tactic:
ext i
  simp

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) ↑i • v ↑i = ∑ i, c i • v ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
m : M
r : R
⊢ (b.coord i) (r • m) = r * (b.coord i) m

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Ioi i.succ = map (succEmb n) (Ioi i)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iio i.castSucc = map castSuccEmb (Iio i)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
⊢ #{i | Vector.nil.get i = a} = List.count a Vector.nil.toList

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Icc ↑a ↑b).attachFin ⋯ ↔ a ≤ x ∧ x ≤ b

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ico ↑a ↑b).attachFin ⋯ ↔ a ≤ x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ioc ↑a ↑b).attachFin ⋯ ↔ a < x ∧ x ≤ b

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ioo ↑a ↑b).attachFin ⋯ ↔ a < x ∧ x < b

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Ico (↑a) n).attachFin ⋯ ↔ a✝ ∈ Ici a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Ioo (↑a) n).attachFin ⋯ ↔ a✝ ∈ Ioi a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Iic ↑a).attachFin ⋯ ↔ a✝ ∈ Iic a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Iio ↑a).attachFin ⋯ ↔ a✝ ∈ Iio a

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ (fun f ↦ (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (cons s (cons t finZeroElim))

Tactic:
by
  ext f
  simp [Fin.forall_fin_two]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i x : Fin (n + 1)
⊢ (fun x ↦ x.casesOn' i i.succAbove) (i.insertNth none some i) = i

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i x : Fin (n + 1)
j : Fin n
⊢ (fun x ↦ x.casesOn' i i.succAbove) (i.insertNth none some (i.succAbove j)) = i.succAbove j

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case none
m n : ℕ
i : Fin (n + 1)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) none) = none

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) (some val✝)) = some val✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
j i : Fin n
hi : i.castSucc ≠ Fin.last n
hj : i.castSucc.succAbove j ≠ i.castSucc
⊢ (finSuccEquiv' i.castSucc) (i.castSucc.succAbove j) = some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case pos.zero
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : 0 < o + 1
h : ↑⟨0, hi⟩ < m + 1
⊢ vecCons x u ⟨↑⟨0, hi⟩, h⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨0, hi⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case pos
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ↑i < m + 1
⊢ vecCons x u ⟨↑i, h⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩
    · simp
    · simp only [Nat.add_lt_add_iff_right] at h
      simp [h]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
m n : ℕ
y : Fin m
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y

Tactic:
simp

Goal state after: