mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x) 1) a✝ = ((id ∘ₗ lsingle x) 1) a✝

Tactic:
dsimp [splittingOfFinsuppSurjective]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (f ((single x 1).sum fun x r ↦ r • ⋯.choose)) a✝ = (single x 1) a✝
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
by
  rw [finprod_mem_def, mulIndicator_mulSupport]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
classical
  rw [finprod_def]
  simp only [HasFiniteMulSupport]
  rw [dif_neg hf]

Goal state after:
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)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]

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
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
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)
s : Finset α := (mulSupport f ∪ mulSupport g).toFinset
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]

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
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : ↥(Finset.image (⇑b) Finset.univ)
⊢ b.reindexFinsetRange x = ↑x

Tactic:
rcases x with ⟨bi, hbi⟩

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 : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
bi : M
hbi : bi ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨bi, hbi⟩ = ↑⟨bi, hbi⟩
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
⊢ (Fintype.linearCombination R v).range = span R (Set.range v)

Tactic:
by
  rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
      LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]

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

Tactic:
rw [← Set.image_id s]

Goal state after:
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 (_root_.id '' s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a

Tactic:
rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]

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

Goal state before:
pp: case refine_1
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 : ι
⊢ ((((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:
obtain rfl | hk := eq_or_ne i k

Goal state after:
case refine_1.inl
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 : ι
⊢ ((((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)
      i =
    ((LinearMap.id ∘ₗ lsingle j) 1) i

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
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
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 : ι
⊢ ((((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:
obtain rfl | hk := eq_or_ne i k

Goal state after:
case refine_2.inl
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 : ι
⊢ ((((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)
      i =
    ((LinearMap.id ∘ₗ lsingle j) 1) i

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
rw [finprod_mem_insert, finprod_mem_singleton]
  exacts [h, finite_singleton b]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a < a - b ↔ a < b

Tactic:
fin_omega

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)

Tactic:
have (a : _) :
      ∏ i ∈ (s.filter fun ab => Prod.fst ab = a).image Prod.snd, f (a, i) =
        (s.filter (Prod.fst · = a)).prod f := by
    refine Finset.prod_nbij' (fun b ↦ (a, b)) Prod.snd ?_ ?_ ?_ ?_ ?_ <;> aesop

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
Module: Mathlib.Logic.Equiv.Fin.Rotate

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

Tactic:
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']

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

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

Tactic:
have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm

Goal state after:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)
Module: Mathlib.Logic.Equiv.Fin.Rotate

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

Tactic:
Fin.val_succ,

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((⇑(finRotate (n + 1)))^[↑k + 1] i)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ 0 ^ y = 0

Tactic:
induction y with

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

Goal state before:
pp: y : ℕ∞
⊢ 1 ^ y = 1

Tactic:
induction y with

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

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ ⊤ ^ y = ⊤

Tactic:
induction y with

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

Goal state before:
pp: case mp
ι : 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 : ↑↑s → R), ∑ i, f i • v ↑i = ∑ i, g i • v ↑i → ∀ (i : ↑↑s), f i = g i) →
    ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Icc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Icc a b, f (Fin.cast h i)

Tactic:
by
  simp [← map_finCongr_Icc]

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 ∈ Ioo (castAdd m a) (castAdd m b), f i = ∏ i ∈ Ioo a b, f (castAdd m i)

Tactic:
simp [← map_castAddEmb_Ioo]

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:
by
  simp [← map_castAddEmb_Iio]

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

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

Tactic:
castSucc_lt_iff_succ_le,

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

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

Tactic:
castSucc_lt_iff_succ_le,

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a / m ^ 0 % m * m ^ 0 + ∑ i, ↑a / m ^ ↑i.succ % m * m ^ ↑i.succ = ↑a

Tactic:
Fin.val_succ,

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a / m ^ 0 % m * m ^ 0 + ∑ x, ↑a / m ^ (↑x + 1) % m * m ^ (↑x + 1) = ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]

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

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
simp [linearIndependent_empty_type]

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✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, 0 < f i

Tactic:
simp only [linearIndependent_iffₒₛ, not_forall, pos_iff_ne_zero]
  refine ⟨fun ⟨t, f, heq, i, hfi⟩ => ?_, fun ⟨t, f, heq, i, hi, hfi⟩ =>
    ⟨t, f, heq, i, hfi⟩⟩
  by_cases hi' : i ∈ t
  · exact ⟨t, f, heq, i, hi', hfi⟩
  · refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩
    simp [heq]

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

Goal state before:
pp: case refine_1
ι : 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 ι
s : Finset ι
h : ∀ (t : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ (∑ a, if ↑a ∈ t then f ↑a • v ↑a else 0) = ∑ a, if ↑a ∉ t then f ↑a • v ↑a else 0

Tactic:
rw [Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,
      Finset.sum_coe_sort s fun i => if i ∉ t then f i • v i else 0]

Goal state after:
case refine_1
ι : 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 ι
s : Finset ι
h : ∀ (t : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ (∑ i ∈ s, if i ∈ t then f i • v i else 0) = ∑ i ∈ s, if i ∉ t then f i • v i else 0
Module: Mathlib.Algebra.EuclideanDomain.Defs

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
conv =>
    lhs
    rw [xgcdAux]
  exact if_neg h

Goal state after:
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₁
⊢ Module.rank R ↥f.range ≤ Module.rank R M

Tactic:
simpa using lift_rank_range_le f

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).encard = s.encard

Tactic:
insert_eq_of_mem h

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.encard = s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ≠ b

Tactic:
rintro rfl; exact ha hb

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
exact WithTop.le_of_add_le_add_right hs hkt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ ENat.card α ≤ (f '' univ).encard

Tactic:
hf.encard_image,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ ENat.card α ≤ univ.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
by
  rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case neg
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : ¬j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j

Tactic:
· simp [heq]

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

Goal state before:
pp: α : Type u_3
⊢ ∅.ncard = 0

Tactic:
rw [ncard_eq_zero]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).ncard = s.ncard

Tactic:
insert_eq_of_mem h

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.ncard = s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ op g • ↑s

Tactic:
← h

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a₁ : α
⊢ ∀ (a₂ : α) (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂

Tactic:
a₂

Goal state after:
case convert_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a₁ a₂ : α
⊢ ∀ (ha₁ : a₁ ∈ s.toFinset) (ha₂ : a₂ ∈ s.toFinset), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ univ.ncard ≤ s.ncard + t.ncard

Tactic:
← h

Goal state after:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: case h
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
h : G
hh : h ∈ ↑H
n : G
hy : (fun x1 x2 ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
⊢ (leftRel (N.subgroupOf (H ⊔ N))) ((inclusion ⋯) ⟨h, hh⟩) ⟨(fun x1 x2 ↦ x1 * x2) h n, hy⟩

Tactic:
simp [leftRel_apply, inclusion, mem_subgroupOf, hn]

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

Goal state before:
pp: case pos
α : Type u_3
s : Set α
hs : s.Finite
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard

Tactic:
simp [(ncard_union_eq_iff (.image _ hs) (.image _ hs)).2 disjoint_image_inl_image_inr,
      ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p p' p'' : Submodule R M
inst✝ : Subsingleton M
⊢ Subsingleton (M ⧸ p)

Tactic:
simpa using Subsingleton.elim ..

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)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
c : S
f : (i : ι) → φ i →ₗ[R] M
⊢ ∑ i, (c • f) i ∘ₗ proj i = (RingHom.id S) c • ∑ i, f i ∘ₗ proj i

Tactic:
by simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
· rw [update_of_ne h, update_of_ne h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
β : Type v
F : Type w
R : Type ?u.7
M : Type ?u.9
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m m' : M
x✝¹ x✝ : R
h : x✝ ∈ {r | r • m = r • m'}
⊢ x✝¹ • x✝ ∈ {r | r • m = r • m'}

Tactic:
simpa [mul_smul] using congr(_ • $h)

Goal state after: