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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
⊢ ∀ a ∈ Multiset.map (fun i ↦ g i) s.val, p a

Tactic:
intro _ ha

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
M : Type u_4
inst✝ : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
a✝ : M
ha : a✝ ∈ Multiset.map (fun i ↦ g i) s.val
⊢ p 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
⊢ f.curry.support = image Prod.fst f.support

Tactic:
unfold Finsupp.curry

Goal state after:
α : 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
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
rw [mul_assoc]

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
rw [mul_assoc]

Goal state after:
case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 ≤ f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ 2 * (r i * ((∑ j ∈ s, g j) * ∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
rw [mul_assoc]

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

Goal state before:

Tactic:
rw [mul_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Subsingleton R
⊢ HasFiniteSupport f

pp: case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ HasFiniteSupport f

Tactic:
· simp_rw [HasFiniteSupport, Subsingleton.support_eq, finite_empty]

Goal state after:
case inr
α : Type u_1
R : Type u_7
inst✝ : NonAssocSemiring R
f : α → R
h : ∑ᶠ (i : α), f i = 1
h✝ : Nontrivial R
⊢ HasFiniteSupport f
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
v : ι →₀ R
⊢ (v.sum fun i vi ↦ b.repr.symm (single i vi)) = (linearCombination R ⇑b) v

Tactic:
simp only [repr_symm_single,
                                                         Finsupp.linearCombination_apply]

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

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

Tactic:
range_natAdd

Goal state after:
n m : ℕ
i : Fin n
⊢ Ici (natAdd m i) ⊆ {i | m ≤ ↑i}
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ 1 < ∏ᶠ (i : ι) (_ : i ∈ univ), f i

Tactic:
apply one_lt_finprod_cond

Goal state after:
case h
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∀ i ∈ univ, 1 ≤ f i

case h'
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ ∃ i ∈ univ, 1 < f i

case hf
ι : Type u_3
M : Type u_7
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
h : ∀ (i : ι), 1 ≤ f i
h' : ∃ i, 1 < f i
hf : HasFiniteMulSupport f
⊢ (mulSupport f ∩ {i | i ∈ univ}).Finite
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
x : M
i✝ : ι
a✝ : Nontrivial R
i j : ι
⊢ Injective fun i ↦ ⟨b i, ⋯⟩

Tactic:
exact fun i j h => b.injective (Subtype.mk.inj h)

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h : ¬↑⟨i + 1, hi⟩ < m + 1
⊢ v ⟨↑⟨i + 1, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩

Tactic:
rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h

Goal state after:
case neg.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h✝ : ¬↑⟨i + 1, hi⟩ < m + 1
h : m ≤ i
⊢ v ⟨↑⟨i + 1, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: case inr
n i : ℕ
hi : i ≥ n
⊢ (Sum.inr (i - n)).isLeft = decide (i < n)

Tactic:
hi.not_gt,

Goal state after:
case inr
n i : ℕ
hi : i ≥ n
⊢ (Sum.inr (i - n)).isLeft = decide False
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:
finRotate_apply

Goal state after:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
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✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False

Tactic:
simp_rw [Finsupp.linearCombination_apply] at e

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : ((b.repr x).sum fun i a ↦ a • b i) = x
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
⊢ False
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 : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.lapply i) (Finsupp.single j (f j)) = 0

Tactic:
by rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne' hji]

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
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✝
⊢ x✝ ∈ f.support ∪ g.support

Tactic:
· contrapose hni
          simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni
          rw [hni.1, hni.2]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
x✝ : a ≡ b [PMOD n • p]
k l : ℕ
h : k • n • p + a = l • n • p + b
⊢ (k * n) • p + a = (l * n) • p + b

Tactic:
by simpa [mul_nsmul']

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ (k % ↑n).toNat < n ∧ ∃ m, a - b = (m * ↑n + ↑(k % ↑n).toNat) • p

Tactic:
← Int.ofNat_lt,

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℤ
hk : a - b = k • p
⊢ ↑(k % ↑n).toNat < ↑n ∧ ∃ m, a - b = (m * ↑n + ↑(k % ↑n).toNat) • p
Module: Mathlib.Algebra.BigOperators.Fin

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

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

Tactic:
· simp [*]

Goal state after:
case neg
R : Type u_3
inst✝ : Ring R
n : ℕ
IH : ∑ n_1, (-1) ^ ↑n_1 = if Even n then 0 else 1
h : ¬Even n
⊢ 1 + (-1) ^ n = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩
  convert! h.units_smul (fun i ↦ (w i)⁻¹)
  simp [funext_iff]

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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∉ span R (v '' s)

Tactic:
by
  have h' : v x ∈ Submodule.span R (v '' {x}) := by
    rw [Set.image_singleton]
    exact mem_span_singleton_self (v x)
  intro w
  apply LinearIndependent.ne_zero x hv
  refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w
  simpa using h

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

Goal state before:
pp: m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ d ∣ a ↔ d ∣ b

Tactic:
simp only [← modEq_zero_iff_dvd]

Goal state after:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
isLt✝² : a < n
b : ℕ
isLt✝¹ : b < n
c : ℕ
isLt✝ : c < n
⊢ a * b * c ≡ a * (b * c) [MOD n]

Tactic:
rw [mul_assoc]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ [].alternatingProd = ∏ i, [][i] ^ (-1) ^ ↑i

Tactic:
rw [alternatingProd, Finset.prod_eq_one]
    rintro ⟨i, ⟨⟩⟩

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

Goal state before:
pp: case refine_1
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i✝ : G →* L
his : i✝ ∈ s
x y : G
i : G →* L
⊢ g i * i x * i y = g i * (i x * i y)

Tactic:
rw [mul_assoc]

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
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
Module.rank

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ ι, #↑↑ι)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.encard = ↑s.toFinset.card

Tactic:
rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]

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

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

Tactic:
unfold encard
  simp [ENat.card_congr (Equiv.Set.union h)]

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ Module.rank R M

Tactic:
Module.rank

Goal state after:
R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ ⨆ ι, #↑↑ι ≤ ⨆ ι, #↑↑ι
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
lt_iff_not_ge,

Goal state after:
α : Type u_1
s : Set α
⊢ ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}
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
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
⊢ l = 0

Tactic:
by
      ext i; simp only [Finsupp.zero_apply]
      by_contra hn
      refine hn (H i _ ?_)
      refine (Finsupp.mem_span_image_iff_linearCombination R).2 ⟨Finsupp.single i (l i) - l, ?_, ?_⟩
      · rw [Finsupp.mem_supported']
        intro j hj
        have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_sdiff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)
        simp [hij]
      · simp [hl]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
simp only [preimage_sdiff, subset_def, mem_sdiff, mem_singleton_iff, mem_preimage, and_imp]
    at hf₀s

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard = hs.toFinset.card

Tactic:
← _root_.Nat.card_coe_set_eq,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ Nat.card ↑s = hs.toFinset.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.ncard = s.toFinset.card

Tactic:
simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
← _root_.Nat.card_coe_set_eq,

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ Nat.card ↑s = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
⊢ {x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s

Tactic:
refine ⟨nonempty_of_ncard_ne_zero, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
⊢ y ∈ f '' s → {x | x ∈ s ∧ f x = y}.ncard ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.ncard < t.ncard

Tactic:
rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]

Goal state after:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.encard < t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
b : α
⊢ b ∈ op a • ↑s ↔ b ∈ ↑s

Tactic:
by simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s

Tactic:
rw [mul_assoc]

Goal state after:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
y : β
hy : y ∈ t
⊢ ∃ a, f' a = ⟨y, hy⟩

Tactic:
obtain ⟨a, ha, rfl⟩ := hsurj y hy

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = ⟨f a ha, hy⟩
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
r : R
a : A
b : B
⊢ ((algebraMap R A) r * a, (algebraMap R B) r * b) = (a * (algebraMap R A) r, b * (algebraMap R B) r)

Tactic:
rw [commutes r a, commutes r b]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
h : s.ncard = 1
⊢ False

Tactic:
simp [h] at he

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ sInf (Set.range (DFunLike.coe ∘ f)) = ⨅ i, ⇑(f i)

Tactic:
sInf_range,

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ iInf (DFunLike.coe ∘ f) = ⨅ i, ⇑(f i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = Pi.single i (b i) i

Tactic:
refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ i ∉ I → Pi.single i (b i) i = 0
Module: Mathlib.Order.Interval.Set.SuccPred

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

Tactic:
Ico_succ_right_of_not_isMax hb,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Icc a b
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:
by
    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.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[(-0).toNat] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Tactic:
simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

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

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)

Tactic:
rw [sub_mul, mul_sub]; abel

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ (a : R ⧸ I), a ≠ 0 → ∃ b, b * a = 1

Tactic:
rintro ⟨a⟩ h

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
⊢ f #z = f y

Tactic:
rw [(mem_powersetCard.1 hz).2]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
refine sum_congr rfl fun y _ ↦ ?_
    rw [← card_powersetCard, ← sum_const]
    refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_
    rw [(mem_powersetCard.1 hz).2]

Goal state after: