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

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
⊢ ∏ᶠ (a : α), s.mulIndicator f a = ∏ i ∈ t, f i
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
finprod_mem_def,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a = ∏ᶠ (i : α) (_ : i ∈ s), f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
finprod_mem_def,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a = ∏ᶠ (a : α), s.mulIndicator f a
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
by
  simp [uIcc, ← rev_anti.map_min, ← rev_anti.map_max]

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

Goal state before:
pp: case h
α : 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
x : α → R
⊢ ((linearEquivFunOnFinite R R α).symm x).support ⊆ Finset.univ

Tactic:
exact Finset.subset_univ _

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

Goal state before:
pp: case hf
α : 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
x✝ : α → R
x : α
a✝ : x ∈ Finset.univ
hx : x ∉ ((linearEquivFunOnFinite R R α).symm x✝).support
⊢ (fun i ↦ ⇑((fun i ↦ LinearMap.id.smulRight (v i)) i)) x 0 = 0

Tactic:
exact zero_smul _ _

Goal state after:
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
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i, c i • v i = x

Tactic:
by
  simp_rw [← mem_span_range_iff_exists_fun]
  exact ⟨fun h x => h trivial, fun h x _ => h x⟩

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

Tactic:
exact l.support.sum_coe_sort fun a ↦ l a • v a

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

Goal state before:
pp: case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ #{i | (x ::ᵥ xs).get i = a} = List.count a (x ::ᵥ xs).toList

Tactic:
simp_rw [card_filter_univ_succ', Vector.get_cons_zero, Vector.toList_cons, Vector.get_cons_succ,
      hxs, List.count_cons, add_comm (ite (x = a) 1 0), beq_iff_eq]

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

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

Tactic:
by
  ext
  simp [vecTail]

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

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

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:
· simp [Nat.mod_eq_of_lt, h]

Goal state after:
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)
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
hb : ↑b + 1 < n
⊢ Iio (b + 1) = Iic b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Icc (a + 1) b = Ioc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Ico (a + 1) b = Ioo a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ico a (b + 1) = Icc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

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

Tactic:
cases n with
  | zero =>
    obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
  | succ n =>
    split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · 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
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Tactic:
vecAlt0

Goal state after:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) i
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 : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)
  simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
  symm
  apply Finset.prod_subset <;> aesop

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (Equiv.symm (finRotate n)) i = i - 1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero i.pos.ne'

Goal state after:
n : ℕ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ)) i = i - 1
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)
⊢ (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v

Tactic:
simp only [← Set.range_comp]

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)
⊢ range (Subtype.val ∘ fun i ↦ ⟨v i, ⋯⟩) = range v
Module: Mathlib.LinearAlgebra.Basis.Basic

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

Tactic:
by simp [Basis.singleton, Unique.eq_default i]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

Tactic:
rw [Order.lt_one_iff.1 x_0, zero_epow y_0] at h

Goal state after:
case inl
x y : ℕ∞
h : 0 = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = x ^ ⊤ * x ^ z

pp: case inr.inr.coe
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + z) = x ^ ↑a✝ * x ^ z

Tactic:
· rw [top_add, epow_top x_2, top_mul]
      exact (epow_pos x_2.ne_zero).ne'

Goal state after:
case inr.inr.coe
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
⊢ x ^ (↑a✝ + z) = x ^ ↑a✝ * x ^ z
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
⊢ ¬LinearIndependent R v ↔ ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
rw [linearIndependent_iff'ₛ]

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
⊢ (¬∀ (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
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p

Tactic:
simp_rw [modEq_iff_zsmul', sub_eq_iff_eq_add']

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) ↔ ∃ i, i < n ∧ ∃ m, a - b - i • p = m • n • p

Tactic:
sub_eq_iff_eq_add (b := _ • _),

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
⊢ (∃ m, a - b = m • p) ↔ ∃ i, i < n ∧ ∃ m, a - b = m • n • p + i • p
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ a ≡ c + b * n [MOD n] ↔ a ≡ c [MOD n]

Tactic:
modEq_add_mul_modulus_iff

Goal state after:
n a b c : ℕ
⊢ a ≡ c [MOD n] ↔ a ≡ c [MOD n]
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✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
rw [linearIndependent_iff'ₛ]

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✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
⊢ (∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * (i x * i y) - ∑ i ∈ insert a s, a x * (g i * i y) =
    (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y

Tactic:
by simp [Finset.mul_sum]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h✝ : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #↑↑⟨s, hs⟩
t : Set M
hst : t ⊆ ↑⟨s, hs⟩
ht : #↑t = c'
⊢ ∃ s, lift.{w, v} #↑s = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
exact ⟨t, by simp [ht, hcc'], hs.mono hst⟩

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑n + 1 ≤ #↑↑s
⊢ ∃ s, s.card = n + 1 ∧ LinearIndepOn R id ↑s

Tactic:
← Nat.cast_add_one

Goal state after:
case succ
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
⊢ ∃ s, s.card = n + 1 ∧ LinearIndepOn R id ↑s
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case insert
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ ∀ i ∈ insert a s, g i = 0

Tactic:
have h4 : g a = 0 :=
    calc
      g a = g a * 1 := (mul_one _).symm
      _ = (g a • a : G → L) 1 := by rw [← a.map_one]; rfl
      _ = (∑ i ∈ insert a s, g i • i : G → L) 1 := by
        rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]
      _ = 0 := by rw [hg]; rfl

Goal state after:
case insert
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
h4 : g a = 0
⊢ ∀ i ∈ insert a s, g i = 0
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
  rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans_lt natCast_lt_aleph0
  · exact natCast_lt_aleph0

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ (insert a s).encard = s.encard + 1

Tactic:
rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
rw [linearIndependent_iff'ₛ]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → 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 : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k

Tactic:
have hk : k ≤ encard (t \ s) := by
    rw [← encard_sdiff_add_encard_of_subset hst, add_comm] at hkt
    exact WithTop.le_of_add_le_add_right hs hkt

Goal state after:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
hk : k ≤ (t \ s).encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
Module: Mathlib.LinearAlgebra.Basis.Submodule

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✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
⊢ (N' : Submodule R M) → N' ≤ ⊥ → (x : M) → x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'

Tactic:
intro N

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✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
⊢ N ≤ ⊥ → (x : M) → x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ Commute z y

Tactic:
rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
y : A
⊢ ∑ i ∈ (b.repr y).support, z * (b.repr y) i • b i = ∑ i ∈ (b.repr y).support, (b.repr y) i • b i * z
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

Tactic:
suffices
    Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
      ((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
    by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range ⇑b))
i : ι
⊢ mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr =
    (↑R ↑b.repr).domRestrict (span R (range ⇑b))
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Tactic:
simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) b b

Tactic:
exact ConGen.Rel.refl _

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : M₂ →ₗ[R] M₃
I : Type u_1
c : R
h : I → M₂
x : I
⊢ (⇑f ∘ (c • h)) x = ((RingHom.id R) c • ⇑f ∘ h) x

Tactic:
exact f.map_smul' c (h x)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
codisjoint_iff_le_sup

Goal state after:
case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ (inl R M M₂).range ⊔ (inr R M M₂).range
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
h : a < b
⊢ ↑(insert (succ a) (Ioc (succ a) b)) = ↑(Ioc a b)

Tactic:
simpa using Set.insert_Ioc_succ_left_eq_Ioc h

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]
  exact Set.image_add_const_Ico _ _ _

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i

Tactic:
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]
  exact fun x hx ↦ le_of_lt hx

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
⊢ ∀ x_1 ∈ Set.Ioi i, x ≤ x_1

Tactic:
intro y hy

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
⊢ x ≤ y
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (f i \ ∅.sup f)

Tactic:
simpa only [sup_empty, sdiff_bot] using hpi

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ (∏ x > a, f x) * f a = ∏ x ≥ a, f x

Tactic:
by
  rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]

Goal state after: