mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n

Tactic:
cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Submonoid M
⊢ ↑s * ↑s = ↑s

Tactic:
by
  simp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹

Tactic:
apply le_antisymm
  · rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
    exact subset_closure
  · rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
    exact subset_closure

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (f (g 0)).tail.length < (f (g 0)).length

Tactic:
List.length_tail,

Goal state after:
case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (f (g 0)).length - 1 < (f (g 0)).length
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (b : G), 1 • b = b

Tactic:
simp [smul_def]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (r : ConjAct G), r • 1 = 1

Tactic:
simp [smul_def]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (r : ConjAct G) (x y : G), r • (x * y) = r • x * r • y

Tactic:
simp [smul_def]

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

Goal state before:
pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y ∈ ↑A

Tactic:
suffices y * z * z⁻¹ ∈ A by simpa

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y * z * z⁻¹ ∈ A
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (s.noncommProd f comm)

Tactic:
refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ p b
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore ↔ g ∈ ⨅ g, g • H

Tactic:
simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ { carrier := {a | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ } ↔
    ∀ (i : ConjAct G), i⁻¹ • g ∈ H
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

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

Tactic:
by rintro ⟨n, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
Quot.eq

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ (L₁✝ ++ L₂✝))

Tactic:
← List.append_assoc

Goal state after:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹

Tactic:
by
      simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]

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

Goal state before:
pp: case hc
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ p a

Tactic:
simpa using (mem_filter.1 h).2

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
c : Con G
a✝ b✝ : G
hx : a✝ ∈ {x | c x 1}
hy : b✝ ∈ {x | c x 1}
⊢ a✝ * b✝ ∈ {x | c x 1}

Tactic:
by simpa using c.mul hx hy

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs✝ : s ∈ ⊥
hs : s = 1
⊢ ↑⟨s, hs✝⟩ * x✝ = x✝ * ↑⟨s, hs✝⟩

Tactic:
simp [hs]

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.toRingHom.comp e.symm.toRingHom = RingHom.id S

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toRingHom.comp e.toRingHom = RingHom.id R

Tactic:
by
  simp

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

Goal state before:
pp: M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
⊢ Bijective ⇑f

Tactic:
by
    refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩
    · have ⟨c, eq⟩ := h.exists_of_eq eq
      exact mul_left_cancel eq
    · have ⟨x, eq⟩ := h.surj m
      use x.1 / x.2
      rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]

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

Goal state before:
pp: R : Type u_1
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
r : R
x : X
⊢ r • (x /ₒ 1) = r • x /ₒ 1

Tactic:
rw [← smul_one_oreDiv_one_smul, smul_div_one, smul_assoc, one_smul]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
| succ n ihn =>

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Goal state after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₁ a₂ b₁ b₂ : WithTop α
ha : a₁ < a₂
hb : b₁ < b₂
this : MulPosStrictMono α
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) < y (n + 1)

Tactic:
| succ n ihn =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b

Tactic:
refine ⟨?_, exists_succ_iterate_of_le⟩
  rintro ⟨n, rfl⟩
  exact id_le_iterate_of_id_le le_succ n a

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ b < succ a ↔ b ≤ a

Tactic:
contrapose!
  exact succ_le_iff_of_not_isMax' hb

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
⊢ insert b (Iio b) ∩ Ici a = insert b (Iio b ∩ Ici a)

Tactic:
insert_inter_of_mem (mem_Ici.2 h₁)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ f i = ∏ x ∈ s ∩ {i}, f x

Tactic:
simp [hs]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
⊢ (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

Tactic:
split_ifs with h
  · obtain ⟨i, hi, hpi⟩ := h
    rw [prod_eq_single_of_mem _ hi, if_pos hpi]
    exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi
  · push Not at h
    rw [prod_eq_one]
    exact fun i hi => if_neg (h i hi)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
by
  simp

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

Goal state before:
pp: case succ
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
ihn : Countable (Fin n → ℕ)
⊢ Countable (Fin (n + 1) → ℕ)

Tactic:
| succ n ihn =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Countable
this : Countable ↑s
t : Finset ↑s
ht : (Subtype.val '' ↑t).Finite
⊢ Subtype.val '' ↑t ∈ range fun t ↦ Subtype.val '' ↑t

Tactic:
exact mem_range_self _

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c (g (f a))
⊢ c ∈ Set.range (⇑g ∘ ⇑f)

Tactic:
rcases g.2 _ _ h with ⟨b, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t (g.toRelEmbedding b) (g (f a))
⊢ g.toRelEmbedding b ∈ Set.range (⇑g ∘ ⇑f)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).2 ≤ (p₁, p₂).2

Tactic:
rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]

Goal state after:
case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).2 ∈ {x | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x}
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type u_4
x : Part α✝
y : Part β✝
⊢ (x *> y).Dom ↔ (const α✝ id <$> x <*> y).Dom

Tactic:
by simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, (· <$> ·)]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsAdmissible x f {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
apply IsAdmissible.mk
    · constructor
      · constructor
        · exact (bot_isAdmissible le_map).base_isLeast.1
        · exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)
      · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1
    · rintro _ ⟨z, ⟨hz, (hzy | hyz)⟩, rfl⟩ <;>
        refine ⟨map_mem_bot le_map hz, ?_⟩
      · rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
        · left; exact hy.map_le_of_mem_of_lt hz hzy
        · right; exact le_refl _
      · right; exact le_trans hyz (le_map z)
    · intro c hc
      refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩
      · by_cases! h : ∀ z ∈ c, z ≤ y
        · left; apply cSup_le c y h
        · rcases h with ⟨z, hz, hzy⟩
          have h' := Or.resolve_left (hc hz).2 hzy
          right
          apply le_trans h' (le_cSup _ _ hz)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ (g '' (f '' s)ᶜ)ᶜ = sᶜᶜ

Tactic:
simp [hs]

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

Goal state before:
pp: α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ ↑(n + 1) = c ^ ↑n * c

Tactic:
rw [cast_succ, power_add, power_one]

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

Goal state before:
pp: case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ∃ x, ¬∃ a, f a = x
⊢ #α + 1 ≤ #β

Tactic:
obtain ⟨b, hb⟩ := hf

Goal state after:
case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ #α + 1 ≤ #β
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c

Tactic:
by
  simpa using lift_le (a := ℵ₀)

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

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x = ↑m ↔ x = ↑m

Tactic:
by
  rw [← lift_ofENat.{u, v}, lift_inj]

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

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m = lift.{u, v} x ↔ ↑m = x

Tactic:
by
  rw [← lift_ofENat.{u, v}, lift_inj]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]

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

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none * ∏ i, f (some i))

Tactic:
lift_mul,

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * lift.{u, v} (∏ i, f (some i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ #(Finset α) = 2 ^ Fintype.card α

Tactic:
by
  simp

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

Goal state before:
pp: n : ℕ
⊢ ↑n.succ = succ ↑n

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
x : α
⊢ Nontrivial α ↔ ∃ y, y ≠ x

Tactic:
nontrivial_iff_exists_ne x

Goal state after:
α : Type u
x : α
⊢ (∃ y, y ≠ x) ↔ ∃ y, y ≠ x
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
a a' : α
⊢ mn • (a + a') = mn • a + mn • a'

Tactic:
by change mn.1 • mn.2 • _ = (_ : α); rw [smul_add, smul_add]; rfl

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ 0 ∈ s

Tactic:
simp [hs]

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
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

Tactic:
let := Classical.decEq ι

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ (g⁻¹ * ↑h) • g • a = a

Tactic:
smul_smul

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints (↥H) α
h : ↥H
⊢ (g⁻¹ * ↑h * g) • a = a
Module: Mathlib.Algebra.Module.Submodule.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ ((G ^ k) ∘ₗ N.subtype) m = 0

Tactic:
hG,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ (0 ∘ₗ N.subtype) m = 0
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 σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm x) = ↑x

Tactic:
rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬↑u = -↑u

Tactic:
eq_neg_iff_add_eq_zero,

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ ¬↑u + ↑u = 0
Module: Mathlib.Algebra.Ring.Subsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
x✝ : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄, (subtype s) x✝ = (subtype s) a₂ → x✝ = a₂

Tactic:
by
  simp

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Defs

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : NonUnitalSubring R
x : ↥s
⊢ ↑x = 0 ↔ x = 0

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑(n + 1) * (x✝¹ * x✝) = ↑(n + 1) * x✝¹ * x✝

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑(n + 1) = x✝¹ * (x✝ * ↑(n + 1))

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective ⇑f
S : Subsemigroup N
x : N
h : x ∈ S
y : M
hy : f y = x
⊢ y ∈ comap f S ∧ f y = x

Tactic:
simp [hy, h]

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x : E
⊢ ∃ a, (algebraMap F E) a = x

Tactic:
by
  obtain ⟨x, rfl⟩ := hb x
  obtain ⟨y, hy⟩ := hb (b 1 * b 1)
  refine ⟨x * y, ?_⟩
  obtain ⟨z, hz⟩ := hb 1
  apply_fun (x • z • ·) at hy
  rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy

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

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
simp only [Submonoid.mem_map]

Goal state after:
case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ ∃ x ∈ algebraMapSubmonoid A M, f x = (algebraMap R B) r
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f t

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩

Goal state after:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
⊢ x ≠ 0