mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ Pi.single a (f a) = ⇑(single a (f a))

Tactic:
single_eq_pi_single

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ Pi.single a (f a) = Pi.single a (f a)
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

pp: case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Tactic:
· refine Or.inl ⟨h, ?_⟩
      rwa [h, (single_injective a₂).eq_iff] at eq

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a₁ a₂ : α
b₁ b₂ : M
eq : single a₁ b₁ = single a₂ b₂
h : ¬a₁ = a₂
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive f

Tactic:
suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive (single a (f a) + erase a f)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive (erase a f)

Tactic:
apply ih _ _

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case refine_1
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
⊢ (s i).mulIndicator (f i) ≤ (⋃ i, s i).mulIndicator (⨆ i, f i)

Tactic:
grw [← le_iSup f i, ← subset_iUnion s i]

Goal state after:
case hf
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
i : ι
⊢ 1 ≤ f i
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : optionElim y f ≠ 0
⊢ f ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! h

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
h : f = 0 ∧ y = 0
⊢ optionElim y f = 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: case cons
α : Type u_1
β : Type u_7
M : Type u_8
inst✝¹ : DecidableEq β
inst✝ : AddCommMonoid M
f : α → β →₀ M
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
ih : (s✝.sum f).support ⊆ s✝.sup fun x ↦ (f x).support
⊢ ((cons a✝ s✝ h✝).sum f).support ⊆ (cons a✝ s✝ h✝).sup fun x ↦ (f x).support

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -u • x = -(u • x)

Tactic:
by
  rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]

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

Goal state before:
pp: case inl
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑↑n)⁻¹ • x) = (↑↑n)⁻¹ • f x

pp: case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x

Tactic:
· rw [Int.cast_natCast, Int.cast_natCast, map_inv_natCast_smul _ R S]

Goal state after:
case inr
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : M
n : ℕ
⊢ f ((↑(-↑n))⁻¹ • x) = (↑(-↑n))⁻¹ • f x
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ∑ a, single a (f a) = f

Tactic:
refine DFunLike.coe_injective ?_
  simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]

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 : α → β
x : α →₀ M
b : β
h : (mapDomain f x) b ≠ 0
⊢ b ∈ Set.range f

Tactic:
contrapose! h

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
h : b ∉ Set.range f
⊢ (mapDomain f x) b = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
refine le_trans
    (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ ?_ ?_) ?_

Goal state after:
case refine_1
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ Multiset.map (fun i ↦ g i) s.val ≠ ∅

case refine_2
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ ∀ a ∈ Multiset.map (fun i ↦ g i) s.val, p a

case refine_3
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : s.Nonempty
hs : ∀ i ∈ s, p (g i)
⊢ (Multiset.map f (Multiset.map (fun i ↦ g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
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
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ ∏ k ∈ cons i {j} ⋯, f k ≤ ∏ k ∈ s, f k

Tactic:
refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ cons i {j} ⋯ ⊆ s
Module: Mathlib.Data.Finsupp.Basic

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

Tactic:
exact ⟨f, Multiset.mem_cons_self _ _, h⟩

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✝¹ : LinearOrder M
f g : ι → M
s : Finset ι
inst✝ : IsOrderedCancelMonoid M
hs : s.Nonempty
Hlt : ∀ i ∈ s, g i < f i
⊢ ∏ i ∈ s, g i < ∏ i ∈ s, f i

Tactic:
exact prod_lt_prod_of_nonempty' hs Hlt

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 : Finset α
h : mulSupport f ⊆ ↑s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

Tactic:
have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f := by
    rw [mulSupport_comp_eq_preimage]
    exact (Equiv.plift.symm.image_eq_preimage_symm _).symm
  have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
    rw [A, Finset.coe_map]
    exact image_mono h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this]
  simp only [Finset.prod_map, Equiv.coe_toEmbedding]
  congr

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 : mulSupport f ⊆ s
hs : s.Finite
⊢ mulSupport f ⊆ ↑hs.toFinset

Tactic:
Set.Finite.coe_toFinset

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : mulSupport f ⊆ s
hs : s.Finite
⊢ mulSupport f ⊆ s
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
i j : ι
inst✝ : Decidable (i = j)
⊢ (b.repr (b i)) j = if i = j then 1 else 0

Tactic:
rw [repr_self, Finsupp.single_apply]

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
by_cases h₂ : Set.Finite f.mulSupport
  · grind [finprod_eq_prod f h₂, Finset.prod_ne_zero_iff]
  · simp [finprod_of_infinite_mulSupport h₂]

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

Goal state before:
pp: case refine_1
α : 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 : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i ∈ s, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) i • v i = x

Tactic:
rw [← hc, ← Finset.sum_coe_sort (s := s)]

Goal state after:
case refine_1
α : 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 : Finset α
x✝ : ∃ c, ∑ i, c i • v ↑i = x
c : ↥s → R
hc : ∑ i, c i • v ↑i = x
⊢ ∑ i, (fun i ↦ if h : i ∈ s then c ⟨i, h⟩ else 0) ↑i • v ↑i = ∑ i, c i • v ↑i
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 : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∑ i, (fun i ↦ c ↑i) i • v ↑i = x

Tactic:
rw [← hc, ← Finset.sum_coe_sort (s := s)]

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 t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
← finprod_mem_union',

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∪ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

case hst
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ Disjoint (s ∩ t) (s \ t)

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s ∩ t ∩ mulSupport f).Finite

case ht
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (s \ t ∩ mulSupport f).Finite
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_1
x y : ℕ∞
h : x ^ y = 0
⊢ x = 0

Tactic:
contrapose! h

Goal state after:
case refine_1
x y : ℕ∞
h : x ≠ 0
⊢ x ^ y ≠ 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ x ^ (↑a✝ * ⊤) = (x ^ ↑a✝) ^ ⊤

Tactic:
rw [mul_top y_0, epow_top x_2, epow_top]

Goal state after:
case inr.inr.inr.inr.coe.top
x y z : ℕ∞
x_2 : 1 < x
a✝ : ℕ
y_0 : ↑a✝ ≠ 0
z_0 : ⊤ ≠ 0
⊢ 1 < x ^ ↑a✝
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ (k + m) • p + (a + c) = (l + n) • p + (b + d)

Tactic:
rw [add_nsmul, add_add_add_comm, hab, hcd, add_nsmul, add_add_add_comm]

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ 0 ≡ a [PMOD p] ↔ ∃ z, a = z • p

Tactic:
modEq_iff_eq_add_zsmul

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a : G
⊢ (∃ z, a = 0 + z • p) ↔ ∃ z, a = z • p
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ¬LinearIndepOn R v s ↔
    ∃ f g,
      f ∈ Finsupp.supported R R s ∧
        g ∈ Finsupp.supported R R s ∧ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g ∧ f ≠ g

Tactic:
by
  simp [linearIndepOn_iffₛ]

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

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (Fin.cons x xs (Fin.castLE ⋯ 0) * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 *
          (Fin.cons x xs (Fin.castLE ⋯ 0) * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a

Tactic:
Fin.castLE_zero,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (Fin.cons x xs 0 * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 *
          (Fin.cons x xs 0 * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n : ℕ
⊢ n % 4 = 3 → n % 2 = 1

Tactic:
by
  simpa [ModEq] using @ModEq.of_mul_left 2 n 3 2

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

Goal state before:
pp: case refine_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
⊢ ∀ i ∈ s, f i = g i

Tactic:
specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_
    · simp_rw [Finset.disjoint_left, Finset.mem_filter]
      exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'
    · rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]
      conv_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]
      conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]
      convert! heq
        <;> simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]
        <;> congr! 2 with i hi
        <;> simp only [Finset.mem_filter] at hi
      · simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]
      · simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]
    simp only [Finset.mem_filter] at h
    intro i hi
    by_cases hi' : g i ≤ f i
    · apply hi'.antisymm'
      simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩
    · apply (not_le.1 hi').le.antisymm
      simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₁ : ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
⊢ ∑ i, (-1) ^ (↑i + 1) • (r i.castSucc + r i.succ) =
    ∑ i, (-1) ^ (↑i + 1) • r i.castSucc + ∑ i, (-1) ^ (↑i + 1) • r i.succ

Tactic:
zsmul_add,

Goal state after:
α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₁ : ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
⊢ ∑ x, ((-1) ^ (↑x + 1) • r x.castSucc + (-1) ^ (↑x + 1) • r x.succ) =
    ∑ i, (-1) ^ (↑i + 1) • r i.castSucc + ∑ i, (-1) ^ (↑i + 1) • r i.succ
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
let := Fintype.ofSubsingleton a

Goal state after:
α : Type u_1
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
⊢ ∃ s, lift.{w, v} #↑s = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
by
  rcases Cardinal.lt_lift_iff.mp h with ⟨c', hc', hcc'⟩
  rcases exists_lt_of_lt_ciSup (by simpa [← hcc', Module.rank_def] using h) with ⟨⟨s, hs⟩, h⟩
  rcases Cardinal.le_mk_iff_exists_subset.mp h.le with ⟨t, hst, ht⟩
  exact ⟨t, by simp [ht, hcc'], hs.mono hst⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : ¬FaithfulSMul R M
⊢ Module.rank R M = 0

Tactic:
contrapose! h

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.rank R M ≠ 0
⊢ FaithfulSMul R M
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
by
  rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans natCast_lt_aleph0
  · exact natCast_lt_aleph0

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

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
contrapose! h

Goal state after:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ finrank R M ≤ n
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'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(f ∘ₗ p.subtype).range) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
rwa [LinearMap.range_comp, range_subtype] at h

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

Tactic:
have h := lift_rank_range_le (f.comp (Submodule.subtype p))
  rwa [LinearMap.range_comp, range_subtype] at h

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

Tactic:
rw [linearIndependent_iff'ₛ]
  refine ⟨fun h s f ↦ ?_, fun h s f g ↦ ?_⟩
  · convert! h s f 0; simp_rw [Pi.zero_apply, zero_smul, Finset.sum_const_zero]
  · rw [← sub_eq_zero, ← Finset.sum_sub_distrib]
    convert! h s (f - g) using 3; simp only [Pi.sub_apply, sub_smul, sub_eq_zero]

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

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

Tactic:
rw [Setoid.prod_apply]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (leftRel (s.prod s')) x y ↔ (leftRel s) x.1 y.1 ∧ (leftRel s') x.2 y.2
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = AddSubgroup.toIntSubmodule (span ℤ (range ⇑b)).toAddSubgroup

Tactic:
toAddSubgroup_toIntSubmodule

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M✝ : Type u_5
M' : Type u_6
M : Type u_7
R : Type u_8
inst✝⁴ : Ring R
inst✝³ : Nontrivial R
inst✝² : IsAddTorsionFree R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : AddSubgroup M
ι : Type u_9
b : Basis ι R M
h : A = AddSubgroup.closure (range ⇑b)
⊢ span ℤ (range ⇑b) = span ℤ (range ⇑b)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ ((rightRel s).prod (rightRel s')) x y

Tactic:
rw [Setoid.prod_apply]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ (graphOn f s).ncard = s.ncard

Tactic:
← fst_injOn_graph.ncard_image,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ (Prod.fst '' graphOn f s).ncard = s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ

Tactic:
contrapose! h

Goal state after:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ Nat.card α ≤ s.ncard + t.ncard