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 : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)

Tactic:
eq

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ (mapDomain f v₂) (f a) = (mapDomain f v₂) (f a)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
⊢ mapDomain f v₁ = mapDomain f v₂ → v₁ = v₂

Tactic:
eq

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

Tactic:
eq

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ (mapDomain f v₂) (f a) = (mapDomain f v₂) (f a)

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ f a ≤ f a ^ #({a_1 ∈ s | g a_1 = a})

Tactic:
apply le_self_pow (hf a hag)

Goal state after:
ι : Type u_1
N : Type u_5
inst✝³ : CommMonoid N
inst✝² : Preorder N
s : Finset ι
ι' : Type u_9
inst✝¹ : DecidableEq ι'
inst✝ : MulLeftMono N
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ #({a_1 ∈ s | g a_1 = a}) ≠ 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst✝ : MulLeftStrictMono M
i j : ι
hij : j ≠ i
hi : i ∈ s
hj : j ∈ s
hlt : 1 < f j
hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k
⊢ f i = ∏ k ∈ {i}, f k

Tactic:
by rw [prod_singleton]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t \ s ∪ s ∩ t, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
inter_comm,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t \ s ∪ t ∩ s, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x < ∏ x ∈ t \ s ∪ s ∩ t, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
inter_comm,

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x < ∏ x ∈ t \ s ∪ t ∩ s, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = (range (x.card + 1)).bind fun k ↦ powersetCard k x

Tactic:
Multiset.bind,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) =
    (map (fun k ↦ powersetCard k x) (range (x.card + 1))).join
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∀ x ∈ m.toFinset, 1 ≤ count x m

Tactic:
by simp [one_le_count_iff_mem]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
h : Function.Surjective v
⊢ Function.Surjective ⇑(linearCombination R v)

Tactic:
by
  intro x
  obtain ⟨y, hy⟩ := h x
  exact ⟨single y 1, by simp [hy]⟩

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 α
hs : (s ∩ mulSupport f).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite

Tactic:
← mulSupport_mulIndicator

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (mulSupport (s.mulIndicator f)).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite
Module: Mathlib.Algebra.BigOperators.Finprod

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

Tactic:
← mulSupport_mulIndicator

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

Tactic:
g.map_finprod

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
M' : Type u_7
inst✝⁴ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ b.map (b.equiv b' e) = b'.reindex e.symm

Tactic:
by
  ext i
  simp

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

Goal state before:
pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
notMem_mulSupport.mp ha

Goal state after:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin m × Fin n
⊢ ↑x.2 + n * ↑x.1 + 1 = ↑x.1 * n + ↑x.2 + 1

Tactic:
by ac_rfl

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
← Nat.card_Ico,

Goal state after:
n : ℕ
a b : Fin n
⊢ #(Ico a b) = #(Ico ↑a ↑b)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : ¬↑i + ↑i + 1 < n + 1 + 1
⊢ ↑i + ↑i + 1 - (n + 1 + 1) = ((↑i + ↑i) % (n + 1 + 1) + 1 % (n + 1 + 1)) % (n + 1 + 1)

Tactic:
· rw [Fin.val_mk, not_lt] at h
      simp only [Nat.mod_add_mod,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by lia)]
      refine (Nat.mod_eq_of_lt ?_).symm
      lia

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ (Equiv.symm (finRotate n.succ)) i = i - 1

Tactic:
apply (finRotate n.succ).symm_apply_eq.mpr

Goal state after:
n : ℕ
i : Fin n.succ
⊢ i = (finRotate n.succ) (i - 1)
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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i

Tactic:
eq

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
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ (∏ i, f (castAdd b i)) * ∏ i, f (natAdd a i) = ∏ i, f (castAdd b i)

Tactic:
Fintype.prod_eq_one _ hf,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ (∏ i, f (castAdd b i)) * 1 = ∏ i, f (castAdd b i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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
w : ι → M
h : EqOn v w s
⊢ LinearIndepOn R v s ↔ LinearIndepOn R w s

Tactic:
rw [LinearIndepOn, LinearIndepOn]

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : ι → M
h : EqOn v w s
⊢ (LinearIndependent R fun (x : ↑s) ↦ v ↑x) ↔ LinearIndependent R fun (x : ↑s) ↦ w ↑x
Module: Mathlib.Algebra.Group.ModEq

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

Tactic:
· rw [hk, Int.ediv_mul_add_emod]

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

Goal state before:
pp: a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1

Tactic:
← Nat.sub_add_cancel h,

Goal state after:
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
this : a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1)
⊢ (a ^ (c - b + b) - 1) % (a ^ b - 1) = a ^ ((c - b + b) % b) - 1
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 : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this : ↑(↑hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
⊢ ↑hv.linearCombinationEquiv l = x

Tactic:
eq

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 : LinearIndependent R v
l : ι →₀ R
x : ↥(span R (range v))
eq : (Finsupp.linearCombination R v) l = ↑x
this : ↑(↑hv.linearCombinationEquiv l) = ↑x
⊢ ↑hv.linearCombinationEquiv l = x
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
h : a ≡ b [MOD n]
⊢ n ∣ b - a

Tactic:
obtain h0 | h0 : a ≤ b ∨ b ≤ a := le_total a b

Goal state after:
case inl
n a b : ℕ
h : a ≡ b [MOD n]
h0 : a ≤ b
⊢ n ∣ b - a

case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ b - a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
  exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

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

Goal state before:
pp: m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m]

Tactic:
by
  rcases m.eq_zero_or_pos with (rfl | hm)
  · simp only [gcd_zero_left] at hmc
    simp only [hmc, one_mul, modEq_zero_iff] at h
    subst h
    rfl
  simpa [hmc] using h.cancel_left_div_gcd hm

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ s.encard + {a}.encard = s.encard + 1

Tactic:
encard_singleton

Goal state after:
α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ s.encard + 1 = s.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
x y : α
hne : x ≠ y
⊢ {y}.encard + 1 = 1 + 1

Tactic:
encard_singleton

Goal state after:
α : Type u_1
x y : α
hne : x ≠ y
⊢ 1 + 1 = 1 + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ {x}.encard = 1

Tactic:
encard_singleton

Goal state after:
α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ 1 = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ {z}.encard + 1 + 1 = 3

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}

Tactic:
encard_singleton

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ 1 + 1 + 1 = 3

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ {w}.encard + 1 + 1 + 1 = 4

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ z ∉ {w}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ y ∉ {z, w}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ x ∉ {y, z, w}

Tactic:
encard_singleton

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ 1 + 1 + 1 + 1 = 4

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ z ∉ {w}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ y ∉ {z, w}

case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ x ∉ {y, z, w}
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0

Tactic:
have := card_eq_zero_iff.mp h
    have := Function.isEmpty f
    exact Nat.card_of_isEmpty

Goal state after:
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
⊢ s.ncard = Nat.card (Fin n)

Tactic:
← Set.ncard_univ,

Goal state after:
α : 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
⊢ s.ncard = univ.ncard
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case left_assoc
ι : 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)
⊢ ∀ (b c : A), z * (b * c) = z * b * c

pp: case mpr.right_assoc
ι : 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)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case left_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
        Finset.smul_sum, smul_mul_assoc, mul_smul_comm, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]
      rw [Finset.sum_comm]

Goal state after:
case mpr.right_assoc
ι : 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)
⊢ ∀ (a b : A), a * b * z = a * (b * z)
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 = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard

Tactic:
inter_comm,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (t ∩ s).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
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 ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
inter_comm,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (t ∩ s).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
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 < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
inter_comm,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (t ∩ s).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩

Tactic:
coe_mul_of_left_le_normalizer_right H N hLE

Goal state after:
G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H

Tactic:
have : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
    rwa [inv_one, one_mul] at this

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

Goal state before:
pp: case pos
α : Type u_3
s : Set α
hs : s.Finite
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard

pp: case neg
α : Type u_3
s : Set α
hs : ¬s.Finite
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard

Tactic:
· simp [(ncard_union_eq_iff (.image _ hs) (.image _ hs)).2 disjoint_image_inl_image_inr,
      ncard_image_of_injective _ Sum.inl_injective, ncard_image_of_injective _ Sum.inr_injective]

Goal state after:
case neg
α : Type u_3
s : Set α
hs : ¬s.Finite
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard