mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
⊢ {i}.mulIndicator f = Pi.mulSingle i (f i)

Tactic:
by
  ext j
  simp only [Set.mulIndicator_apply, Pi.mulSingle_apply, Set.mem_singleton_iff]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ single a b = single a' b' ↔ b = b'

Tactic:
Finsupp.unique_ext_iff,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Unique α
b' : M
⊢ (single a b) default = (single a' b') default ↔ b = b'
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x ≤ ⨆ i, (s i).mulIndicator f x

Tactic:
rcases hx with ⟨i, hi⟩

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Tactic:
by
  refine ((sum_sum_index ?_ ?_).trans ?_).symm
  · intro
    exact single_zero _
  · intro
    exact single_add _
  refine sum_congr fun _ _ => sum_single_index ?_
  exact single_zero _

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

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ g i (f i) + (single i a).sum g = (single i (f i)).sum g + g i a

Tactic:
sum_single_index (hg _),

Goal state after:
case e_a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ g i (f i) + g i a = (single i (f i)).sum g + g i a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α →₀ β →₀ M
⊢ (↑f.support).PairwiseDisjoint fun a ↦ map (Embedding.sectR a β) (f a).support

Tactic:
intro a₁

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝ : Zero M
f : α →₀ β →₀ M
a₁ : α
⊢ a₁ ∈ ↑f.support →
    ∀ ⦃y : α⦄, y ∈ ↑f.support → a₁ ≠ y → (Disjoint on fun a ↦ map (Embedding.sectR a β) (f a).support) a₁ y
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

Tactic:
by_cases hd'S : d' ∈ S

Goal state after:
case pos
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∈ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x

case neg
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S', f x < ∏ x ∈ S, f x
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
hs : s.Nonempty
Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
by
  contrapose! Hle with Hlt
  exact prod_lt_prod_of_nonempty' hs Hlt

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
refine t.induction_on zero.le fun i t it h ↦ ?_
  simpa only [sup_insert, Finset.sum_insert it] using ih.trans (by gcongr)

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ⊔ i.sup f ↔ ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)

Tactic:
Finset.mem_cons,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ⊔ i.sup f ↔
    ∀ (x : β), x = z ∨ x ∈ i → ∀ (y : β), y = z ∨ y ∈ i → x ≠ y → Disjoint (f x) (f y)
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
rw [← l.sum_single]
    refine sum_mem fun i il => ?_
    rw [show single i (l i) = l i • single i 1 by simp]
    exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

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

Goal state before:
pp: case pos
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (x : M), f x = 1 → x = 1
g : α → M
hg : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)

Tactic:
exact f.map_finprod_plift g hg

Goal state after:
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
hx : x ∈ Set.range v
⊢ x ∈ ↑(linearCombination R v).range

Tactic:
rcases hx with ⟨i, hi⟩

Goal state after:
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
⊢ x ∈ ↑(linearCombination R v).range
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
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

Tactic:
exact Finset.prod_le_prod' fun i _ ↦ h i

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
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
f g : α → R
⊢ ∑ i, (f + g) i • v i = ∑ i, f i • v i + ∑ i, g i • v i

Tactic:
by simp_rw [← Finset.sum_add_distrib, ← add_smul]; rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ x ∈ Finset.image g hs.toFinset, f x

Tactic:
refine finprod_mem_eq_prod_of_inter_mulSupport_eq f ?_

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image g hs.toFinset) ∩ mulSupport f
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inl
n i : ℕ
hi : i < n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
finSumNatEquiv_symm_apply_of_lt hi,

Goal state after:
case inl
n i : ℕ
hi : i < n
⊢ (Sum.inl ⟨i, hi⟩).isLeft = decide (i < n)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : ∏ y ∈ s with f y = x, g y ≠ 1
a : β
h : a ∈ {y ∈ s | f y = x}
⊢ x ∈ ↑(Finset.image f s)

Tactic:
simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
x : α
hx : ∏ y ∈ s with f y = x, g y ≠ 1
a : β
h : a ∈ s ∧ f a = x
⊢ ∃ x_1 ∈ s, f x_1 = x
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑((finRotate (n + 1)) i) = ↑i + 1

Tactic:
rw [finRotate_apply]

Goal state after:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
simp_rw [finprod_mem_finset_product']

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι

Tactic:
calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp

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

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

pp: case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝

Tactic:
· rcases lt_trichotomy x 1 with x_0 | rfl | x_2
    · rw [Order.lt_one_iff.1 x_0, zero_epow_top]; exact bot_le
    · rw [one_epow]; exact one_le_epow (Order.one_le_iff_ne_zero.1 x_z)
    · rw [epow_top (x_2.trans_le x_z)]; exact le_top

Goal state after:
case coe
y x z : ℕ∞
x_z : x ≤ z
a✝ : ℕ
⊢ x ^ ↑a✝ ≤ z ^ ↑a✝
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
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : ¬f x✝ = g x✝
⊢ ∑ i ∈ f.support ∪ g.support, f i • v i = ∑ i ∈ f.support ∪ g.support, g i • v i

Tactic:
rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;>
            rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x, f (finSumFinEquiv.toFun x) = (∏ i, f (castAdd b i)) * ∏ i, f (natAdd a i)

pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
· apply Fintype.prod_sum_type

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y

pp: case refine_1
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ x) = (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ y)

Tactic:
· ext i
    exact hinj congr($this i)

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
⊢ (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ x) = (Finsupp.linearCombination K v) (Finsupp.mapRange f ⋯ y)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [MOD n]
⊢ ↑a ≡ ↑b [PMOD ↑n]

Tactic:
rw [← modEq_iff_natModEq] at h

Goal state after:
M : Type u_1
inst✝ : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [PMOD n]
⊢ ↑a ≡ ↑b [PMOD ↑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
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x

Tactic:
apply (LinearIndependent.linearCombinationEquiv hv).injective

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
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ hv.linearCombinationEquiv (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x)) =
    hv.linearCombinationEquiv (hv.repr x)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h₁ : a ≡ b [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ c ≡ d [MOD n]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_add] at *
  rw [add_sub_add_comm] at h₂
  convert! Int.dvd_sub h₂ h₁ using 1
  rw [add_sub_cancel_left]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x, g x.succ • v x = 0
⊢ ∑ i, g i.succ • v i ∈ span R (range v)

Tactic:
exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0

Tactic:
rw [this, zero_smul, zero_add] at total_eq

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : ∑ x, g x.succ • v x = 0
this : g 0 = 0
⊢ g j = 0
Module: Mathlib.Data.ZMod.Defs

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

Tactic:
← Int.natCast_dvd

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

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

Tactic:
rw [← Int.natCast_dvd] at h
      rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ ¬↑n ∣ x

Tactic:
← Int.natCast_dvd

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬↑n ∣ x
⊢ ¬↑n ∣ x
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
rw [Bijective, and_congr_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)
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 ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
| Finset.map (Embedding.subtype (Membership.mem s)) Finset.univ

Tactic:
change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _

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
inst✝ : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
| Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) Finset.univ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
⊢ ∅.encard = 0

Tactic:
encard_eq_zero

Goal state after:
α : Type u_1
⊢ ∅ = ∅
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
h₁ : f ![0, 1] = 0
h₂ : 0 = f ![1, 0]
⊢ 0 = 1

Tactic:
by simpa using congr($(inj (h₁.trans h₂)) 1)

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Finite
⊢ s.encard < ⊤

Tactic:
induction s, h using Set.Finite.induction_on with

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'
⊢ lift.{v, v'} (Module.rank R ↥f.range) ≤ lift.{v', v} (Module.rank R M)

Tactic:
by
  simp only [Module.rank_def]
  rw [Cardinal.lift_iSup Cardinal.bddAbove_of_small]
  apply ciSup_le'
  rintro ⟨s, li⟩
  apply le_trans
  swap
  · apply Cardinal.lift_le.mpr
    refine le_ciSup Cardinal.bddAbove_of_small ⟨rangeSplitting f '' s, ?_⟩
    apply LinearIndependent.of_comp f.rangeRestrict
    convert! li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1
  · exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

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
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

Tactic:
simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
  constructor
  · rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
  · rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.encard = 0 ↔ s = ∅

Tactic:
encard_eq_zero

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ Cardinal.mk ↑s
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
← cast_ncard hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
h : ↑(𝒫 s).ncard = 2 ^ ↑s.ncard
⊢ (𝒫 s).ncard = 2 ^ s.ncard
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:
intro 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.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = 0 i

pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i

Tactic:
· exact (h.le_bot ⟨hiI, hiJ⟩).elim

Goal state after:
case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∉ J
⊢ b i = 0 i