mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

pp: case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
· rw [mk_eq_mk_iff_isConj] at H
    exact H.eq_of_left_mem_center hx

Goal state after:
case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
⊢ S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer

Tactic:
simp_all [subset_def, mem_centralizer_iff]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • um • m = um • a • m

Tactic:
by rw [units_smul_def, units_smul_def, mul_smul_comm, smul_mul_assoc]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ (MulAut.conj g)⁻¹ • (g * n * g⁻¹) ∈ H

Tactic:
← map_inv,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ MulAut.conj g⁻¹ • (g * n * g⁻¹) ∈ H
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
hx : x ∈ closure s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

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

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ : β
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ x✝

Tactic:
| refl _ =>

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

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = mapOfSurjective f h hf

Tactic:
← conGen_of_con (c.mapOfSurjective f h hf)

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = conGen ⇑(mapOfSurjective f h hf)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : α
⊢ (lift f) (of x) = f x

Tactic:
simp [of]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
hf : Function.Surjective f
⊢ (lift f).range = ⊤

Tactic:
range_lift_eq_closure,

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
hf : Function.Surjective f
⊢ Subgroup.closure (Set.range f) = ⊤
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (lift (of ∘ f)).range = Subgroup.closure (of '' Set.range f)

Tactic:
range_lift_eq_closure,

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ Subgroup.closure (Set.range (of ∘ f)) = Subgroup.closure (of '' Set.range f)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : ∏ x ∈ s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
contrapose! h

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : ∀ a ∈ s, f a = 1
⊢ ∏ x ∈ s, f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
N : Submonoid M
| N.FG

Tactic:
← N.mrange_subtype,

Goal state after:
M : Type u_1
inst✝ : Monoid M
N : Submonoid M
| (MonoidHom.mrange N.subtype).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
l : List ι
f : ι → M
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l

Tactic:
induction l with
  | nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
  | cons a s IH =>
  simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∀ x ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = x, f y = 1

Tactic:
intro xbar

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
xbar : Quotient R
⊢ xbar ∈ image (Quotient.mk R) s → ∏ y ∈ s with ⟦y⟧ = xbar, f y = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ _root_.commutator G

Tactic:
rw [commutator_eq_closure]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case 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' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
⊢ ∃ u v, u • r = v • r' ∧ ↑u * ↑s = v * ↑s'

Tactic:
rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩

Goal state after:
case 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' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ ∃ u v, u • r = v • r' ∧ ↑u * ↑s = v * ↑s'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = r₁ * r' * r₂ /ₒ s

Tactic:
OreLocalization.expand' _ s t'

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)
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)
⊢ g (f.sec 1).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec 1).2)⁻¹ = 1

Tactic:
rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])

Goal state after:
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 : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : S.IsLocalizationMap ⇑f
⊢ f 1 = 1

Tactic:
← (hf.map_units 1).mul_right_inj,

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : S.IsLocalizationMap ⇑f
⊢ f ↑1 * f 1 = f ↑1 * 1
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
z : N
⊢ f (f.sec z).1 = f ↑(f.sec z).2 * z

Tactic:
rw [mul_comm, sec_spec]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)

Tactic:
exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithTop α
h : a ≠ 0
⊢ a * ⊤ = ⊤

Tactic:
rw [mul_top', if_neg h]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
c✝ : WithTop α
b c : α
h₀ : 0 < a
hbc : b < c
⊢ a * b < a * c

Tactic:
exact mul_lt_mul_of_pos_left hbc h₀

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x y : OreLocalization S R
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (x * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ x * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y

Tactic:
cases x with | _ r₁ s₁
    cases y with | _ r₂ s₂
    rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
    rw [liftExpand_of, liftExpand_of, liftExpand_of, Units.inv_mul_eq_iff_eq_mul, map_mul, map_mul,
      Units.val_mul, mul_assoc, ← mul_assoc (fS s₁ : T), ← mul_assoc (fS s₁ : T), Units.mul_inv,
      one_mul, ← hf, ← mul_assoc, ← map_mul _ _ r₁, ha, map_mul, hf s₂, mul_assoc,
      ← mul_assoc (fS s₂ : T), (fS s₂).mul_inv, one_mul]

Goal state after:
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 : Type ?u.51
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : IsScalarTower R M M
inst✝¹ : MulAction R X
inst✝ : IsScalarTower R M X
x : X
s : ↥S
⊢ 1 • (x /ₒ s) = x /ₒ s

Tactic:
rw [← smul_one_oreDiv_one_smul, one_smul, ← OreLocalization.one_def, one_smul]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ ⊥
x0' : ⊥ ≠ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ ⊥
x0' : ⊥ ≠ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a b : WithBot α
x0 : 0 ≤ ⊥
h : ⊥ * a < ⊥ * b
x0' : ⊥ ≠ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a b : WithBot α
x0 : 0 ≤ ⊥
h : a * ⊥ < b * ⊥
x0' : ⊥ ≠ 0
⊢ False

Tactic:
exact (WithBot.bot_lt_coe (0 : α)).not_ge x0

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : x < y
⊢ x ≤ pred y

Tactic:
exact le_pred_of_lt 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

Tactic:
contrapose! h

Goal state after:
case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : succ a < b
⊢ (Ioo a b).Nonempty
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 - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i

Tactic:
exact hn h_not_max

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
rw [Finset.prod_eq_one]
    grind

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1

Tactic:
rw [Finset.prod_eq_one]
    grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β

Tactic:
refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
  contrapose! H; cases H
  infer_instance

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

Goal state before:
pp: α : Type u_1
f : Fin 0 → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_zero, toList, nil]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (f 0 ::ᵥ ofFn fun i ↦ f i.succ).toList = f 0 :: List.ofFn fun i ↦ f i.succ

Tactic:
toList_cons,

Goal state after:
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ f 0 :: (ofFn fun i ↦ f i.succ).toList = f 0 :: List.ofFn fun i ↦ f i.succ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (v.head ::ᵥ v.tail).head ∈ (v.head ::ᵥ v.tail).toList

Tactic:
toList_cons,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (v.head ::ᵥ v.tail).head ∈ v.head :: v.tail.toList
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ (v.head ::ᵥ v.tail).toList

Tactic:
toList_cons,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.head :: v.tail.toList
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty β
h : Countable (α × β)
⊢ Countable α

Tactic:
contrapose! h

Goal state after:
α : Type u
β : Type v
inst✝ : Nonempty β
h : Uncountable α
⊢ Uncountable (α × β)
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty α
h : Countable (α × β)
⊢ Countable β

Tactic:
contrapose! h

Goal state after:
α : Type u
β : Type v
inst✝ : Nonempty α
h : Uncountable β
⊢ Uncountable (α × β)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ (x : α), x ∈ v.toList → p x
i : ℕ
hi : i < n
⊢ v[i] ∈ v.toList

Tactic:
simp [getElem_def, List.getElem_mem]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
⊢ Countable (List α)

Tactic:
have := Encodable.ofCountable α

Goal state after:
α✝ : Type u_1
inst✝¹ : Encodable α✝
α : Type u_2
inst✝ : Countable α
this : Encodable α
⊢ Countable (List α)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ (↑⟨l, hl⟩).length

Tactic:
rw [hl]

Goal state after:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ n
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
· exact h.isLUB_Iio.csSup_eq ⟨⊥, hx⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : c₀ i ≤ c₁ w✝
⊢ c₀ i ≤ ωSup c₁

Tactic:
exact le_trans h (le_ωSup _ _)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

Tactic:
constructor <;> intros
  · trans ωSup c
    · exact le_ωSup _ _
    · assumption
  exact ωSup_le _ _ ‹_›

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < ↑n ↔ a < ↑n

Tactic:
rw [← lift_natCast.{v, u}, lift_lt]

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

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n < lift.{v, u} a ↔ ↑n < a

Tactic:
rw [← lift_natCast.{v, u}, lift_lt]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

Tactic:
by
  simp_rw [IsSMulRegular, Function.Injective]
  conv_rhs => rw [← n.sign_mul_natAbs]
  obtain h | h | h := n.sign_trichotomy
  · simp [h]
  · simp [Int.sign_eq_zero_iff_zero.mp h]
  · simp [h, neg_zsmul]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ (fun x ↦ 0 • x) a = (fun x ↦ 0 • x) b

Tactic:
dsimp only [Function.comp_def]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (iSup f) = ⨆ i, lift.{u, w} (f i)

Tactic:
by
  rw [iSup, iSup, lift_sSup hf, ← range_comp]
  simp [Function.comp_def]

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

Goal state before:
pp: c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
contrapose! h

Goal state after:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)

Tactic:
by
    obtain ⟨f⟩ := Quotient.exact h
    exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩

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

Goal state before:
pp: α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
contrapose! h

Goal state after:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α ≤ ↑l.length
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S✝ : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : AddCommMonoid V
inst✝¹¹ : Module R V
inst✝¹⁰ : Module S V
inst✝⁹ : AddCommMonoid W
inst✝⁸ : Module R W
inst✝⁷ : Module S W
inst✝⁶ : AddCommMonoid G
inst✝⁵ : Module R G
inst✝⁴ : Module S G
inst✝³ : SMulCommClass R S W
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R V
inst✝ : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x✝ : W
⊢ (↑α • ↑e).toFun ((fun x ↦ ↑α⁻¹ • e.symm x) x✝) = x✝

Tactic:
by simp [smul_smul]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : f ≠ 0
s : Set (Submodule R M)
hs : sSup s = ⊤
⊢ ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0

Tactic:
contrapose! h

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ f = 0
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
⊢ p ≤ comap (f ^ k) p

Tactic:
induction k with

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ ↑e.symm x✝ ∈ K

Tactic:
LinearEquiv.coe_coe

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ e.symm x✝ ∈ K
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
by
  have : S i ≤ iSup S := le_iSup _ _
  tauto

Goal state after: