mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
⊢ Disjoint (f '' U) (f '' V)

Tactic:
rw [Set.disjoint_left]

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U V : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
h : ∀ x ∈ U, ∀ (g : G), g • x ∉ V
⊢ ∀ ⦃a : Quotient (orbitRel G α)⦄, a ∈ f '' U → a ∉ f '' V
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s

Tactic:
· convert! hh
    simpa using hg _ hh

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : SemiconjBy (f a) (f x) (f y)
⊢ f (a * x) = f (y * a)

Tactic:
by simpa only [SemiconjBy, map_mul] using h

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ (zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

Tactic:
zpowers_eq_closure,

Goal state after:
G : Type u_2
inst✝ : Group G
g : G
⊢ (closure {g}).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
this : ∀ b ∈ s.erase a, Commute a b
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
by
    rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']

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

Goal state before:
pp: M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod

Tactic:
refine Multiset.prod_dvd_prod_of_le ?_

Goal state after:
M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ map id S.toFinset.val ≤ S
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

Tactic:
exact fun _ => s.symm'

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
⊢ (cons a s h).prod = fun f ↦ f a * ∏ x ∈ s, f x

Tactic:
by
  funext f
  rw [Finset.prod_cons h]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : c.Quotient
⊢ ((fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯) ((fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d)) x y ↔ d x y

Tactic:
refine ⟨?_, Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : c.Quotient
⊢ ((fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯) ((fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d)) x y → d x y
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = g * ↑⟨g⁻¹ * Quotient.out ↑g, ⋯⟩

Tactic:
rw [mul_inv_cancel_left]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : IsEmpty α
⊢ Function.Injective ⇑(map f)

pp: case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)

Tactic:
· exact Function.injective_of_subsingleton _

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

Tactic:
have := Fintype.ofFinite ι
  refine iSup_map_mulSingle_le.antisymm fun x hx => ?_
  rw [← Finset.noncommProd_mulSingle x]
  exact noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
classical
  rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
commutator_eq_bot_iff_le_centralizer,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅H₂, H₃⁆ ≤ centralizer ↑H₁
h2 : ⁅H₃, H₁⁆ ≤ centralizer ↑H₂
⊢ ⁅H₁, H₂⁆ ≤ centralizer ↑H₃
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> y = (fun b a ↦ (a, b)) <$> y <*> pure p

Tactic:
induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
l : List ι
⊢ ∑ a ∈ l.toFinset, count a l = l.length

Tactic:
by
  simpa [List.map_const'] using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, H⁆ = ⊥ ↔ IsMulCommutative ↥H

Tactic:
commutator_eq_bot_iff_le_centralizer,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ centralizer ↑H ↔ IsMulCommutative ↥H
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, ⊤⁆ = ⊥ ↔ H ≤ center G

Tactic:
commutator_eq_bot_iff_le_centralizer,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ centralizer ↑⊤ ↔ H ≤ center G
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
commutator_comm

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₂, H₁⁆
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' • ↑u' • r₃ = r' • v • r₁

Tactic:
hur₂,

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' • v' • r₂ = r' • v • r₁
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ f (f.sec x✝).1 = f ↑(f.sec x✝).2 * x✝

Tactic:
← sec_spec'

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
x✝ : N
⊢ f (f.sec x✝).1 = f (f.sec x✝).1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ (OreLocalization.oreEqv S M) x y

Tactic:
simp +instances only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv,
    smul_eq_mul, Submonoid.mk_smul]
  constructor
  · rintro ⟨u, hu, e⟩
    exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩
  · rintro ⟨u, hu, v, e₁, e₂⟩
    exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

Tactic:
rw [← f.map_comp_map (k := k) hy j hl]

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = ((k.map hl j).comp (f.map hy k)) x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.mk' (x * ↑y) y = f x

Tactic:
mk'_mul_cancel_right

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f x = f x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : ∃ c, ↑c * (m * (ms₁.1 * ↑ms₂.2)) = ↑c * (m * (ms₂.1 * ↑ms₁.2))
⊢ ∃ c, ↑c * (ms₁.1 * ↑ms₂.2) = ↑c * (ms₂.1 * ↑ms₁.2)

Tactic:
simp_rw [mul_left_comm _ m] at eq

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : ∃ c, m * (↑c * (ms₁.1 * ↑ms₂.2)) = m * (↑c * (ms₂.1 * ↑ms₁.2))
⊢ ∃ c, ↑c * (ms₁.1 * ↑ms₂.2) = ↑c * (ms₂.1 * ↑ms₁.2)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : OreLocalization S M
x : OreLocalization S X
⊢ (r • m) • x = r • m • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, smul_eq_mul]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : Ioo a b = ∅
⊢ b ≤ succ a

pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
⊢ Ioo a b = ∅

Tactic:
· contrapose! h
    exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩

Goal state after:
case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
⊢ Ioo a b = ∅
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n] i)

Tactic:
have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
⊢ ¬IsMax (succ^[n] i)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f (a + 1) < f a) → StrictAnti f

Tactic:
simpa [Order.succ_eq_add_one] using strictAnti_of_succ_lt (f := f)

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∈ s
⊢ ↑(pred a) = pred ↑a

Tactic:
classical
  change Subtype.val (dite ..) = _
  simp [h]

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) g

Tactic:
rw [update_piecewise]
  refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..
  exact fun h => hj (h.symm ▸ hi)

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
classical
    convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
    rw [Fintype.card_sum]

Goal state after:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).get i.succ = v.get i

Tactic:
← get_tail_succ,

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).tail.get i = v.get i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ ¬a = x) ↑m) + count b ↑(replicate (count a ↑m) a) = count b ↑m

Tactic:
count_filter,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ (if ¬a = b then count b ↑m else 0) + count b ↑(replicate (count a ↑m) a) = count b ↑m
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ j ∈ univ.erase i, #(s j)

Tactic:
by
  calc
    _ = ∏ j, #(Function.update s i {a} j) := by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
    _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
    _ = _ := by simp [prod_update_of_mem, erase_eq]

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

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
· rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
      refine ⟨fun n => s n, fun n => hps _ (s n).coe_prop, ?_⟩
      rwa [hs.iSup_comp, ← sSup_eq_iSup']

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ univ.Countable

Tactic:
← Set.preimage_univ (f := f),

Goal state after:
α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ (f ⁻¹' univ).Countable
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_gt b

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁✝ a₂✝ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
a₁ a₂ : α
⊢ (⇑f)^[n] (f a₁) ⊔ a₂ = (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
by rw [← Function.iterate_succ_apply]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o ↦ o.toOption) ↑o = (↑o).toOption

Tactic:
by dsimp; congr

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) n = (pair (a₁, b₁) (a₂, b₂) ⋯) n

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ (lfp.comp h) (lfp h.onDiag) ≤ lfp h.onDiag

Tactic:
exact lfp_le _ h.onDiag.map_lfp.le

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ a ≤ ωSup c

Tactic:
apply h.2

Goal state after:
case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (a : ℕ), c a ≤ ωSup c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ ∀ (a b c : Cardinal.{u}), a ≤ b → b ≤ c → a ≤ c

Tactic:
by
    rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨e₁⟩ ⟨e₂⟩
    exact ⟨e₁.trans e₂⟩

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
by have := H i; rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this

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

Goal state before:
pp: c : ℕ
⊢ ↑(toNat ↑c) = ↑c

Tactic:
rw [toNat_natCast]

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

Goal state before:
pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * ⊤

Tactic:
rw [toENatAux_eq_top, ENat.mul_top]

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ x.toENatAux ≠ 0

case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s

Tactic:
use sum.{u, u} fun x ↦ e.symm x

Goal state after:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ (sum fun x ↦ ↑(e.symm x)) ∈ upperBounds s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 2 ≤ c ↔ 1 < c

Tactic:
convert! natCast_add_one_le_iff
  norm_cast

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ ∃ s, n = s.card

Tactic:
obtain ⟨t, -, rfl⟩ := @Finset.exists_subset_card_eq α .univ n <| by simpa using h

Goal state after:
case inl
α : Type u_1
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
t : Finset α
h : ↑t.card ≤ #α
⊢ ∃ s, t.card = s.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ succ c = c + 1

Tactic:
rw [hn, succ_natCast]

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

Goal state before:
pp: ⊢ (sum fun n ↦ 0 ^ n) = 1

Tactic:
by
  rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
f g : A →ₑ*[φ] B
h : (fun m ↦ m.toFun) f = (fun m ↦ m.toFun) g
⊢ f = g

Tactic:
by
    rcases f with ⟨tF, _, _⟩; rcases g with ⟨tG, _, _⟩
    cases tF; cases tG; congr

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R'
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R' M'
σ₁₂ : R →+* R'
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module S M'
inst✝¹ : SMulCommClass R' S M'
inst✝ : SMulCommClass R S M
x✝³ x✝² : Sᵈᵐᵃ
x✝¹ : M →ₛₗ[σ₁₂] M'
x✝ : M
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝

Tactic:
by
    simp_rw [add_apply, DomMulAct.smul_linearMap_apply, ← map_add, ← add_smul]; rfl

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
⊢ { toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    apply mul_smul

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑p = Set.univ ↔ p = ⊤

Tactic:
rw [iff_comm, ← SetLike.coe_set_eq, top_coe]

Goal state after: