mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
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)
a : α
⊢ ∀ (s : Multiset α),
    ((∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod) →
      (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
s

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
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)
a : α
s : Multiset α
⊢ ((∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod) →
    (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
h : ∀ i ∈ s, 1 ≤ f i
⊢ 1 ≤ ∏ i ∈ s, 1

Tactic:
rw [prod_const_one]

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
h : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, 1 = 1

Tactic:
rw [prod_const_one]

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
a : ι
⊢ ∀ (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
        (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)

Tactic:
s

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
⊢ a ∉ s →
    ((∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)) →
      (∀ i ∈ insert a s, 1 ≤ f i) → (∏ i ∈ insert a s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
f : α →₀ M
⊢ ∀ (s : Multiset (α →₀ M)),
    (a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support) → a ∈ (f ::ₘ s).sum.support → ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support

Tactic:
s

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s✝ : Multiset (α →₀ M)
a : α
f : α →₀ M
s : Multiset (α →₀ M)
⊢ (a ∈ s.sum.support → ∃ f ∈ s, a ∈ f.support) → a ∈ (f ::ₘ s).sum.support → ∃ f_1 ∈ f ::ₘ s, a ∈ f_1.support
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
h : ∀ i ∈ s, 1 < f i
hs : s.Nonempty
⊢ 1 ≤ ∏ i ∈ s, 1

Tactic:
rw [prod_const_one]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
h : ∀ i ∈ s, f i < 1
hs : s.Nonempty
⊢ ∏ i ∈ s, 1 ≤ 1

Tactic:
rw [prod_const_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
i : α
h : (mapDomain f x) (f i) = 0 (f i)
⊢ x i = 0 i

Tactic:
simp [mapDomain_apply_eq_sum] at h

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
i : α
h : ∀ (i_1 : α), ¬x i_1 = 0 → f i_1 = f i → x i_1 = 0
⊢ x i = 0 i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ s ∩ mulSupport f

Tactic:
Set.ext_iff.mp h x,

Goal state after:
case refine_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
x : α
hxf : x ∈ mulSupport f
hx : x ∈ t
⊢ x ∈ ↑t ∩ mulSupport f
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ Ioi (natAdd m i) ⊆ range (natAdd m)

Tactic:
exact Ioi_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

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:
simp_rw [← Finset.sum_add_distrib, ← add_smul]

Goal state after:
α : 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 = ∑ x, (f x + g x) • v x
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
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, h⟩ = b i

Tactic:
by
  rw [reindexFinsetRange, reindex_apply, reindexRange_apply]
  rfl

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by_contra! h'

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
h' : ∀ x ∈ s, f x = 1
⊢ False
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
← finprod_mem_inter_mulSupport f t,

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
← finprod_mem_inter_mulSupport f t,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : 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 : f a = 1
⊢ ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
apply Finset.prod_erase _ ha

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 β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a) ⊆ ↑(image g s)

Tactic:
by
  simp only [Finset.coe_image]
  intro b h
  suffices {a ∈ s | g a = b}.Nonempty by
    simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]
  exact Finset.nonempty_of_prod_ne_one h

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

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
R' : Type u_6
M' : Type u_7
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
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
⊢ ∀ i ∈ S, r₁ i = r₂ i

Tactic:
s

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
R' : Type u_6
M' : Type u_7
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
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r₁ r₂ : ι → R'
H : ∑ i ∈ S, r₁ i • (⇑j ∘ v) i = ∑ i ∈ S, r₂ i • (⇑j ∘ v) i
s : ι
⊢ s ∈ S → r₁ s = r₂ s
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ ∑ n_1, (-1) ^ ↑n_1 = if Even (n + 1) then 0 else 1

Tactic:
simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]

Goal state after:
case succ
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
⊢ (if Even n then 0 else 1) + (-1) ^ n = if Even n then 1 else 0
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ (a * b).gcd (d * b) = b

Tactic:
rw [gcd_mul_right]

Goal state after:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b
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:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_lt h

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

Goal state before:
pp: n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑n ∣ ↑d - ↑c

Tactic:
convert! Int.dvd_sub h₂ h₁ using 1

Goal state after:
n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
⊢ ∀ i ∈ S, r' i = 0

Tactic:
s

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
r' : ι → R'
H : ∑ i ∈ S, r' i • (⇑j ∘ v) i = 0
s : ι
⊢ s ∈ S → r' s = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0

Tactic:
if_neg (not_le_of_gt hc),

Goal state after:
a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = (a + b) % c + 0
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
if_neg (not_le_of_gt hc),

Goal state after:
a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ a / c + b / c + 0 = a / c + b / c
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = #α

Tactic:
rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]

Goal state after:
α : Type u_1
inst✝ : Finite α
⊢ #α < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ ¬1 < Module.rank R R ∧ 1 ≤ Module.rank R R

Tactic:
← two_le_iff_one_lt,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ ¬2 ≤ Module.rank R R ∧ 1 ≤ Module.rank R R
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ Module.rank R R = 1

Tactic:
rw [le_antisymm_iff, ← not_lt, ← two_le_iff_one_lt, ← Nat.cast_two,
    Module.le_rank_iff_exists_linearMap, Module.one_le_rank_iff]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (¬∃ f, Injective ⇑f) ∧ ∃ f, Injective ⇑f
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:
by
  rw [← rank_range_of_surjective f h]
  apply lift_rank_range_le

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard = (s ∪ t).encard

Tactic:
by
  rw [← encard_union_eq disjoint_sdiff_left, sdiff_union_self]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : 1 < s.encard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra! h'

Goal state after:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ b ∈ s, b = a
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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

Tactic:
rw [linearIndependent_iff']
  simp only [exists_prop, not_forall]

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
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0

Tactic:
by
  refine
    ⟨fun H g => by simpa using linearIndependent_iff'.1 H Finset.univ g, fun H =>
      linearIndependent_iff''.2 fun s g hg hs i => H _ ?_ _⟩
  rw [← hs]
  refine (Finset.sum_subset (Finset.subset_univ _) fun i _ hi => ?_).symm
  rw [hg i hi, zero_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ ENat.card ↑s = s.encard

Tactic:
encard

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ ENat.card ↑s = ENat.card ↑s
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
⊢ Pi.mulSingle i (x i) ∈ H

Tactic:
simp [h2]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin ⋯.choose
⊢ α ≃ Fin (Nat.card α)

Tactic:
rwa [Nat.card_eq_of_equiv_fin this]

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:
Nat.cast_zero,

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).ncard ≤ 1

Tactic:
rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]
  apply encard_singleton_inter

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n ↦ x * n * x⁻¹) '' S)

Tactic:
Set.card_image_of_injective S conj_injective

Goal state after:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑S
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ leftRel (s.prod s') = (leftRel s).prod (leftRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [leftRel_apply]
  rfl

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
⊢ (f a.1 * ↑b)⁻¹ * (f a.1 * ↑c) ∈ s

Tactic:
rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Tactic:
intro h
    exact ⟨x.fst, Prod.ext rfl h.symm⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ insert (succ b) (Icc a b) = Icc a (succ b)

Tactic:
ext x; simp [or_and_left, le_succ_iff_eq_or_le]; simp_all

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s

Tactic:
convert! (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
    rw [Finset.inf_eq_iInf]
    simp_rw [Set.mem_toFinset]
    rfl

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

Goal state before:
pp: α : Sort u_4
β : Sort u_5
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ x y, x ≠ y ∧ f x = f y

Tactic:
by
  simpa [Injective, and_comm] using not_injective_infinite_finite f

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
this : Iic (Order.succ i) = Iic i ∪ {Order.succ i}
⊢ (partialSups f) (Order.succ i) = (partialSups f) i ⊔ f (Order.succ i)

Tactic:
simp only [partialSups_apply, this,
    sup'_union nonempty_Iic ⟨_, mem_singleton_self _⟩ f, sup'_singleton]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ sSup (Set.range fun i ↦ (partialSups f) i) = sSup (Set.range fun i ↦ f i)

Tactic:
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,

Goal state after:
case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ sSup (Set.range fun i ↦ (partialSups f) i) = sSup ∅
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case refine_2
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
this : y - x ∈ f.ker ⊔ g.ker
x' : M
hx' : x' ∈ f.ker
y' : M
hy' : y' ∈ g.ker
H : x' + y' = y - x
⊢ g (x' + x) = g y

Tactic:
· simp [← eq_sub_iff_add_eq.1 H, map_add, mem_ker.mp hy']

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

Goal state before:
pp: case succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ ¬IsMax (succ^[n + 1 - 1] i)

Tactic:
rw [Nat.succ_sub_succ_eq_sub, tsub_zero]

Goal state after:
case succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ ¬IsMax (succ^[n] i)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = image (fun i ↦ (i, n - i)) (range (n + 1))

Tactic:
by
  simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
refine prod_congr rfl fun i hi ↦ ?_
    rw [choose_symm (this _ hi)]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (x : (ι → R) ⧸ pi fun x ↦ I), 0 • x = 0

Tactic:
rintro ⟨a⟩; exact congr_arg _ (zero_smul _ _)

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

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
⊢ let s := x.support ∪ y.support;
  ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
s

Goal state after:
case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
⊢ ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets

Tactic:
rcases B.mem_filter_iff.mp U_in with ⟨V, V_in, h⟩

Goal state after:
case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot

Tactic:
by
  rw [neBot_iff, Ne, inf_principal_eq_bot]; rfl

Goal state after: