mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • 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 α
h : ∀ x ∈ s, f x = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = 1

Tactic:
by simp +contextual [h]

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) = ⊤ ↔ Function.Surjective ⇑(Fintype.linearCombination R v)

Tactic:
by
  rw [← LinearMap.range_eq_top, Fintype.range_linearCombination]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
n : ℕ
f : Fin n → R × M
hf : ∀ (i : Fin n), (f i).2 ∈ s
⊢ ∃ f_1 g, ∑ i, f_1 i • ↑(g i) = ∑ i, (f i).1 • (f i).2

Tactic:
exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩

Goal state after:
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
k : Fin n
hk : ¬p k
⊢ {i | p i} ⊆ Iio k

Tactic:
by grind

Goal state after:
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
⊢ ↑j < #{i | p i} → p j

Tactic:
by grind

Goal state after:
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 q univ ⊆ filter p univ

Tactic:
by grind

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

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

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

Tactic:
· simp

Goal state after:
case pos.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h : ↑⟨i + 1, hi⟩ < m + 1
⊢ vecCons x u ⟨↑⟨i + 1, hi⟩, h⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
by rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]

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

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

Tactic:
| succ n =>

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

Goal state before:
pp: case e'_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x✝ : Option α
⊢ f x✝ = ∏ᶠ (_ : x✝ ∈ insert none (range some)), f x✝

pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
· simp

Goal state after:
case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) i.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) i.succ

pp: case inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)

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

Goal state before:
pp: case inr.inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : j.succ ≠ 0
hki : j.succ ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) j.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) j.succ

pp: case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
· simp

Goal state after:
case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ i

Tactic:
by grind

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ ⟨↑k - 1, ⋯⟩ ≠ j

Tactic:
by grind

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

Goal state before:
pp: case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

pp: case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1

Tactic:
· simp

Goal state after:
case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case inl
n✝ n : ℕ
⊢ (finRotate (n + 2)) (Fin.last (n + 1)) = Fin.last (n + 1) + 1

pp: case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1

Tactic:
· simp [finRotate_last]

Goal state after:
case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport fun i ↦ ↑(f i)
⊢ ↑1 = ∏ᶠ (x : ι), ↑(f x)

Tactic:
finprod_of_not_hasFiniteMulSupport H,

Goal state after:
case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
H : ¬HasFiniteMulSupport fun i ↦ ↑(f i)
⊢ ↑1 = 1
Module: Mathlib.Data.ENat.Pow

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

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

Tactic:
· simp

Goal state after:
case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inl
b c : ℕ
ha0 : succ 0 > 0
⊢ (succ 0 ^ c - 1) % (succ 0 ^ b - 1) = succ 0 ^ (c % b) - 1

pp: case inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
· simp

Goal state after:
case inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inl
a c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
⊢ (a ^ c - 1) % (a ^ 0 - 1) = a ^ (c % 0) - 1

pp: case inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
· simp

Goal state after:
case inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * (partialProd f i.castSucc * f i) = f i

Tactic:
inv_mul_cancel_left

Goal state after:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ f i = f i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_1
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i : Fin (n + 1)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) 0 = (partialProd g ∘ a.succ.succAbove) 0

pp: case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc →
      partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ

Tactic:
· simp

Goal state after:
case refine_2
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc →
      partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inl
a c : ℕ
⊢ (a ^ 0 - 1).gcd (a ^ c - 1) = a ^ gcd 0 c - 1

pp: case inr
a b c : ℕ
hb : b > 0
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
· simp

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

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

Tactic:
by
  rw [Coprime, Coprime, gcd_mul_left_add_left]

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

Goal state before:
pp: m n : ℕ
cop : m.Coprime n
x : ℕ
ha : 1 ≤ x ∧ n ≠ 0
y : ℕ
hb : 1 ≤ y ∧ m ≠ 0
h : n * x * m + m * y * n = m * n
⊢ (x + y) * (m * n) = m * n

Tactic:
rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]

Goal state after:
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 + 1 ≤ ↑k.castSucc.castSucc

Tactic:
exact Nat.succ_le_of_lt h

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i

Tactic:
finFunctionFinEquiv_apply,

Goal state after:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∑ i_1, ↑(Pi.single i j i_1) * m ^ ↑i_1 = ↑j * m ^ ↑i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_2.a
ι : 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
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ {i ∈ s | g i ≤ f i}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i

Tactic:
simp only [Finset.mem_filter] at hi

Goal state after:
case e'_2.a
ι : 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
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s ∧ g i ≤ f i
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_3.a
ι : 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
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ {x ∈ s | f x < g x}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i

Tactic:
simp only [Finset.mem_filter] at hi

Goal state after:
case e'_3.a
ι : 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
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s ∧ f i < g i
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ ↑(-↑x.natAbs) = (x % ↑n).toNat

Tactic:
simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]

Goal state after:
case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ (if n ∣ x.natAbs then 0 else n - x.natAbs % n) = (x % ↑n).toNat
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case succ
n : ℕ
inst✝ : Fintype (ZMod (n + 1))
⊢ Fintype.card (ZMod (n + 1)) = n + 1

Tactic:
| succ n =>

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

Goal state before:
pp: case neg
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]

Goal state after:
case neg
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ card α = 0 ↔ IsEmpty α

Tactic:
by
  rw [← Cardinal.mk_eq_zero_iff]
  simp [card]

Goal state after:
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
inst✝ : Subsingleton R
⊢ finrank R M = 1

Tactic:
rw [finrank, rank_subsingleton, map_one]

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
← rank_range_of_surjective f h

Goal state after:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R M₁ ≤ Module.rank R M

Tactic:
← rank_range_of_surjective f h

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥f.range ≤ Module.rank R M
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
h' : IsEmpty α
⊢ InjOn f s

pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
t : Set β
hs : ∅.Finite
hle : ∅.encard ≤ t.encard
⊢ ∃ f, ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅

pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
h : s.encard = ⊤
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
· simp

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
h : s.encard = ⊤
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
by
  cases finite_or_infinite α
  · let := Fintype.ofFinite α
    simp only [this, *, Nat.card_eq_fintype_card, dif_pos]
  · simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
have := Fintype.ofFinite α
  simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ ↑(Nat.card ↑(s ∪ t)) ≤ ↑(Nat.card ↑s + Nat.card ↑t)

Tactic:
Nat.cast_add,

Goal state after:
case inl.intro
α : Type u_1
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ ↑(Nat.card ↑(s ∪ t)) ≤ ↑(Nat.card ↑s) + ↑(Nat.card ↑t)
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
· simp

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).encard = ↑(s.ncard + 1)

Tactic:
Nat.cast_add,

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).encard = ↑s.ncard + ↑1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (insert a s).ncard ↔ Even s.ncard

Tactic:
ncard_insert_of_notMem ha hs,

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (s.ncard + 1) ↔ Even s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Even (insert a s).ncard ↔ Odd s.ncard

Tactic:
ncard_insert_of_notMem ha hs,

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Even (s.ncard + 1) ↔ Odd s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ s

Tactic:
by
  rw [← SetLike.mem_coe, ← ha]; exact mem_own_rightCoset s a

Goal state after:
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
  refine Basis.ext (b.restrictScalars R) fun _ => ?_
  simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one,
    Basis.repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, LinearMap.domRestrict_apply,
    Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (↑b)⁻¹ * ((f a.1)⁻¹ * (f a.1 * ↑c)) ∈ s

Tactic:
inv_mul_cancel_left

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (↑b)⁻¹ * ↑c ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (Quotient.mk'' a, Quotient.mk'' ⟨(f (Quotient.mk'' a))⁻¹ * (f (Quotient.mk'' a) * ↑b), ⋯⟩) =
    (Quotient.mk'' a, Quotient.mk'' b)

Tactic:
inv_mul_cancel_left

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)

Tactic:
simp_rw [leftRel_eq]
      exact id

Goal state after: