mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ∀ (x : α), ¬(x ≤ b ∧ a ⋖ x)
⊢ x ≤ a

Tactic:
not_and

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ∀ x ≤ b, ¬a ⋖ x
⊢ x ≤ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
s : Set α
a : α
ha : a ∈ s
⊢ Disjoint a (⨆ a_1 ∈ s \ {a}, a_1) ↔ Disjoint a (⨆ j, ⨆ (_ : j ≠ ⟨a, ha⟩), ↑j)

Tactic:
simp [iSup_subtype, iSup_and]

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
by
  by_cases h : a ∈ s
  · exact Or.inr (mulIndicator_of_mem h f)
  · exact Or.inl (mulIndicator_of_notMem h f)

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr.refine_2.refl
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : ↑(Iic k)
c₀ : ¬c = ⊤
ba : b ≤ ↑c
h : Maximal (fun x ↦ x ∈ Iio k) ↑c
hck : ⟨↑c, ⋯⟩ < c
⊢ False

Tactic:
exact lt_irrefl _ hck

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.List

Goal state before:
pp: R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ l.sum

Tactic:
induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

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

Goal state before:
pp: case mem_mem
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
u : M
v : N
hu : u ∈ s
hv : v ∈ t
⊢ (B u) v ∈ P'

Tactic:
exact hB u hu v hv

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

Goal state before:
pp: case smul_left
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B (t • u)) v ∈ P'

Tactic:
simpa using Submodule.smul_mem _ _ huv

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

Goal state before:
pp: case smul_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B u) (t • v) ∈ P'

Tactic:
simpa using Submodule.smul_mem _ _ huv

Goal state after:
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ (f ∘ ⇑g) a ≠ 0 → a ∈ g.support

Tactic:
rw [mem_support_iff, not_imp_not]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N
hf : f 0 = 0
g : α →₀ M
a : α
⊢ g a = 0 → (f ∘ ⇑g) a = 0
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ Codisjoint s (K ∙ x)

Tactic:
simpa only [codisjoint_iff, sup_comm, not_lt_top_iff] using hs.2 (covBy_span_singleton_sup hx).1

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
rw [mul_sum]
    refine sum_congr rfl fun i hi => ?_
    rw [filter_insert, if_neg (ha i hi).not_gt, filter_insert, if_pos (ha i hi), prod_insert,
      mul_left_comm]
    exact mt (fun ha => (mem_filter.1 ha).1) ha'

Goal state after:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint {i} {j} ↔ i ≠ j

Tactic:
disjoint_singleton

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ i ≠ j ↔ i ≠ j
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ a b, f = single a b

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = (∏ x ∈ f1.support, g x (f1 x + f2 x)) * f2.prod g

Tactic:
← this hd.symm,

Goal state after:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = (∏ x ∈ f1.support, g x (f1 x + f2 x)) * ∏ x ∈ f2.support, g x (f2 x + f1 x)
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s fun x x_1 ↦ f x).prod h = ∏ x ∈ s, h x (f x)

Tactic:
simp +contextual [h_zero]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f.support = g.support

Tactic:
← image_fst_graph,

Goal state after:
α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ image Prod.fst f.graph = g.support
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
b : β
⊢ ¬(mapDomain (⇑f) x) b = 0 ↔ ∃ a, ¬x a = 0 ∧ f a = b

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
b : β
h : ¬(mapDomain (⇑f) x) b = 0
⊢ ∃ a, ¬x a = 0 ∧ f a = b

case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
b : β
⊢ (∃ a, ¬x a = 0 ∧ f a = b) → ¬(mapDomain (⇑f) x) b = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ (¬∀ i ∈ s, f i = 1) ↔ ∃ x ∈ s, 1 < f x

Tactic:
not_forall

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
hsum : 1 ≤ ∏ x ∈ s, f x
⊢ (∃ x, ¬(x ∈ s → f x = 1)) ↔ ∃ x ∈ s, 1 < f x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 0 ≤ ∏ i ∈ s \ {i}, f i

Tactic:
· apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case hf
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_1

Tactic:
· intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g

Tactic:
cases f; cases g; congr

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

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

Tactic:
rw [← preimage_val_Ici_val, image_preimage_eq_inter_range, range_val, Ici_inter_Iio]

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

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

Tactic:
← preimage_val_Ioi_val,

Goal state after:
n : ℕ
i : Fin n
⊢ val '' val ⁻¹' Ioi ↑i = Ioo (↑i) n
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)
⊢ (linearCombination R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
rw [linearCombination_apply]; rfl

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

Goal state before:
pp: 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'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (map (lmapDomain R R f) ⊤) = span R (range f)

Tactic:
←
    Finsupp.supported_univ,

Goal state after:
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'
S : Type u_13
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)) = span R (range f)
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 : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i, (⇑l ∘ Subtype.val) i • v ↑i = x

Tactic:
rw [← hx]

Goal state after:
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 : Set α
h : x ∈ span R (v '' s)
l : α →₀ R
hl : l ∈ Finsupp.supported R R s
hx : (Finsupp.linearCombination R v) l = x
⊢ ∑ i, (⇑l ∘ Subtype.val) i • v ↑i = (Finsupp.linearCombination R v) l
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
α : 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 : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Tactic:
rw [← hx]

Goal state after:
case refine_2
α : 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 : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ ∑ i, c i • v ↑i ∈ span R (v '' 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
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ n f g, ∑ i, f i • ↑(g i) = m

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

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

case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ (∃ n f g, ∑ i, f i • ↑(g i) = m) → m ∈ span R s
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

Tactic:
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]
    exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

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

Goal state before:
pp: case refine_1.inr
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
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
j k : ι
hk : i ≠ k
⊢ ((((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k

Tactic:
simp [hk]

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

Goal state before:
pp: case refine_2.inr
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
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
j k : ι
hk : i ≠ k
⊢ ((((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
            linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
          lsingle j)
        1)
      k =
    ((LinearMap.id ∘ₗ lsingle j) 1) k

Tactic:
simp [hk]

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

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

Tactic:
by
  ext i
  simp_rw [vecAlt0]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      vecAlt0]

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

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
h' : ⟨i + 2, h⟩ = ⟨i, ⋯⟩.succ.succ
⊢ (vecCons a (vecCons b x) ∘ ⇑(Equiv.swap 0 1)) ⟨i + 2, h⟩ = vecCons b (vecCons a x) ⟨i + 2, h⟩

Tactic:
simp only [Nat.succ_eq_add_one, h', Function.comp_apply,
      Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero _) (Fin.succ_succ_ne_one _), cons_val_succ]

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
classical
  by_cases hr : r = 0
  · simp_all
  by_cases h : f.support.Finite
  · exact mul_finsum' f r h
  simp [finsum_def, HasFiniteSupport, h, (by aesop : (r * f ·).support = f.support)]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
⊢ ∀ (a b : Fin n), a + b = b + a

Tactic:
by simp [add_def, Nat.add_comm]

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

Goal state before:
pp: case pos
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
exact map_finprod (Nat.castRingHom R) hf

Goal state after:
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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ False

Tactic:
have := @hv (Finsupp.single i 1 : ι →₀ R) 0 (by simpa using h)

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
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
this : Finsupp.single i 1 = 0
⊢ False
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
⊢ (¬∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
simp only [exists_prop, not_forall]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ ∏ i ∈ uIcc (castAdd m a) (castAdd m b), f i = ∏ i ∈ uIcc a b, f (castAdd m i)

Tactic:
by
  simp [← map_castAddEmb_uIcc]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a : Fin n
⊢ ∏ i ≤ castAdd m a, f i = ∏ i ≤ a, f (castAdd m i)

Tactic:
simp [← map_castAddEmb_Iic]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) % (a ^ b - 1) * ((a ^ b - 1) % (a ^ b - 1)) % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) %
      (a ^ b - 1) =
    a ^ ((c - b) % b) - 1

Tactic:
mod_self,

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b) % (a ^ b - 1) * 0 % (a ^ b - 1) + (a ^ (c - b) - 1) % (a ^ b - 1)) % (a ^ b - 1) = a ^ ((c - b) % b) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr
a b c : ℕ
hb : c % b < b
⊢ a ^ (c % b).gcd b - 1 = a ^ b.gcd c - 1

Tactic:
← gcd_rec

Goal state after:
case inr
a b c : ℕ
hb : c % b < b
⊢ a ^ b.gcd c - 1 = a ^ b.gcd c - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.gcd (m * k + n) = 1 ↔ m.gcd n = 1

Tactic:
gcd_mul_left_add_right

Goal state after:
m n k : ℕ
⊢ m.gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ span R (range v)

Tactic:
← Finsupp.range_linearCombination

Goal state after:
case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R), (Finsupp.linearCombination R v) c ∈ (Finsupp.linearCombination R v).range
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ k.castSucc

pp: case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc

Tactic:
· exact le_iff_val_le_val.2 (le_of_lt h)

Goal state after:
case inr.inr.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j.succ ≤ k.castSucc.castSucc
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
i : ι
inst✝ : Nontrivial R
hv : LinearIndepOn R v s
hi : i ∈ s
hi' : v i ∈ span R (v '' (s \ {i}))
⊢ 1 • v i ∈ span R (v '' (s \ {i}))

Tactic:
by simpa [Set.compl_eq_univ_sdiff] using hi'

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : n ≤ b
⊢ a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
by
  rw [← modEq_add_modulus_iff, Nat.sub_add_cancel h]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]

Tactic:
rw [hn, gcd_zero_left] at h

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ¬(n = 0 ∧ m = 0)

Tactic:
not_and

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ n = 0 → ¬m = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ n ∣ n.lcm m

Tactic:
exact dvd_lcm_left n m

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

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩

Goal state after:
case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∑ i ∈ tᶜ, f i • v i = ∑ i ∈ tᶜᶜ, f i • v i
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M = ↑n
⊢ finrank R M = n

Tactic:
by
  simp [finrank, h]

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a

Tactic:
rw [gcd]
  exact if_pos rfl

Goal state after: