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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
⊢ g • 0 = 0

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝² : Monoid G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
a : α
⊢ (g • 0) a = 0 a
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : 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
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ f (f.symm x) • y • z = x • y • z

Tactic:
f.apply_symm_apply

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝ : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module R✝ M'
ι : 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
R' : Type u_13
inst✝¹ : Semiring R'
inst✝ : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), f c • x = c • x
this : Module R' R := compHom R ↑f.symm
x : R'
y : R
z : M
⊢ x • y • z = x • y • z
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 bi : M
i : ι
h : b i = bi
⊢ (b.reindexRange.repr x) ⟨bi, ⋯⟩ = (b.repr x) i

Tactic:
by
  nontriviality
  subst h
  apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm
  · intro x y
    ext i
    simp only [Pi.add_apply, map_add, Finsupp.coe_add]
  · intro c x
    ext i
    simp
  · intro i
    ext j
    simp only [reindexRange_repr_self]
    apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))
    exact fun i j h => b.injective (Subtype.mk.inj 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 : Set α
h : x ∈ span R (v '' s)
⊢ ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x

pp: case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Tactic:
· obtain ⟨l, hl, hx⟩ := (Finsupp.mem_span_image_iff_linearCombination R).mp h
    refine ⟨l.support, hl, l ∘ (↑), ?_⟩
    rw [← hx]
    exact l.support.sum_coe_sort fun a ↦ l a • v a

Goal state after:
case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
finprod_mem_union' _ _ hs,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ {a}), f i) * ∏ᶠ (i : α) (_ : i ∈ s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ Disjoint {a} s

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : i.succAbove j ≠ i
⊢ (finSuccEquiv' i) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))

Tactic:
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩

Goal state after:
n : ℕ
j i : Fin n
hi : i.castSucc ≠ Fin.last n
hj : i.castSucc.succAbove j ≠ i.castSucc
⊢ (finSuccEquiv' i.castSucc) (i.castSucc.succAbove j) = some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = !((finSumNatEquiv n).symm i).isLeft

Tactic:
cases (finSumNatEquiv n).symm i

Goal state after:
case inl
n i : ℕ
val✝ : Fin n
⊢ (Sum.inl val✝).isRight = !(Sum.inl val✝).isLeft

case inr
n i val✝ : ℕ
⊢ (Sum.inr val✝).isRight = !(Sum.inr val✝).isLeft
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt0_vecAppend]; rfl

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

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ (fun a ↦ r * ∑ᶠ (_ : a ∈ s), f a) = fun a ↦ ∑ᶠ (_ : a ∈ s), r * f a

Tactic:
ext a

Goal state after:
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ r * ∑ᶠ (_ : a ∈ s), f a = ∑ᶠ (_ : a ∈ s), r * f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
⊢ (fun a ↦ (∑ᶠ (_ : a ∈ s), f a) * r) = fun a ↦ ∑ᶠ (_ : a ∈ s), f a * r

Tactic:
ext a

Goal state after:
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
s : Set α
f : α → R
r : R
a : α
⊢ (∑ᶠ (_ : a ∈ s), f a) * r = ∑ᶠ (_ : a ∈ s), f a * r
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ ↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1

Tactic:
Fin.val_add_one i

Goal state after:
n : ℕ
i : Fin n.succ
⊢ (if i = Fin.last n then 0 else ↑i + 1) = if i = Fin.last n then 0 else ↑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
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ (fun a ↦ ∏ᶠ (b : β × γ), f (a, b)) = fun a ↦ ∏ᶠ (b : β) (c : γ), f (a, b, c)

Tactic:
ext a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
a : α
⊢ ∏ᶠ (b : β × γ), f (a, b) = ∏ᶠ (b : β) (c : γ), 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
b : Basis ι R M
p : Submodule R M
h : p = ⊤
⊢ ∀ (i : ι), b i ∈ p

Tactic:
by simp [h]

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

Goal state before:
pp: case mpr.refine_1
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y z : ι →₀ R
⊢ (y + z) default • x = y default • x + z default • x

pp: case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x

pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
· simp [Finsupp.add_apply, add_smul]

Goal state after:
case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x

case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ x ^ ⊤ = ⊤

Tactic:
epow_def,

Goal state after:
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ (if ⊤ < ⊤ then x ^ ⊤.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤) = ⊤
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ioc a b, f (Fin.cast h i)

Tactic:
by
  simp [← map_finCongr_Ioc]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 = a ^ (c % b) - 1

pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 < a ^ b - 1

Tactic:
mod_eq_of_lt h

Goal state after:
case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 = a ^ c - 1

case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c - 1 < a ^ b - 1
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      a [MOD n] ∧
    (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      b [MOD m]

Tactic:
xgcd_val

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ (match (n.gcdA m, n.gcdB m) with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      a [MOD n] ∧
    (match (n.gcdA m, n.gcdB m) with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      b [MOD m]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by simp [h]

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

Goal state before:
pp: case e'_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x) +
      ∑ i ∈ s with f i < g i, f i • v i =
    ∑ i ∈ s with g i ≤ f i, f i • v i + ∑ i ∈ s with f i < g i, f i • v i

Tactic:
congr! 2 with i hi

Goal state after:
case e'_2.a
ι : 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 : ι
hi : i ∈ {i ∈ s | g i ≤ f i}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_3
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∑ i ∈ s with g i ≤ f i, g i • v i +
      ∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x) =
    ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, g i • v i

Tactic:
congr! 2 with i hi

Goal state after:
case e'_3.a
ι : 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 : ι
hi : i ∈ {x ∈ s | f x < g x}
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case e'_2.a
ι : 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 : ι
hi : i ∈ s ∧ g i ≤ f i
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i

Tactic:
simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]

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

Goal state before:
pp: α : Type u_3
⊢ 1 ≤ card α ↔ Nonempty α

Tactic:
simp [Order.one_le_iff_ne_zero, card_eq_zero_iff_empty]

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ card α
x y : α
⊢ 3 ≤ #α

Tactic:
by simpa [ENat.card] using h

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

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

Tactic:
← encard_singleton x,

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ {x}.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ s.encard ≠ 0

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ s.encard ≤ {x}.encard

Tactic:
by simp [h]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊤
⊢ Nat.card ↥H = Nat.card G

Tactic:
by simpa only [h] using card_top

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊥
⊢ Nat.card ↥H ≤ 1

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
rcases s.infinite_or_finite with hs | hs

Goal state after:
case inl
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Infinite
⊢ (s \ {a}).ncard = s.ncard - 1

case inr
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard = s.ncard - 1
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ z * ∑ i ∈ (b.repr c).support, (b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a

Tactic:
Finset.mul_sum,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a

Tactic:
Finset.mul_sum,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ i ∈ (b.repr c).support, z * ((b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (z * ∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * (b.repr d) i • b i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ (s \ {a}).ncard ≤ s.ncard

pp: case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
· apply ncard_le_ncard sdiff_subset hs

Goal state after:
case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, z * (b.repr c) x • (b x * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i

Tactic:
Finset.mul_sum,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, z * (b.repr c) x • ∑ i ∈ (b.repr d).support, b x * (b.repr d) i • b i =
    ∑ i ∈ (b.repr d).support, (∑ i ∈ (b.repr c).support, z * (b.repr c) i • b i) * (b.repr d) i • b i
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, (b.repr c) x • (z * ∑ x_1 ∈ (b.repr d).support, (b.repr d) x_1 • (b x * b x_1)) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr d) x • ((b.repr c) x_1 • (z * b x_1) * b x)

Tactic:
Finset.mul_sum,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ∑ x ∈ (b.repr c).support, (b.repr c) x • ∑ i ∈ (b.repr d).support, z * (b.repr d) i • (b x * b i) =
    ∑ x ∈ (b.repr d).support, ∑ x_1 ∈ (b.repr c).support, (b.repr d) x • ((b.repr c) x_1 • (z * b x_1) * b x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ s.encard

Tactic:
(hs.image _).cast_ncard_eq

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : ↑(f '' s).ncard = s.encard
hs : s.Finite
⊢ InjOn f s

Tactic:
(hs.image _).cast_ncard_eq

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ (f' '' univ).ncard = univ.ncard

Tactic:
exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h

Goal state after: