mathlib-initiative/mathlib-tactics huggingface dataset:
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑(1 * ((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹) = z

Tactic:
Units.val_mul,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑1 * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z
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:
rw [← mul_mk'_one_eq_mk', map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]

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 : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑(fS s * (fS s)⁻¹) * f r))

Tactic:
Units.val_mul,

Goal state after:
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 : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑(fS s) * ↑(fS s)⁻¹ * f r))
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = ↑(fS sa * fS s₁) * (↑(fS s₁)⁻¹ * f r₁ * (↑(fS s₂)⁻¹ * f r₂))

Tactic:
Units.val_mul,

Goal state after:
case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = ↑(fS sa) * ↑(fS s₁) * (↑(fS s₁)⁻¹ * f r₁ * (↑(fS s₂)⁻¹ * f r₂))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ⊤

Tactic:
simp [← coe_mul, top_mul h₀.ne']

Goal state after:
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
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
⊢ n₁ = n₂

Tactic:
have ⟨ms₂, eq₂⟩ := f.surj n₂

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
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
⊢ n₁ = n₂
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑((fS s)⁻¹ * fS s) * φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
Units.val_mul,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * ↑(fS s) * φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
⊢ a * b * c = a * (b * c)

Tactic:
by
    rcases eq_or_ne a 0 with (rfl | ha); · simp only [zero_mul]
    rcases eq_or_ne b 0 with (rfl | hb); · simp only [zero_mul, mul_zero]
    rcases eq_or_ne c 0 with (rfl | hc); · simp only [mul_zero]
    cases a with | top => simp [hb, hc] | coe a => ?_
    cases b with | top => simp [mul_top ha, top_mul hc] | coe b => ?_
    cases c with
    | top =>
      rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    | coe c => simp only [← coe_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ x < 1 ↔ x = 0

Tactic:
by
  simpa using (one_le_iff_ne_zero (x := x)).not

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : SuccAddOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : NeZero 1
⊢ Set.Iic 1 = {0, 1}

Tactic:
ext; simp [le_one_iff]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iio 2 = {0, 1}

Tactic:
ext; simp [le_one_iff]

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

Goal state before:
pp: n m : ℕ
h : ↑m ≤ ↑n
⊢ (↑m).toNat ≤ n

Tactic:
simpa using 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 : ι
v : π i
j : ι
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s

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

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∉ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∈ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∉ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case bot
m : ℕ
⊢ ⊥ + 1 ≤ ↑m ↔ ⊥ < ↑m

Tactic:
| bot =>

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 t : Finset ι
f : ι → M
⊢ (∏ i ∈ s, if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i

Tactic:
by
  rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]

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 ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a

Tactic:
val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a
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 : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (List.scanl f b v.toList).length = n + 1

Tactic:
List.length_scanl,

Goal state after:
α : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ v.toList.length + 1 = n + 1
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (↑m₁.snd).card = ↑m₂.fst

Tactic:
val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (↑m₁.snd).card = ↑m₂.fst
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ #s ^ #(univ.erase i) = #s ^ (card ι - 1)

Tactic:
card_erase_of_mem (mem_univ _),

Goal state after:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ #s ^ (#univ - 1) = #s ^ (card ι - 1)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd) = ↑m.snd

Tactic:
val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd) = ↑m.snd
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then #s ^ #(univ.erase i) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
card_erase_of_mem (mem_univ _),

Goal state after:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then #s ^ (#univ - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match none with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
exact mem_insert _ _

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

Goal state before:
pp: β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ x ∈ univ, c x = if h : ↑x < n then c ⟨↑x, h⟩ else 1

Tactic:
rintro ⟨i, hi⟩ _

Goal state after:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : ⟨i, hi⟩ ∈ univ
⊢ c ⟨i, hi⟩ = if h : ↑⟨i, hi⟩ < n then c ⟨↑⟨i, hi⟩, h⟩ else 1
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk.mk.mk.h
α : Type u_1
n : ℕ
a : α
val✝² : List α
property✝ : val✝².length = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩
⊢ val✝¹ ≠ val✝

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : inl a < inl c
hb : inl c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ succ x ∈ upperBounds (range fun a ↦ succ ↑a)

Tactic:
by simp +contextual [upperBounds, succ_le_succ, le_of_lt]

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

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0

Tactic:
by
  lift f to ι → Type u using fun _ => trivial
  simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

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 a' : α
h✝ : t (g.toRelEmbedding (f.toRelEmbedding a')) (g (f a))
h : s (f.toRelEmbedding a') (f a)
⊢ g.toRelEmbedding (f.toRelEmbedding a') ∈ Set.range (⇑g ∘ ⇑f)

Tactic:
exact ⟨a', rfl⟩

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)

pp: case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b

Tactic:
· rw [h.toOption]
    rfl

Goal state after:
case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
refine ⟨map_mem_bot le_map hz, ?_⟩

Goal state after:
case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
⊢ f z ≤ y ∨ f y ≤ f z
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : Part α
⊢ x.bind some = x

Tactic:
by
  rw [bind_some_eq_map]
  simp [map_id']

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
refine ⟨map_mem_bot le_map hz, ?_⟩

Goal state after:
case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ≤ y ∨ f y ≤ f z
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a = ωSup c

Tactic:
rw [le_antisymm_iff]

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ insert a (maxChain r)

Tactic:
exact mem_insert _ _

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ {y | IsExtremePt x f y} ⊆ bot x f

Tactic:
exact fun _ h ↦ h.mem_bot

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
a b : ULift.{u, v} (Quotient.out (f i))
h : (fun a ↦ ⟨i, a.down⟩) a = (fun a ↦ ⟨i, a.down⟩) b
⊢ a = b

Tactic:
simpa using h

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

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

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

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

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ ↑(toNat c) ↔ ↑n ≤ ↑(toNat d)
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toENat #α = toENat #β

Tactic:
← toENat_lift,

Goal state after:
α : Type u
β : Type v
e : α ≃ β
⊢ toENat (lift.{?u.17, u} #α) = toENat #β
Module: Mathlib.Algebra.Module.RingHom

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
a b : R
x : M
⊢ (f a + f b) • x = f a • x + f b • x

Tactic:
simp only [← f.map_add, hsmul, add_smul]

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

Goal state before:
pp: α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift.{max v u, v} #(Shrink.{v, max u v} α) = #α

Tactic:
lift_mk_shrink.{max u v, v, 0} α,

Goal state after:
α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift.{v, max u v} #α = #α
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective ⇑(σ₂₃.comp σ₁₂)
⊢ Function.Surjective ⇑σ₁₃

Tactic:
RingHomCompTriple.comp_eq

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective ⇑σ₁₃
⊢ Function.Surjective ⇑σ₁₃
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Tactic:
← small_univ_iff,

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} ↑univ
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
⊢ ∃ s, n = s.card

Tactic:
obtain hα | hα := finite_or_infinite α
  · let hα := Fintype.ofFinite α
    obtain ⟨t, -, rfl⟩ := @Finset.exists_subset_card_eq α .univ n <| by simpa using h
    exact ⟨t, rfl⟩
  · obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n
    exact ⟨s, hs.symm⟩

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

Goal state before:
pp: α β : Type u
s : Set α
t : Set β
⊢ #↑(s ×ˢ t) = #↑s * #↑t

Tactic:
by
  rw [mul_def, mk_congr (Equiv.Set.prod ..)]

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

Goal state before:
pp: case mp
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ t.card = n

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ↑3 ≤ #α

Tactic:
simpa using h

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MulZeroClass (α i)
inst✝ : DecidableEq ι
i : ι
f : (i : ι) → α i
⊢ ∀ (a : (i : ι) → α i), 0 * a = 0

Tactic:
intros; ext; exact zero_mul _

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f ∘ₛₗ ↑e₁₂ = g ∘ₛₗ ↑e₁₂
⊢ f = g

Tactic:
rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
⊢ (fun m ↦ { toFun := fun x ↦ m * x, map_smul' := ⋯ }) ((fun f ↦ f 1) f) = f

Tactic:
ext m; change MulOpposite.op m • f 1 = _; simp [← map_smul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inl M N) = fst✝

Tactic:
ext m a; (conv_rhs => rw [← one_smul N a]); rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' ^ n)
⊢ Surjective ⇑f'

Tactic:
rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))
⊢ Surjective ⇑f'
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂✝ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁✝ : Type u_6
M₂✝ : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₁'
inst✝¹⁶ : Semiring R₂'
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₁'
inst✝¹² : AddCommMonoid M₂'
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : Module R₂ M₂
inst✝⁹ : Module R₁' M₁'
inst✝⁸ : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁵ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁴ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
x : M₁
⊢ ((fun f ↦ (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁) ((fun f ↦ (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm) f)) x = f x

Tactic:
simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]

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✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ x - y ∈ f.ker ↔ f x = f y

Tactic:
by rw [mem_ker, map_sub, sub_eq_zero]

Goal state after: