mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ ((s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map ((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal

Tactic:
congr!

Goal state after:
case cons.e'_5.a.e'_4
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map id (cons a) x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).2 = (Prod.map id (cons a) a✝²).2 + x✝.2

case cons.e'_6.a.e'_3
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
a✝² : Multiset α × Multiset α
a✝¹ : a✝² ∈ s.antidiagonal
x✝ : Multiset α × Multiset α
a✝ : x✝ ∈ t.antidiagonal
⊢ (((fun x ↦ Prod.map (cons a) id x) ∘ fun q ↦ (a✝².1 + q.1, a✝².2 + q.2)) x✝).1 = (Prod.map (cons a) id a✝²).1 + x✝.1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton = {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton

Tactic:
congr!

Goal state after:
case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
x✝ : α
⊢ Membership.mem ⟦l₁⟧ = Membership.mem ⟦l₂⟧
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f ↦ indicator s f) a = (fun f ↦ indicator s f) b
⊢ a = b

Tactic:
ext i hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f ↦ indicator s f) a = (fun f ↦ indicator s f) b
i : ι
hi : i ∈ s
⊢ a i hi = b i hi
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ f a ≠ 0

Tactic:
rw [← mem_support_iff, hs]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ a ∈ insert a s
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hs_nonempty : ⟦l⟧ ≠ ∅
hs : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul
      (by simpa using hs_nonempty) (by simpa)]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
s : Multiset ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
  apply List.prod_map_le_prod_map₀ f g h0 h

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0

Tactic:
congr!

Goal state after:
case h₂
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝¹ : α
a✝ : a = a✝¹
⊢ a✝¹ = a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α × β →₀ M
⊢ { support := image Prod.fst f.support,
        toFun := fun a ↦
          { support := filterMap (fun x ↦ if x.1 = a then some x.2 else none) f.support ⋯, toFun := fun b ↦ f (a, b),
            mem_support_toFun := ⋯ },
        mem_support_toFun := ⋯ }.support =
    image Prod.fst f.support

Tactic:
congr!

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

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
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ restrictDom M R s ∘ₗ (supported M R s).subtype = LinearMap.id

Tactic:
ext l a

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a
Module: Mathlib.LinearAlgebra.Finsupp.Supported

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
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i)) = ⊤

Tactic:
eq_top_iff

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun x ↦ x ∈ ⋃ i, s i
⊢ ⊤ ≤ comap ((supported M R (⋃ i, s i)).subtype ∘ₗ restrictDom M R (⋃ i, s i)) (⨆ i, supported M R (s i))
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ ∃ y, (linearCombination R v) y = x

Tactic:
use single i 1

Goal state after:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x✝ x : M
i : α
hi : v i = x
⊢ (linearCombination R v) (single i 1) = x
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ (linearCombinationOn α M R v s).range = ⊤

Tactic:
by
  rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict,
    ← LinearMap.range_le_iff_comap, range_subtype, Submodule.map_top, LinearMap.range_comp,
    range_subtype]
  exact (span_image_eq_map_linearCombination _ _).le

Goal state after:
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
⊢ ∑ i, c i • v ↑i ∈ span R (v '' s)

Tactic:
exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

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

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Tactic:
exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
rw [finprod_eq_prod _ hf]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝ : Fin n
a : ℕ
ha : a < n
⊢ (n - ↑⟨a, ha⟩ + a) % n = ↑0

Tactic:
by
      rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
      exact le_of_lt ha

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

Goal state before:
pp: case coe.top
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Goal state after:
case coe.top.inl
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_0 : x < 1
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤

case coe.top.inr.inl
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
h : 1 ≠ 0
⊢ (fun y ↦ 1 ^ y) ↑a✝ ≤ (fun y ↦ 1 ^ y) ⊤

case coe.top.inr.inr
x : ℕ∞
h : x ≠ 0
a✝ : ℕ
y_z : ↑a✝ ≤ ⊤
x_2 : 1 < x
⊢ (fun y ↦ x ^ y) ↑a✝ ≤ (fun y ↦ x ^ y) ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Goal state after:
case top.inl
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ x ^ ⊤ ≤ z ^ ⊤

case top.inr.inl
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ^ ⊤ ≤ z ^ ⊤

case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤
Module: Mathlib.Data.ENat.Pow

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

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

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

case inr.inl
y : ℕ∞
y_0 : ¬y = 0
h : 1 ^ y = 1
⊢ 1 = 1

case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Goal state after:
case inl
x y z : ℕ∞
x_0 : x < 1
⊢ x ^ (y + z) = x ^ y * x ^ z

case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

case inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x y z : ℕ∞
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Goal state after:
case top.inl
x y z : ℕ∞
x_0 : x < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

case top.inr.inl
y z : ℕ∞
⊢ (1 * y) ^ ⊤ = 1 ^ ⊤ * y ^ ⊤

case top.inr.inr
x y z : ℕ∞
x_2 : 1 < x
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Goal state after:
case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ x ^ (y * z) = (x ^ y) ^ z

case inr.inr.inr.inl
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ 1 ^ (y * z) = (1 ^ y) ^ z

case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ (∃ m n, m • p + a = n • p + b) → ∃ m, m • p = b - a

Tactic:
rintro ⟨m, n, h⟩

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ∃ m, m • p = b - a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j with i ≤ j.castSucc, f i j) * ∏ i, ∏ j with j.castSucc < i, f i j =
    (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j

Tactic:
by
    rw [Fin.prod_univ_castSucc, Fin.prod_univ_succ]
    simp [Finset.filter_le_eq_Ici, Finset.filter_ge_eq_Iic]

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

Goal state before:
pp: case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ k % ↑n < ↑n

Tactic:
refine Int.emod_lt_of_pos _ ?_

Goal state after:
case mp.refine_1
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ 0 < ↑n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ a.gcd (b.gcd c) = a.gcd (c.gcd b)

Tactic:
gcd_comm b c

Goal state after:
a b c : ℕ
⊢ a.gcd (c.gcd b) = a.gcd (c.gcd b)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i✝ i : ι
hi : i ∉ s
⊢ w i • g₁ i = w i • g₂ i

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ ∑ i ∈ s, (w i • g₁ i) • v i = ∑ i ∈ s, (w i • g₂ i) • v i

Tactic:
· simp_rw [hgs i hi]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ ∑ i ∈ s, (w i • g₁ i) • v i = ∑ i ∈ s, (w i • g₂ i) • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i✝ i : ι
hi : i ∉ s
⊢ g₁ i • ↑(w i) = g₂ i • ↑(w i)

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ ∑ i ∈ s, (g₁ i • ↑(w i)) • v i = ∑ i ∈ s, (g₂ i • ↑(w i)) • v i

Tactic:
· simp_rw [hgs i hi]

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ ∑ i ∈ s, (g₁ i • ↑(w i)) • v i = ∑ i ∈ s, (g₂ i • ↑(w i)) • v i
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
Pi.single_eq_of_ne hx,

Goal state after:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑0 * m ^ ↑x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_2
ι : 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
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, f i • v i + ∑ i ∈ s with ¬g i ≤ f i, f i • v i

Tactic:
not_le

Goal state after:
case e'_2
ι : 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
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, f i • v i + ∑ i ∈ s with f i < g i, f i • v i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c

Tactic:
Nat.mod_eq_of_lt (lt_of_not_ge h),

Goal state after:
case neg
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
⊢ a % c + b % c + 0 = a % c + b % c
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_3
ι : 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 ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x) =
    ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with ¬g i ≤ f i, g i • v i

Tactic:
not_le

Goal state after:
case e'_3
ι : 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 ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x) =
    ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, g i • v i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑(Pi.single i j x) * ∏ j, n (Fin.castLE ⋯ j) = 0

Tactic:
Pi.single_eq_of_ne hx,

Goal state after:
m : ℕ
n : Fin m → ℕ
inst✝ : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
⊢ ↑0 * ∏ j, n (Fin.castLE ⋯ j) = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i✝ : ι ⊕ ι'
hi : i✝ ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
i : ι'
x✝ : i ∈ s.preimage Sum.inr ⋯
⊢ (fun x ↦ g x • v x) (Sum.inr i) ∈ span R (v '' range Sum.inr)

Tactic:
exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)

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

Goal state before:
pp: a b n : ℕ
h : b ≤ a % n
⊢ a % n - b = (a - b) % n

Tactic:
by
  rcases n.eq_zero_or_pos with rfl | hn; · simp only [mod_zero]
  nth_rw 2 [← div_add_mod a n]; rw [Nat.add_sub_assoc h, mul_add_mod]
  exact (mod_eq_of_lt <| (sub_le ..).trans_lt (mod_lt a hn)).symm

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ ∀ x ∈ univ, [][x] ^ (-1) ^ ↑x = 1

Tactic:
rintro ⟨i, ⟨⟩⟩

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (Fin n) = n

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
n : ℕ
⊢ Fintype.card (Fin n) = n
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype ↑s
⊢ Fintype.card ↑(f '' s) = Fintype.card ↑s
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(range f) = Nat.card α

Tactic:
rw [← Nat.card_preimage_of_injective hf le_rfl]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(f ⁻¹' range f) = Nat.card α
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Fintype.card (Sigma β) = ∑ x, Fintype.card (β x)
Module: Mathlib.SetTheory.Cardinal.Finite

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

Tactic:
Nat.card_eq_fintype_card,

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