mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
← Cardinal.toNat_lt_iff_lt_of_lt_aleph0,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) < toNat ↑n
⊢ finrank R M < n

case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < Module.rank R M

Tactic:
← Cardinal.toNat_lt_iff_lt_of_lt_aleph0,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ toNat ↑n < toNat (Module.rank R M)

case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).encard = ↑s.card

Tactic:
Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)

Goal state after:
α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 1 ≤ s.encard ↔ ¬s.encard = 0

Tactic:
Order.one_le_iff_ne_zero

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard ≠ 0 ↔ ¬s.encard = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
s.eq_empty_of_isEmpty

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' ∅).encard ≤ ∅.encard
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 0 < Fintype.card α ↔ Nonempty α

Tactic:
Fintype.card_pos_iff

Goal state after:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nonempty α ↔ Nonempty α
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s

Tactic:
rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_sdiff_eq_ncard s t hs, ← ncard_inter_add_ncard_sdiff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ Subgroup.map (mk' N) M ≤ (map N M (MonoidHom.id G) h).ker

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ ↑M
⊢ (mk' N) x ∈ (map N M (MonoidHom.id G) h).ker
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
⊢ f.ker ≤ span R (⇑f ⁻¹' s)

Tactic:
have hy : y ∈ s := Classical.choose_spec h₀

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ f.ker ≤ span R (⇑f ⁻¹' s)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁷ : Semiring R
S : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ι → M
g : ι → R
⊢ ((piRing R M ι S).symm f) g = ∑ i, g i • f i

Tactic:
simp [piRing, LinearMap.lsum_apply]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M
hx : x ∈ ↑p₁
⊢ (inl R M M₂) x ∈ q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
⊢ map (inr R M M₂) p₂ ≤ q

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
case mp.right
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M₂
hx : x ∈ ↑p₂
⊢ (inr R M M₂) x ∈ q
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f) i = f j

Tactic:
simp only [Finset.mem_Iic] at hj_mem hj_le

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ≤ i
hj_le : ∀ k ≤ i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f) i = f j
Module: Mathlib.Algebra.BigOperators.Intervals

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

Tactic:
Ico_add_one_right_eq_Icc

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ q.1 * p.2 = q.1 * q.2

Tactic:
hq,

Goal state after:
A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ q.1 * p.2 = n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
rcases le_or_gt hι.some i with hi | hi

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i
Module: Mathlib.Algebra.BigOperators.Intervals

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

Tactic:
by
  have : ∀ i < m, i ≤ n := by
    intro i hi
    exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
  rcases lt_or_ge k m with hkm | hkm
  · rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
    refine (prod_image ?_).symm
    simp only [mem_Ico, Set.InjOn, mem_coe]
    rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
    rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
  · have : n + 1 - k ≤ n + 1 - m := by
      rw [tsub_le_tsub_iff_left h]
      exact hkm
    simp only [hkm, Ico_eq_empty_of_le, prod_empty, Ico_eq_empty_of_le this]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a - a * a = 0

Tactic:
sub_eq_zero,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a = a * a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ IsIdempotentElem a ∧ IsIdempotentElem b

Tactic:
simp_rw [IsIdempotentElem]; constructor
  · conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
  · conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

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

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]

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

Goal state before:
pp: case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico k (n + k + 1)

Tactic:
Ico_add_one_right_eq_Icc

Goal state after:
case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Icc k (n + k)
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst✝ : I.IsTwoSided
⊢ (ring I).toAddCommGroup = Submodule.Quotient.addCommGroup I

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
by
  apply exists_right_inv_of_exists_left_inv
  rintro ⟨a⟩ h
  rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
  refine ⟨mk _ b, Quot.sound ?_⟩
  simp only [Submodule.quotientRel_def]
  rw [← eq_sub_iff_add_eq'] at abc
  rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc

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

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

Tactic:
iterateMapComap

Goal state after:
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ (fun K ↦ comap f (map i K))^[n + 1] K
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ generate B.sets ≤ B.filter

Tactic:
intro U U_in

Goal state after:
case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
⊢ U ∈ generate B.sets
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:
Filter.Frequently

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.Defs

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

pp: case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
· refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]

Goal state after:
case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : Preorder α
a b : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
Icc_eq_empty_iff

Goal state after:
α : Type v
inst✝ : Preorder α
a b : α
⊢ ¬a ≤ b ↔ ¬a ≤ b
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (⨆ b, bif b then g₁ else g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
comap_iSup,

Goal state after:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ ⨆ i, comap m (bif i then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ f ≤ comap m (map m g) ↔ f ≤ g

Tactic:
comap_map hm

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
hm : Injective m
⊢ f ≤ g ↔ f ≤ g
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
by
  by_cases p <;> simp [*]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b a, ∀ (b_1 : α), a ≤ b_1 → r b_1 b) ↔ ∃ a, ∀ (b : α), a ≤ b → ∃ b_1, ∀ (a : α), b ≤ a → r a b_1

Tactic:
← exists_comm (α := α)

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ a b, ∀ (b_1 : α), a ≤ b_1 → r b_1 b) ↔ ∃ a, ∀ (b : α), a ≤ b → ∃ b_1, ∀ (a : α), b ≤ a → r a b_1
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : Monoid M
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction M B
⊢ DistribMulAction M A

Tactic:
letI := e.addMonoid
  exact { e.distribSMul M, e.mulAction M with }

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
have H (x : s) : ∃ y : α, x ≤ f y := by simpa using hf' x

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
H : ∀ (x : ↑s), ∃ y, ↑x ≤ f y
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s
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₂
⊢ 0 < (a₂ - a₁) • _b

Tactic:
exact smul_pos (sub_pos.2 ha) hb

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₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), PosSMulStrictMono α (β i)
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : (i : ι) → β i⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
by
    simp_rw [lt_def]
    rintro _a ha _b₁ _b₂ ⟨hb, i, hi⟩
    exact ⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ typeLT o.ToType = 0 ↔ o = 0

Tactic:
type_toType

Goal state after:
o : Ordinal.{u_1}
⊢ o = 0 ↔ o = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ typeLT o.ToType ≠ 0 ↔ o ≠ 0

Tactic:
type_toType

Goal state after:
o : Ordinal.{u_1}
⊢ o ≠ 0 ↔ o ≠ 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ typeLT ↑s ≤ typeLT α

Tactic:
type_le_iff'

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ typeLT ↑s ≤ typeLT ↑t

Tactic:
type_le_iff'

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s t : Set α
h : s ⊆ t
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α ≤ typeLT β.ToType

Tactic:
type_toType

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α ≤ β
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α < typeLT β.ToType

Tactic:
type_toType

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α < β
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.38}
ho : 0 < o
⊢ 0 ∈ Iio (typeLT o.ToType)

Tactic:
type_toType

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.38}
ho : 0 < o
⊢ 0 ∈ Iio o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : 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
⊢ False

Tactic:
suffices ∀ a b, Prod.Lex s r (b, a) (enum _ ⟨_, l⟩) from irrefl _ (this _ _)
  intro a b
  rw [← typein_lt_typein (Prod.Lex s r), typein_enum]
  have := H _ (h.succ_lt (typein_lt_type s b))
  rw [mul_succ] at this
  have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this
  refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this
  · rcases a with ⟨⟨b', a'⟩, h⟩
    by_cases e : b = b'
    · exact .inr ⟨a', by grind [asymm_of s]⟩
    · exact .inl (⟨b', by grind⟩, a')
  · grind [subrel_val, Sum.Lex.sep, asymm_of s]

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + a * d

Tactic:
← mul_add

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
· simp [mod_def, hb]

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

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ (typein LT.lt).toRelEmbedding x = ↑x

Tactic:
← type_Iio_lt,

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ type LT.lt = ↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (typein LT.lt).toRelEmbedding x = ↑↑x

Tactic:
← type_Iio_lt,

Goal state after:
n : ℕ
x : Fin n
⊢ type LT.lt = ↑↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit (typeLT c.ord.ToType)

Tactic:
type_toType

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = x

Tactic:
convert! log_opow_mul hb x zero_ne_one.symm using 1

Goal state after:
case e'_2
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x) = log b (b ^ x * 1)

case e'_3
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x = x + log b 1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
hb : b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o

Tactic:
lt_nfp_iff

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + c = c

Tactic:
by
  rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ∈ Ici ℵ₀ ↔ ℵ₀ ≤ c

Tactic:
mem_Ici

Goal state after:
c : Cardinal.{u_1}
⊢ ℵ₀ ≤ c ↔ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ typeLT ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a}) ≤ type r

Tactic:
type_le_iff'

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r r)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : ↑(Iio o)
⊢ 2 ^ preBeth ↑a ≤ ⨆ x, preBeth ↑x

Tactic:
← preBeth_add_one

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : ↑(Iio o)
⊢ preBeth (↑a + 1) ≤ ⨆ x, preBeth ↑x