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

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : Subrel r (fun x ↦ x ∈ s) ((Infinite.natEmbedding s hi) m) ((Infinite.natEmbedding s hi) n)
⊢ False

Tactic:
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Goal state after:
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:
(first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

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

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • ↑x * g • y = ↑x * g • y

Tactic:
x.2 g

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

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
h : ⊤ ⊆ S.centralizer
x✝¹ : M
hx : x✝¹ ∈ S
x✝ : M
⊢ x✝ * x✝¹ = x✝¹ * x✝

Tactic:
by rw [h trivial _ hx]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
by
  refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h
  rw [← left_inv a1 h1, ← left_inv a2 h2]
  simp only [eq]

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 0, f k = 1

Tactic:
range_zero,

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ ∅, f k = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, one_mul]

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
s : Finset { x // p x }
f : { x // p x } → M
g : ι → M
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ map (Embedding.subtype fun x ↦ p x) s, g x = ∏ x ∈ s, f x

Tactic:
by
  rw [Finset.prod_map]
  exact Finset.prod_congr rfl h

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤

Tactic:
exact Subgroup.closure_univ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih : ∀ z ∈ P, z ≠ 1 → z ≤ y → ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) y
z : M
hz₁ : z < y
hz₂ : z ∈ P
hz₃ : z ≠ 1
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩

Goal state after:
case neg
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ z * y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
⊢ ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
by
  rw [← sdiff_singleton_eq_erase]
  refine prod_subset sdiff_subset fun x hx hnx => ?_
  grind

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Tactic:
· exact h1 x hx h

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
add_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
add_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
add_bind

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₁ ⊔ H₂

Tactic:
by grind [mul_assoc, mul_mem, mul_mem_sup, inv_mem]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
h : ∀ (f g : F) (x : α), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x
⊢ g x ≤ f x → f x⁻¹ ≤ g x⁻¹

Tactic:
simpa using h g f x⁻¹

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 : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ (∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)) ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

Tactic:
Localization.r_iff_exists

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ (∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)) ↔ ∃ c, ↑c * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑c * (↑(a₁, a₂).2 * (b₁, b₂).1)
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toRingHom✝¹ : α →+* β
monotone'✝¹ : Monotone (↑↑toRingHom✝¹).toFun
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ }
⊢ toRingHom✝¹ = toRingHom✝

Tactic:
exact DFunLike.coe_injective h

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f H = f a b c d

Tactic:
by
  rw [← mk_eq_monoidOf_mk', liftOn₂_mk]

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

Goal state before:
pp: case h
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
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ f (x.1 / ↑x.2) = m

Tactic:
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.Algebra.Order.Ring.WithTop

Goal state before:
pp: case zero.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

Tactic:
simp [pow_succ]

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

Goal state before:
pp: case zero.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

Tactic:
simp [pow_succ]

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

Goal state before:
pp: case succ.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

Tactic:
simp [pow_succ]

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

Goal state before:
pp: case succ.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
a✝ : α
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

Tactic:
simp [pow_succ]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Ici a ∩ Iic (succ b) = insert (succ b) (Ici a ∩ Iic b)

Tactic:
Iic_succ,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Ici a ∩ insert (succ b) (Iic b) = insert (succ b) (Ici a ∩ Iic b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioi a ∩ Iic (succ b) = insert (succ b) (Ioi a ∩ Iic b)

Tactic:
Iic_succ,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ Ioi a ∩ insert (succ b) (Iic b) = insert (succ b) (Ioi a ∩ Iic b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
h : IsMax a
nh : succ ↑a ∈ s
⊢ False

Tactic:
replace h := congr($h.succ_eq.1)

Goal state after:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : ↑(succ a) = ↑a
⊢ False
Module: Mathlib.Data.Countable.Small

Goal state before:
pp: α : Type v
h : ¬Small.{w, v} α
⊢ Uncountable α

Tactic:
by
  rw [uncountable_iff_not_countable]
  exact mt (@Countable.toSmall α) h

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
by
  apply Vector.eq; simp [scanl]

Goal state after:
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
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
      rw [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]
      · intro b hb
        rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
        exact hb.2 hb.1.2.symm
      · exact fun a ha ha' => h <| ha'.symm ▸ ha

Goal state after:
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u1} ↑t
⊢ Small.{u, u1} ↑(s ∪ t)

Tactic:
by
  rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
  infer_instance

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ MapsTo (fun x ↦ f '' x) univ univ

Tactic:
by simp [MapsTo]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝¹ : ChainCompletePartialOrder α
f : α → α
inst✝ : Nonempty α
le_map : ∀ (x : α), x ≤ f x
⊢ (fixedPoints f).Nonempty

Tactic:
let x : α := Classical.ofNonempty
  let y := cSup
    (NonemptyChain.mk (bot x f) ⟨x, (bot_isAdmissible le_map).base_isLeast.1⟩ (bot_isChain le_map))
  use y
  apply le_antisymm (le_cSup _ _ (_ : f y ∈ bot x f)) (le_map y)
  apply (bot_isAdmissible le_map).image_self_subset_self
  use y
  exact ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_refl _), rfl⟩

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

Goal state before:
pp: case refine_1
α β : Type u
a b : Cardinal.{u}
x✝¹ x✝ : Type u
⊢ lift.{v, u} #x✝¹ ≤ lift.{v, u} #x✝ ↔ #x✝¹ ≤ #x✝

Tactic:
rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : α →𝒄 Part β
⊢ (fun x ↦ f <$> g x) = ⇑(g.bind (const (pure ∘ f)))

Tactic:
ext1

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : α →𝒄 Part β
x✝ : α
⊢ f <$> g x✝ = (g.bind (const (pure ∘ f))) x✝
Module: Mathlib.SetTheory.Cardinal.Order

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

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

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

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

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

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

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

Tactic:
rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ i, f i

Tactic:
simpa [← lift_umax] using sum_le_lift_mk_mul_iSup_lift f

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

Goal state before:
pp: ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)

Tactic:
exact ciSup_mono_of_forall_exists' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩

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

Goal state before:
pp: α : Type u
A : Set (Set α)
⊢ #↑(⋃₀ A) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
rw [sUnion_eq_iUnion]
  apply mk_iUnion_le

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r
⊢ P = Q

Tactic:
replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
⊢ P = Q
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ (algebraMap R A) r * a = r • a

Tactic:
Q.smul_def',

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ (algebraMap R A) r * a = (algebraMap R A) r * a
Module: Mathlib.Algebra.GroupWithZero.Prod

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
by simp [Prod.mul_def]

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝¹ : MulZeroClass M₀
inst✝ : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
by simp [Prod.mul_def]

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝ : (i : I) → g i
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝

Tactic:
ext1

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝¹ : (i : I) → g i
x✝ : I
⊢ ((r✝ + s✝) • x✝¹) x✝ = (r✝ • x✝¹ + s✝ • x✝¹) x✝
Module: Mathlib.Algebra.Module.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝ : (i : I) → g i
⊢ 0 • x✝ = 0

Tactic:
ext1

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ (0 • x✝¹) x✝ = 0 x✝
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 ι
  refine s.induction_on ?_ fun i s _ ih ↦ ?_
  · simp
  · rw [Finset.inf_insert, coe_inf, ih]
    simp

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : FunLike F α β
f : α → β
s : Set (Set β)
⊢ ⋂ t ∈ s, f ⁻¹' t = sInf (preimage f '' s)

Tactic:
simp only [Set.sInf_eq_sInter, Set.sInter_image]

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

Goal state before:
pp: R : Type u_2
n : ℕ
inst✝¹ : Semiring R
inst✝ : CharZero R
a : ℕ
hn : n ≠ 0
⊢ ↑a ^ n = 1 ↔ a = 1

Tactic:
simp [← cast_pow, cast_eq_one, hn]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s

Tactic:
subst ha; exact sa.add_mem

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
x : R
⊢ x ∈ ↑⊥ ↔ x = 0

Tactic:
rw [coe_bot, Set.mem_singleton_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ x✝ • (algebraMap R A) 1 = (algebraMap R A) 1

Tactic:
map_one,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ x✝ • 1 = 1
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod :: List.map List.prod tl).sum

Tactic:
List.sum_cons

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod + (List.map List.prod tl).sum)