mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≠ 0 ↔ s.Nonempty

Tactic:
Ne,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ¬s.ncard = 0 ↔ s.Nonempty
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
⊢ l.length ≤ Nat.card α

Tactic:
by
  have := Fintype.ofFinite α
  grw [h.length_le_card, Fintype.card_eq_nat_card]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ t \ s ≠ ∅

Tactic:
Ne,

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t \ s = ∅
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i

Tactic:
exact hI i hiI

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

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
ι' : Type x'
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M₃
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type ?u.47
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
⊢ (fun f i ↦ f ∘ₗ single R φ i) ((fun f ↦ ∑ i, f i ∘ₗ proj i) f) = f

Tactic:
by
    ext i x
    simp [apply_single]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
⊢ (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) b ∈ ⨅ i ∈ J, (proj i).ker

Tactic:
simp only [mem_iInf, mem_ker, proj_apply, pi_apply]

Goal state after:
case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
⊢ ∀ i ∈ J, (if h : i ∈ I then proj ⟨i, h⟩ else 0) b = 0
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
⊢ ∀ (c : (i : ↑I) → φ ↑i), (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) c ∈ ⨅ i ∈ J, (proj i).ker

Tactic:
intro b
    simp only [mem_iInf, mem_ker, proj_apply, pi_apply]
    intro j hjJ
    have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩
    rw [dif_neg this, zero_apply]

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ Iio (succ b) = Iic b

Tactic:
ext x; rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
convert! (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
    rw [Finset.sup_eq_iSup]
    simp_rw [Set.mem_toFinset]
    rfl

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, f i = ⨆ i, g i

Tactic:
by
  simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]

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
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ False

Tactic:
have hi_mem : i ∈ Finset.Ioc i j := by
    refine Finset.isGLB_mem _ h_glb ?_
    exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩

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
hi_mem : i ∈ Finset.Ioc i j
⊢ False
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
⊢ ∀ {a b : ι}, a ≤ b → ∃ n, succ^[n] a = b

Tactic:
intro i j hij

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (∏ x < a, f x) * f a = ∏ x ≤ a, f x

Tactic:
rw [mul_comm, mul_prod_Iio_eq_prod_Iic]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[(toZ i0 i).toNat] i0 = i

Tactic:
by
  rw [toZ_of_ge hi, Int.toNat_natCast]
  exact Nat.find_spec (exists_succ_iterate_of_le hi)

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
by_cases! h : m ≤ n

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n

Tactic:
rintro ⟨h, rfl⟩

Goal state after:
case mpr
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

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

Tactic:
toZ_iterate_succ_of_not_isMax _ hn_max

Goal state after:
case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (↑↑n).toNat
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (¬I ≠ ⊤ ∨ ¬∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
Ne,

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (¬¬I = ⊤ ∨ ¬∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
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✝ : ℕ
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
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i + n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
cast_add,

Goal state after:
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
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i) + ↑(n.choose i.succ)) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x : α
⊢ span {-x} = span {x}

Tactic:
by
  ext
  simp only [mem_span_singleton']
  exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
Ne,

Goal state after:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ¬M = ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f (((linearEquivFunOnFinite R R α).symm (Pi.single x 1)).sum fun x r ↦ r • ⋯.choose) y = Pi.single x 1 y

Tactic:
linearEquivFunOnFinite_symm_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f ((Finsupp.single x 1).sum fun x r ↦ r • ⋯.choose) y = Pi.single x 1 y
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
⊢ l = ⋯.filter

Tactic:
h.filter_eq

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = l
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : 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
⊢ u = (u ∪ s) ∩ (u ∪ t)

Tactic:
← union_eq_left,

Goal state after:
α : 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 : u ∪ s ∩ t = u
⊢ u = (u ∪ s) ∩ (u ∪ t)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
X : Type u_7
Y : Type u_8
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
s : X → M
y : Y
⊢ (linearMap R M f) s y = {x | f x = y}.sum s

Tactic:
by
  apply map_apply_apply

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
⊢ map g (map f a) ≤ c

Tactic:
rwa [map_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
⊢ map (Sum.elim m₁ m₂) (map inl (comap inl l) ⊔ map inr (comap inr l)) =
    map m₁ (comap inl (map inl (comap inl l) ⊔ map inr (comap inr l))) ⊔
      map m₂ (comap inr (map inl (comap inl l) ⊔ map inr (comap inr l)))

Tactic:
simp [map_sup, map_map, comap_sup, (gc_map_comap _).u_l_u_eq_u]

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

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ l ⊓ 𝓟 {x | p x} ≠ ⊥

Tactic:
Ne,

Goal state after:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ ¬l ⊓ 𝓟 {x | p x} = ⊥
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
by
  refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
  · rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩
    exact map_mono hHF
  · have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) :=
      fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm
    exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
⊢ Group α

Tactic:
let inv := e.Inv

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
⊢ Group α
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
⊢ CommGroup α

Tactic:
let inv := e.Inv

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
⊢ CommGroup α
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
  · rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
    exact ⟨x₀, fun x hx => hx₀ x hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ 0 < a • b ↔ 0 < b

Tactic:
by
  simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ span S (⇑f '' ↑(t.preimage ⇑f ⋯)) = map f N

Tactic:
Finset.coe_preimage,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ span S (⇑f '' ⇑f ⁻¹' ↑t) = map f N
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
h : a₁ • f b ≤ a₂ • f b
⊢ a₁ ≤ a₂

Tactic:
exact le_of_smul_le_smul_right h hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
b : ↑(Iio a)
hb : IsSuccLimit b
c : ↑(Iio (f a))
hc : ∀ b_1 < b, ⟨f ↑b_1, ⋯⟩ ≤ c
⊢ ↑c ∈ upperBounds (f '' Iio ↑b)

Tactic:
simpa [upperBounds] using! fun d hd ↦ hc ⟨d, hd.trans b.2⟩ hd

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

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
⊢ ∀ (α : Type u) (r : α → α → Prop) [inst : IsWellOrder α r],
    liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
intro α r _

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ liftInitialSeg.toRelEmbedding (type r) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
x : α
h : s ⊆ t
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

Tactic:
induction x using WellFoundedLT.induction with | ind x IH

Goal state after:
case ind
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
h : s ⊆ t
x : α
IH : ∀ y < x, ↑((enum t ⋯) y) ≤ ↑((enum s hs) y)
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
x : α
h : s ⊆ t
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

Tactic:
induction x using WellFoundedLT.induction with | ind x IH
  exact enum_le_of_forall_lt (h (Subtype.prop _)) fun y hy ↦
    (IH y hy).trans_lt ((enum s hs).strictMono hy)

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

Goal state before:
pp: o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ sInf (s ∩ {b | ∀ c < o, enumOrd s c < b}) ≤ a

Tactic:
exact csInf_le' ⟨ha, H⟩

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

Goal state before:
pp: case refine_1
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
⊢ { x // s x b } × α ⊕ { x // r x a }

Tactic:
by_cases e : b = b'

Goal state after:
case pos
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ { x // s x b } × α ⊕ { x // r x a }

case neg
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ { x // s x b } × α ⊕ { x // r x a }
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁

Goal state after:
case inr
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ b ^ x ≤ b ^ (log.go y b y).snd
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n ≠ 0 ↔ b ≤ n ∧ 1 < b

Tactic:
Ne,

Goal state after:
b n : ℕ
⊢ ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ ¬n ≠ 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
Ne,

Goal state after:
case inr
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ ¬¬n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
rw [zero_opow']
  exact sub_le_self 1 a

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

Goal state before:
pp: case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = 0

Tactic:
log_of_left_le_one

Goal state after:
case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ 0 = 0

case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = Fintype.card (Fin x)

Tactic:
exact Fintype.card_congr Fin.equivSubtype.symm

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

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

Tactic:
have := hb.ne'

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

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a * ω ≤ b

Tactic:
by
  rw [← add_eq_right_iff_mul_omega0_le]
  exact (isNormal_add_right a).strictMono.le_apply.ge_iff_eq'

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

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'

Tactic:
use x + y, hb hx hy

Goal state after:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * (x + y)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ succ (ℵ_ 0) = ℵ_ 1

Tactic:
succ_aleph,

Goal state after:
⊢ ℵ_ (0 + 1) = ℵ_ 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case limit
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
a✝ : ∀ o' < a, a = o' → a.cof ≤ (f a).cof
⊢ a.cof ≤ (f a).cof

Tactic:
rw [cof_map_of_isNormal hf ha]

Goal state after: