mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
by
  classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
this : (mulSupport fun x ↦ (fun x ↦ 1) x.down) ⊆ ↑∅
⊢ ∏ᶠ (x : α), 1 = 1

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

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:
rwa [Set.Finite.coe_toFinset]

Goal state after:
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
x : M
⊢ (linearCombination R ⇑b) (b.repr x) = x

Tactic:
by
  rw [← b.coe_repr_symm]
  exact b.repr.symm_apply_apply x

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
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x, if x = i then r • v x else 0) = r • v i

Tactic:
rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

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
v : α → M
x : M
⊢ (∃ c, (c.sum fun i a ↦ a • v i) = x) ↔ ∃ x_1, ∑ x, x_1 x • v x = x

Tactic:
exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

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

Goal state before:
pp: case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (if x = a then 1 else 0) + List.count a xs.toList = List.count a (x :: xs.toList)

Tactic:
List.count_cons,

Goal state after:
case cons
α : Type u_1
n✝ : ℕ
inst✝ : DecidableEq α
a : α
n : ℕ
x : α
xs : List.Vector α n
hxs : #{i | xs.get i = a} = List.count a xs.toList
⊢ (if x = a then 1 else 0) + List.count a xs.toList = List.count a xs.toList + if (x == a) = true then 1 else 0
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
rw [finprod_mem_insert, finprod_mem_singleton]

Goal state after:
case h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ a ∉ {b}

case hs
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a b : α
h : a ≠ b
⊢ {b}.Finite
Module: Mathlib.Data.Fin.VecNotation

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

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

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

case pos.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
⊢ vecCons x u ⟨↑⟨i + 1, hi⟩, h⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩
Module: Mathlib.Data.Fin.VecNotation

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

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

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

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⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

Goal state after:
case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

Goal state after:
case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a < a - b ↔ a < b

Tactic:
by
  fin_omega

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

Goal state before:
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

Tactic:
refine smul_left_injective _ nz ?_

Goal state after:
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 x_1 ↦ x_1 • x) (((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default) =
    (fun x_1 ↦ x_1 • x) (f default)
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
⊢ f i = (Finsupp.single i (f i)) i

Tactic:
Finsupp.single_eq_same

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (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
⊢ f i = f i
Module: Mathlib.Data.ENat.Pow

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

Tactic:
have : (0 : ℕ∞) ≤ 1 := zero_le_one

Goal state after:
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ x ^ ⊤ = ⊤
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
⊢ a ≡ b [PMOD 0] ↔ a = b

Tactic:
simp [modEq_iff_nsmul]

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

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

Tactic:
apply Fintype.prod_sum_type

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

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

Tactic:
apply add_right_cancel (b := a)

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + c + a = (n + k) • p + d + a
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (n + m * k) ↔ m.Coprime n

Tactic:
by
  rw [Coprime, Coprime, gcd_add_mul_left_right]

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin nn
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn

Tactic:
cases nn

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin 0
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * 0

case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * (n✝ + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + (↑(n.gcd m) - ↑n * n.gcdA m) * ↑a) / ↑(n.gcd m)

Tactic:
Int.sub_mul,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + (↑(n.gcd m) * ↑a - ↑n * n.gcdA m * ↑a)) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - ((↑(n.gcd m) - ↑m * n.gcdB m) * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
Int.sub_mul,

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑(n.gcd m) * ↑b - ↑m * n.gcdB m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ a.Coprime n

Tactic:
obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n

Goal state after:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.Coprime n
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  rw [encard_eq_zero]

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
h : s.encard ≤ ↑k
⊢ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k

Tactic:
by rwa [ENat.le_natCast_iff] at h

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1

Tactic:
rintro ⟨a, t, h, rfl, rfl⟩

Goal state after:
case refine_2
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + 1 ≤ ↑n
⊢ False

Tactic:
← Nat.cast_one,

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + ↑1 ≤ ↑n
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) → ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

pp: case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))) → ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0

Tactic:
· intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))

Goal state after:
case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))) → ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mpr
ι : 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)
⊢ z ∈ center A

Tactic:
rw [center, mem_ofPred_eq]

Goal state after:
case mpr
ι : 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)
⊢ IsMulCentral z
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ ↑s.ncard ≤ ↑t.ncard

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ ↑s.ncard ≤ t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
h' : ↑t.ncard ≤ ↑s.ncard
ht : t.Finite
⊢ t.encard ≤ s.encard

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
h' : t.encard ≤ ↑s.ncard
ht : t.Finite
⊢ t.encard ≤ s.encard
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:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ ↑s.ncard < t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s

Tactic:
rw [← mem_rightCoset_iff, ← h]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s

Tactic:
mem_rightCoset_iff,

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ ↑s ↔ x_1 * y⁻¹ ∈ ↑s) ↔ y * x⁻¹ ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = s.encard + ↑t.ncard

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = s.encard + t.encard
Module: Mathlib.Data.Set.Card

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

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard = s.encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + ↑s.ncard = ↑t.ncard

Tactic:
ht.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + ↑s.ncard = t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + ↑t.ncard

Tactic:
ht.cast_ncard_eq,

Goal state after:
case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_sdiff_eq_ncard s t hs, ← ncard_inter_add_ncard_sdiff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]

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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ s.ncard + s₁.ncard = k

Tactic:
hs₁card,

Goal state after:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ s.ncard + (k - s.ncard) = k
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
⊢ 1 < s.ncard

Tactic:
have : s.ncard ≠ 1 := fun h ↦ by simp [h] at he

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
this : s.ncard ≠ 1
⊢ 1 < s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
rw [← encard_eq_two, ncard_def]

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 2 ↔ s.encard = 2
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
by
  rw [← encard_eq_two, ncard_def]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0

Tactic:
have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩

Goal state after:
case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : R
x✝ : M × N
⊢ (-(x✝¹ • x✝).2, (x✝¹ • x✝).1) = (RingHom.id R) x✝¹ • (-x✝.2, x✝.1)

Tactic:
by
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ (fun x ↦ (x.2, -x.1)) ((fun x ↦ (-x.2, x.1)) x✝) = x✝

Tactic:
by
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
N : Type ?u.19
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : N × M
⊢ (fun x ↦ (-x.2, x.1)) ((fun x ↦ (x.2, -x.1)) x✝) = x✝

Tactic:
by
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Icc a b) (Icc (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iic, ← Ici_inter_Iic]
  exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => le_of_add_le_add_right hx.2

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p (f i \ (insert a✝ s✝).sup f)

Tactic:
| insert _ _ ht IH =>

Goal state after: