mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

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 x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ioc (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ioc i j

Tactic:
;

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 x✝ : Fin n
⊢ x✝ ∈ (fun x ↦ x.addNat m) ⁻¹' Ioo (i.addNat m) (j.addNat m) ↔ x✝ ∈ Ioo i j

Tactic:
;

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 α
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

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 : α → 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 : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v 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
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a ↦ a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ici i ↔ x✝ ∈ Iic i.rev

Tactic:
;

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 x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioi i ↔ x✝ ∈ Iio i.rev

Tactic:
;

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioi i ↔ x✝ ∈ Iio i.rev
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)
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
let s := (f.mulSupport ∪ g.mulSupport).toFinset

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
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iic i ↔ x✝ ∈ Ici i.rev

Tactic:
;

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 x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iio i ↔ x✝ ∈ Ioi i.rev

Tactic:
;

Goal state after:
n : ℕ
i x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Iio i ↔ x✝ ∈ Ioi 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
x✝ : M
a✝ : ι
⊢ (b₁.repr x✝) a✝ = (b₂.repr x✝) a✝

Tactic:
;

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 x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Icc i j ↔ x✝ ∈ Icc j.rev i.rev

Tactic:
;

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

Goal state before:
pp: n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ico i j ↔ x✝ ∈ Ioc j.rev i.rev

Tactic:
;

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 x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioc i j ↔ x✝ ∈ Ico j.rev i.rev

Tactic:
;

Goal state after:
n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioc i j ↔ x✝ ∈ Ico j.rev i.rev
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)
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
let s := (f.mulSupport ∪ g.mulSupport).toFinset

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
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j x✝ : Fin n
⊢ x✝ ∈ rev ⁻¹' Ioo i j ↔ x✝ ∈ Ioo j.rev i.rev

Tactic:
;

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
a✝ : α
⊢ (linearCombination R (u + v) ∘ₗ lsingle a✝) 1 = ((linearCombination R u + linearCombination R v) ∘ₗ lsingle a✝) 1

Tactic:
;

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
a✝ : α
⊢ (linearCombination R (r • v) ∘ₗ lsingle a✝) 1 = (((RingHom.id S) r • linearCombination R v) ∘ₗ lsingle a✝) 1

Tactic:
;

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
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ x, (f x + g x) • v x

Tactic:
;

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
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ x, (f x + g x) • 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 : R
f : α → R
⊢ ∑ i, (r • f) i • v i = ∑ x, ((RingHom.id R) r * f x) • v x

Tactic:
;

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 : R
f : α → R
⊢ ∑ i, (r • f) i • v i = ∑ x, ((RingHom.id R) r * f x) • 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✝ u v : α → M
x✝ : α → R
⊢ (Fintype.linearCombination R (u + v)) x✝ = (Fintype.linearCombination R u + Fintype.linearCombination R v) x✝

Tactic:
;

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
x✝ : α → R
⊢ (Fintype.linearCombination R (r • v)) x✝ = ((RingHom.id S) r • Fintype.linearCombination R v) x✝

Tactic:
;

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.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set α
ht : t.Finite
s : Finset α
⊢ (∏ᶠ (i : α) (_ : i ∈ ↑s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ ↑s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ ↑s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : M → R
t : Finset M
hts : ↑t ⊆ s
⊢ ∑ a ∈ t, n a • a ∈ span R s

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : M → R
t : Finset M
hts : ↑t ⊆ s
⊢ ∑ a ∈ t, n a • a ∈ span R s
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
f : M → R
⊢ ∑ a ∈ s, f a • a ∈ span R ↑s

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
f : M → R
⊢ ∑ a ∈ s, f a • a ∈ span R ↑s
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
x✝ : Fin n.succ
⊢ x✝ ∈ ↑(Ioi 0) ↔ x✝ ∈ ↑(map (succEmb n) univ)

Tactic:
;

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 : ℕ
x✝ : Fin (n + 1)
⊢ x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)

Tactic:
;

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}

Tactic:
;

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x ↦ p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
h : m ∈ span R s
⊢ ∃ n f g, ∑ i, f i • ↑(g i) = m

Tactic:
rcases mem_span_set.1 h with ⟨c, cs, rfl⟩
    have A : c.support ≃ Fin c.support.card := Finset.equivFin _
    refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
    rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]
    exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}) = (if p 0 then 1 else 0) + #{x | p x.succ}

Tactic:
;

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}) = (if p 0 then 1 else 0) + #{x | p x.succ}
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
;

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 a✝ : Fin n
⊢ a✝ ∈ (Ioo (↑a) n).attachFin ⋯ ↔ a✝ ∈ Ioi a

Tactic:
;

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 a✝ : Fin n
⊢ a✝ ∈ (Iic ↑a).attachFin ⋯ ↔ a✝ ∈ Iic a

Tactic:
;

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 a✝ : Fin n
⊢ a✝ ∈ (Iio ↑a).attachFin ⋯ ↔ a✝ ∈ Iio a

Tactic:
;

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ min n #{i | p i}

Tactic:
;

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ min n #{i | p i}
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
a✝ : ι
⊢ ((linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀)) ∘ₗ lsingle a✝) 1 =
    (linearCombination R (v + fun x ↦ c x • v i) ∘ₗ lsingle a✝) 1

Tactic:
;

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: case zero
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi✝ : i < 0 + 1
hi : i = 0
⊢ (if h : ↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi✝⟩ + ⟨i, hi✝⟩ + 1)

Tactic:
;

Goal state after:
case zero
α : Type u
v : Fin (0 + 1) → α
i : ℕ
hi✝ : i < 0 + 1
hi : i = 0
⊢ (if h : ↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 < 0 + 1 then v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1, ⋯⟩
    else v ⟨↑⟨i, hi✝⟩ + ↑⟨i, hi✝⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨i, hi✝⟩ + ⟨i, hi✝⟩ + 1)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case zero
α : Type u
v : Fin (0 + 1) → α
hi : 0 < 0 + 1
⊢ (if h : ↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨0, hi⟩ + ⟨0, hi⟩ + 1)

Tactic:
;

Goal state after:
case zero
α : Type u
v : Fin (0 + 1) → α
hi : 0 < 0 + 1
⊢ (if h : ↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 < 0 + 1 then v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩
    else v ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1 - (0 + 1), ⋯⟩) =
    v (⟨0, hi⟩ + ⟨0, hi⟩ + 1)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
rw [Fin.val_mk, not_lt] at h
      simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
      refine (Nat.mod_eq_of_lt ?_).symm
      lia

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1) i

Tactic:
;

Goal state after:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1) i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1 + 1) i

Tactic:
;

Goal state after:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 ↦ n_1 + n_1 + 1) i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)

Tactic:
← Set.insert_sdiff_self_of_mem has

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∈ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a (s \ {a})), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ HasFiniteMulSupport fun i ↦ f i a

Tactic:
fun_prop (disch := simp)

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

Goal state before:
pp: n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i

Tactic:
;

Goal state after:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i - k) ((fun i ↦ i + k) i) = i
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i

Tactic:
;

Goal state after:
n : ℕ
k i : Fin n
this : NeZero n
⊢ (fun i ↦ i + k) ((fun i ↦ i - k) i) = i
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n✝ n : ℕ
k i : Fin (n + 1)
⊢ ↑((finCycle k) i) = ↑((⇑(finRotate (n + 1)))^[↑k] i)

Tactic:
;

Goal state after:
n✝ n : ℕ
k i : Fin (n + 1)
⊢ ↑((finCycle k) i) = ↑((⇑(finRotate (n + 1)))^[↑k] 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
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
i : ι
⊢ b i ∈ ↑p

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
i : ι
⊢ b i ∈ ↑p
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
⊢ LinearIndependent R b.coord

Tactic:
refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_
  simpa [hj, Finsupp.single_apply] using congr($h (b j))

Goal state after:
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))
i✝ : ι
⊢ ↑((Basis.span ⋯) i✝) =
    ↑(((Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)) i✝)

Tactic:
;

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✝)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x✝ : ι
⊢ (Basis.singleton ι R) x✝ = 1 x✝

Tactic:
;

Goal state after:
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x✝ : ι
⊢ (Basis.singleton ι R) x✝ = 1 x✝
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
inst✝ : IsDomain R
b : Basis ι R M
c : R
x : M
this : IsTorsionFree R M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
c : R
x : M
this : IsTorsionFree R M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
x✝ : R
⊢ x✝ • v i = (⇑(Finsupp.linearCombination R v) ∘ Finsupp.single i) x✝

Tactic:
;

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
x✝ : R
⊢ x✝ • v i = (⇑(Finsupp.linearCombination R v) ∘ Finsupp.single i) x✝