mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
rw [← preimage_natAdd_Ici_natAdd, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ range (natAdd m)
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
⊢ (ofEquivFun v.equivFun).repr = v.repr

Tactic:
ext

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 : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ici (i.addNat m) = Ici i

Tactic:
ext

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 : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Ioi (i.addNat m) = Ioi i

Tactic:
ext

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 : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iic (i.addNat m) = Iic i

Tactic:
ext

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 : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' Iio (i.addNat m) = Iio i

Tactic:
ext

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

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

Tactic:
ext

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
⊢ (linearCombination R fun i ↦ w i.2 • v i.1) =
    ↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(curryLinearEquiv R)

Tactic:
ext

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
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
n m : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ioo i j
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 α
⊢ map (LinearMap.codRestrict (span R (v '' s)) (linearCombination R v ∘ₗ (supported R R s).subtype) ⋯) ⊤ = ⊤

Tactic:
LinearMap.map_codRestrict,

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 : α → M
s : Set α
⊢ comap (span R (v '' s)).subtype (map (linearCombination R v ∘ₗ (supported R R s).subtype) ⊤) = ⊤
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 α
⊢ linearCombination R (s.domRestrict v) =
    (span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm

Tactic:
ext

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 : α → M
s : Set α
a✝ : ↑s
⊢ (linearCombination R (s.domRestrict v) ∘ₗ lsingle a✝) 1 =
    (((span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm) ∘ₗ lsingle a✝) 1
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
α' : Type u_7
v : α → M
f : α' → α
⊢ linearCombination R (v ∘ f) = linearCombination R v ∘ₗ lmapDomain R R f

Tactic:
ext

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
v : α → M
f : α' → α
a✝ : α'
⊢ (linearCombination R (v ∘ f) ∘ₗ lsingle a✝) 1 = ((linearCombination R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Ici i = Iic i.rev

Tactic:
ext

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ici i ↔ x✝ ∈ Iic i.rev
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Ioi i = Iio i.rev

Tactic:
ext

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioi i ↔ x✝ ∈ Iio i.rev
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Iic i = Ici i.rev

Tactic:
ext

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iic i ↔ x✝ ∈ Ici i.rev
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ rev ⁻¹' Iio i = Ioi i.rev

Tactic:
ext

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iio i ↔ x✝ ∈ Ioi i.rev
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' Icc i j = Icc j.rev i.rev

Tactic:
ext

Goal state after:
n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Icc i j ↔ x✝ ∈ Icc j.rev i.rev
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₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
⊢ b₁.repr = b₂.repr

Tactic:
ext

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
x✝ : M
a✝ : ι
⊢ (b₁.repr x✝) a✝ = (b₂.repr x✝) a✝
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ico i j = Ioc j.rev i.rev

Tactic:
ext

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ioc i j = Ico j.rev i.rev

Tactic:
ext

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ rev ⁻¹' Ioo i j = Ioo j.rev i.rev

Tactic:
ext

Goal state after:
n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioo i j ↔ x✝ ∈ Ioo j.rev i.rev
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
u v : α → M
⊢ linearCombination R (u + v) = linearCombination R u + linearCombination R v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
u v : α → M
a✝ : α
⊢ (linearCombination R (u + v) ∘ₗ lsingle a✝) 1 = ((linearCombination R u + linearCombination R v) ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
r : S
v : α → M
⊢ linearCombination R (r • v) = (RingHom.id S) r • linearCombination R v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
M' : Type u_8
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
v✝ : α → M
v' : α' → M'
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
r : S
v : α → M
a✝ : α
⊢ (linearCombination R (r • v) ∘ₗ lsingle a✝) 1 = (((RingHom.id S) r • linearCombination R v) ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (Fintype.linearCombination R v) (Pi.single i r) = r • v i

Tactic:
simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x, if x = i then r • v x else 0) = r • v i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ u v : α → M
⊢ Fintype.linearCombination R (u + v) = Fintype.linearCombination R u + Fintype.linearCombination R v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ u v : α → M
x✝ : α → R
⊢ (Fintype.linearCombination R (u + v)) x✝ = (Fintype.linearCombination R u + Fintype.linearCombination R v) x✝
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ : α → M
r : S
v : α → M
⊢ Fintype.linearCombination R (r • v) = (RingHom.id S) r • Fintype.linearCombination R v

Tactic:
ext

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v✝ : α → M
r : S
v : α → M
x✝ : α → R
⊢ (Fintype.linearCombination R (r • v)) x✝ = ((RingHom.id S) r • Fintype.linearCombination R v) x✝
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'
⊢ (fun f i ↦ f (b i)) ((fun f ↦ linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ ↑b.repr) f) = f

Tactic:
ext

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'
ι : 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✝
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'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ f (g (b' i)) = LinearMap.id (b' i)

Tactic:
hfg,

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'✝
ι : 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'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ b' i = LinearMap.id (b' 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 : ι), (b.coord i) x = 0) ↔ b.repr x = 0

Tactic:
by simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply]

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

Goal state before:
pp: n : ℕ
⊢ map valEmbedding univ = Iio n

Tactic:
ext

Goal state after:
n a✝ : ℕ
⊢ a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
⊢ ↑(Ioi 0) = ↑(map (succEmb n) univ)

Tactic:
ext

Goal state after:
n : ℕ
x✝ : Fin n.succ
⊢ x✝ ∈ ↑(Ioi 0) ↔ x✝ ∈ ↑(map (succEmb n) univ)
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
⊢ ↑(Iio (last n)) = ↑(map castSuccEmb univ)

Tactic:
ext

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
⊢ x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
ext

Goal state after:
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Ico (↑a) n).attachFin ⋯ ↔ a✝ ∈ Ici a
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
ext

Goal state after:
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Ioo (↑a) n).attachFin ⋯ ↔ a✝ ∈ Ioi a
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
ext

Goal state after:
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Iic ↑a).attachFin ⋯ ↔ a✝ ∈ Iic a
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
ext

Goal state after:
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ (Iio ↑a).attachFin ⋯ ↔ a✝ ∈ Iio a
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioo (↑a) n

Tactic:
← attachFin_Ioo_eq_Ioi,

Goal state after:
n : ℕ
a : Fin n
⊢ map valEmbedding ((Ioo (↑a) n).attachFin ⋯) = Ioo (↑a) n
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
⊢ image val univ = range n

Tactic:
ext

Goal state after:
n a✝ : ℕ
⊢ a✝ ∈ image val univ ↔ a✝ ∈ range n
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
⊢ linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀) = linearCombination R (v + fun x ↦ c x • v i)

Tactic:
ext

Goal state after:
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
a✝ : ι
⊢ ((linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀)) ∘ₗ lsingle a✝) 1 =
    (linearCombination R (v + fun x ↦ c x • v i) ∘ₗ lsingle a✝) 1
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u

Tactic:
ext

Goal state after:
α : Type u
m : ℕ
x : α
u : Fin m → α
x✝ : Fin m
⊢ vecTail (vecCons x u) x✝ = u x✝
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ ![] v = v

Tactic:
ext

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin n
⊢ vecAppend ⋯ ![] v x✝ = v x✝
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) ∩ mulSupport f

Tactic:
← image_inter_mulSupport_eq,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = g '' s ∩ mulSupport f ∩ mulSupport f
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ v ![] = v

Tactic:
ext

Goal state after:
α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin (n + 0)
⊢ vecAppend ⋯ v ![] x✝ = v x✝
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n k : ℕ
h : k < n
⊢ (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

Tactic:
ext

Goal state after:
n k : ℕ
h : k < n
⊢ ↑((finRotate (n + 1)) ⟨k, ⋯⟩) = ↑⟨k + 1, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ (if h_1 : ↑⟨i, h⟩ < n then cast ⋯ (v (⟨i, h⟩.castLT h_1)) else cast ⋯ a) = cons a v ⟨i + 1, ⋯⟩

Tactic:
Fin.cons,

Goal state after:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ (if h_1 : ↑⟨i, h⟩ < n then cast ⋯ (v (⟨i, h⟩.castLT h_1)) else cast ⋯ a) = cases a v ⟨i + 1, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ (if h_1 : ↑⟨n, h⟩ < n then cast ⋯ (v (⟨n, h⟩.castLT h_1)) else cast ⋯ a) = cons a v ⟨0, ⋯⟩

Tactic:
Fin.cons,

Goal state after:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ (if h_1 : ↑⟨n, h⟩ < n then cast ⋯ (v (⟨n, h⟩.castLT h_1)) else cast ⋯ a) = cases a v ⟨0, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
· have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
    subst h''
    rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
    rfl

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
have h_x_eq_y : x = y := by
      rw [Subtype.ext_iff, ← hy₂]
      simp

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
h_x_eq_y : x = y
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ (Basis.span hli) i = ⟨v i, ⋯⟩

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
i : ι
⊢ ↑((Basis.span hli) i) = ↑⟨v i, ⋯⟩
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_7
M : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
h : span R (range v) = span R (range (-v))
⊢ Basis.span ⋯ =
    (Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_7
M : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
h : span R (range v) = span R (range (-v))
i✝ : ι
⊢ ↑((Basis.span ⋯) i✝) =
    ↑(((Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)) i✝)