mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ (f a)⁻¹ * f x✝ = 1

Tactic:
inv_mul_eq_one,

Goal state after:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ f a = f x✝
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
rw [← zsmul_eq_mul, mk_zsmul N a n]

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

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm (w * y)
fb : b = f.symm (x * z)
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
map_mul

Goal state after:
case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ i, f i) ⊔ a = ⨆ i, f i ⊔ a

Tactic:
refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ ⨆ i, f i ≤ ⨆ i, f i ⊔ a

case refine_2
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ≤ ⨆ i, f i ⊔ a
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨆ i, f i) = ⨆ i, g (f i)

Tactic:
by
  obtain ⟨j, hj⟩ : ∃ j, f j = ⨆ i, f i := exists_eq_ciSup_of_finite
  rw [← hj]
  exact le_antisymm (le_ciSup_of_le j le_rfl) <|
    ciSup_le fun i ↦ hg (hs i) (hs j) (hj ▸ le_ciSup f i)

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i a✝ : ι
⊢ a✝ ≤ Order.succ i → a✝ ≤ i ∨ a✝ = Order.succ i

Tactic:
exact fun h ↦ (Order.le_succ_iff_eq_or_le.mp h).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Unique M₂
⊢ ∀ (c : R) (x : M × M₂), AddEquiv.prodUnique (c • x) = c • AddEquiv.prodUnique x

Tactic:
simp [AddEquiv.prodUnique]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ False

Tactic:
have h_glb : IsGLB (Finset.Ioc i j : Set ι) i := by
    rw [Finset.coe_Ioc]
    have h := succFn_spec i
    rw [h_succFn_eq] at h
    exact isGLB_Ioc_of_isGLB_Ioi hij_lt h

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
have ha : a ∉ Ico (a + 1) b := by simp

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMonoid A
inst✝ : HasMulAntidiagonal A
n : A
x✝ : A × A
a b : A
⊢ (a, b) ∈ map (Equiv.prodComm A A).toEmbedding (mulAntidiagonal n) ↔ (a, b) ∈ mulAntidiagonal n

Tactic:
by simp [mul_comm]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : succ^[↑n] ⊥ = ⊤
⊢ ↑n ≤ (toZ ⊥ ⊤).toNat

Tactic:
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)

Goal state after:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
| ∏ p ∈ map { toFun := Prod.swap, inj' := ⋯ } (antidiagonal n), f p.swap

Tactic:
Finset.prod_map

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
| ∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
β : Type v
F : Type w
R : Type ?u.7
M : Type ?u.9
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m m' : M
⊢ 0 ∈ {r | r • m = r • m'}

Tactic:
simp_rw [Set.mem_ofPred, zero_smul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
x✝ y✝ : α
h : x✝ * y✝ ∈ ⊥
⊢ x✝ * y✝ = 0

Tactic:
by simpa only [Submodule.mem_bot] using h

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0

Tactic:
mul_zero

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ 0 = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ m ∈ range (n + 1 + 1), t (n + 1) m

Tactic:
rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), x * t n i + ∑ i ∈ range (n + 1), y * t n i =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ x_1 ∈ range n.succ, ↑(n.choose x_1) * (x ^ x_1 * y ^ (n - x_1))

Tactic:
cast_comm,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ x_1 ∈ range n.succ, x ^ x_1 * y ^ (n - x_1) * ↑(n.choose x_1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ∃ I ∈ s, x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
obtain ⟨I, hI, hI'⟩ := hx

Goal state after:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
⊢ y ∈ I

Tactic:
let J : Ideal α := Submodule.span α (insert x ↑I)
      have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
      have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
      obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
      specialize oJ J x IJ hx xJ
      rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
      obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
      rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
      refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)
      rwa [Submodule.span_eq] at h

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

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∀ c ∈ Finset.range (k + 1), ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I

Tactic:
intro c

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
⊢ c ∈ Finset.range (k + 1) → ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0

Tactic:
rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

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

Goal state before:
pp: case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
⊢ ∀ c ∈ Finset.range ((s.card + 1) * n + 1 + 1),
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
      span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)

Tactic:
intro c

Goal state after:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
⊢ c ∈ Finset.range ((s.card + 1) * n + 1 + 1) →
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
      span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ (mk I) (x - y) = 0

Tactic:
map_sub,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ (mk I) x - (mk I) y = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ 2 * ∑ i ∈ range (n + 1), i * n.choose i =
    ∑ i ∈ range (n + 1), (n - i) * n.choose (n - i) + ∑ i ∈ range (n + 1), i * n.choose i

Tactic:
by
      rw [two_mul, ← sum_flip]

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

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' ∅)

Tactic:
rw [Set.image_empty, hs]
      trivial

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, (∃ i_1, p i_1 ∧ s i_1 = i) ∧ id i ⊆ x✝

Tactic:
by simp [h.mem_iff]

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

Goal state before:
pp: case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
this : u = (u ∪ s) ∩ (u ∪ t)
⊢ p ((u ∪ s) ∩ (u ∪ t))

Tactic:
exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∃ᶠ (x : α) in atTop, p x
a : α
⊢ ∃ b, a ≤ b ∧ p b

Tactic:
rw [Filter.Frequently] at h

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
⊢ ∃ b, a ≤ b ∧ p b
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
⊢ Disjoint atBot atTop

Tactic:
by
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  by_cases hle : x ≤ y
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
    exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge
  · refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

Tactic:
by
  simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
    (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i : ι
hi : p i
h : sa i ×ˢ sb i ⊆ t
⊢ ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t

Tactic:
exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
M : Type u_3
inst✝ : SMul M α
m : M
x : Shrink.{v, u_2} α
⊢ (equivShrink α).symm (m • x) = m • (equivShrink α).symm x

Tactic:
simp [Equiv.smul_def]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
M : Type u_3
inst✝ : SMul M α
m : M
x : α
⊢ (equivShrink α) (m • x) = m • (equivShrink α) x

Tactic:
simp [Equiv.smul_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (b : α), 1 • b = b

Tactic:
simp [Equiv.smul_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (a : A), a • 0 = 0

Tactic:
simp [Equiv.smul_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (a : A) (x y : α), a • (x + y) = a • x + a • y

Tactic:
simp [Equiv.smul_def]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (x : α), 0 • x = 0

Tactic:
simp [Equiv.smul_def]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ (∀ ⦃d : Set α⦄, d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    DirSupInaccOn D s

Tactic:
DirSupInaccOn,

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ (∀ ⦃d : Set α⦄, d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupClosed x
⊢ DirSupClosed (⋂₀ s)

Tactic:
simpa using DirSupClosedOn.sInter fun x hx ↦ (hs x hx).dirSupClosedOn (D := .univ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
← sub_pos,

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < a₂ • _b - a₁ • _b
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∪ t)

Tactic:
by
  intro d hD hdu hd₀ hd₁ a ha
  have hdst : d ∩ s ∪ d ∩ t = d := by grind
  wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
  · rw [union_comm] at hdu hdst ⊢
    exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
      (directedOn_union_iff.mp (by rwa [hdst])).resolve_right h
  obtain ⟨hds, hcof⟩ := h
  have hcof' : IsCofinalFor d (d ∩ s) := hcof.union_right.mono_left hdst.ge
  exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right
    (hcof'.nonempty hd₀) hds (ha.of_isCofinalFor inter_subset_left hcof')

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
⊢ IsCofinalFor t (t \ s)

Tactic:
grind [IsCofinalFor, not_subset]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
⊢ ∀ a' < a, f a' ≤ b

Tactic:
intro c

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
⊢ c < a → f c ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r ((enum r) ⟨(typein r).toRelEmbedding x, ⋯⟩) ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d

Tactic:
constructor <;> rintro ⟨d, hd, ha⟩

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ ∃ d < c, a < b + d

case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a < b + d
⊢ ∃ d < c, a ≤ b + d
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ ∀ b_1 < succ b, enumOrd s b_1 < a

Tactic:
intro c

Goal state after:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
⊢ c < succ b → enumOrd s c < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * 0)

Tactic:
mul_zero

Goal state after:
case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 = a * 0

Tactic:
mul_zero

Goal state after:
a : Ordinal.{u_4}
⊢ 0 = 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case e'_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
a✝ : Ordinal.{u}
⊢ (∀ (h : a✝ < o), f a✝ h < a) ↔ ∀ (h : a✝ < o), succ (f a✝ h) ≤ a

Tactic:
simp_rw [succ_le_iff]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
⊢ 0 = 0 ^ b * 0

Tactic:
mul_zero

Goal state after:
case inl
b : Ordinal.{u_1}
⊢ 0 = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a = 1 ∨ b = 0 → a ^ b = 1

Tactic:
by simp +contextual [or_imp]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 = 0 ^ b * 0

pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0

Tactic:
mul_zero

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 = 0

case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ n, o = ↑n

Tactic:
by
  simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z

Tactic:
by rw [clog_le_iff_le_pow hb, Nat.pow_le_pow_iff_right hb]

Goal state after: