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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ partialSups (disjointed f) = partialSups f

Tactic:
by
  -- This seems to be much more awkward than the case of linear orders, because the supremum
  -- in the definition of `disjointed` can involve multiple "paths" through the poset.
  classical
  -- We argue by induction on the size of `Iio i`.
  suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
  intro r i hi
  induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.
    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons,
      sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`
    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
    -- Key claim: we can write `Iio i` as a union of (finitely many) `Iic` intervals.
    have hun : (Iio i).biUnion Iic = Iio i := by
      ext r; simpa using ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
    -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
    -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
    -- can rewrite via the induction hypothesis.
    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
⊢ pred^[n.succ] i0 = pred^[0] i0

Tactic:
rwa [Function.iterate_zero, id]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
disjointed_apply

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f ⊔ f i = f (succ i)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ (partialSups f) i ⊔ f i = f (succ i)

Tactic:
hf.partialSups_eq,

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
h : ¬IsMax i
this : Iio (succ i) = Iic i
⊢ f (succ i) \ f i ⊔ f i = f (succ i)
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ ↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) =
    (n + 1, 0) ::ₘ ↑(List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n))

Tactic:
cons_coe

Goal state after:
n : ℕ
⊢ ↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n)) =
    ↑((n + 1, 0) :: List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ 4 ^ n = (1 + 1) ^ (2 * n)

Tactic:
by simp [pow_mul]

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

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

Tactic:
by_cases h : n = 0

Goal state after:
case pos
n : ℕ
h : n = 0
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * 2 ^ (n - 1)

case neg
n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * 2 ^ (n - 1)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝) * n.choose x✝ + x✝ * n.choose x✝ = n * n.choose x✝

Tactic:
← add_mul,

Goal state after:
case a
n : ℕ
h : ¬n = 0
x✝ : ℕ
h' : x✝ ∈ range (n + 1)
⊢ (n - x✝ + x✝) * n.choose x✝ = n * n.choose x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
y : S
⊢ ∃ a, (lift I f H) a = y

Tactic:
obtain ⟨x, rfl⟩ := hf y

Goal state after:
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ ∃ a, (lift I f H) a = f x
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
n k : ℕ
⊢ ∑ i ∈ range (n + 1), (k + 1).multichoose i = (n + (k + 1)).choose (k + 1)

Tactic:
grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]

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

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

Tactic:
have : Nontrivial (R ⧸ I) := ⟨H.2.1⟩

Goal state after:
case refine_1
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : (∑ i ∈ f.support, f i * ↑i) ^ (f.support.card * n + 1) ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
hf,

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ^ (f.support.card * n + 1) ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero
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
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ f.iterateMapComap i 0 K = f.iterateMapComap i (0 + 1) K

Tactic:
contrapose! heq
    induction m with
    | zero => exact heq
    | succ m ih =>
      rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))

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

Goal state before:
pp: case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ ∑ ij ∈ antidiagonal (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
Nat.sum_antidiagonal_succ,

Goal state after:
case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ (d + (0, n + 1).2).choose d + ∑ p ∈ antidiagonal n, (d + (p.1 + 1, p.2).2).choose d = (d + (n + 1) + 1).choose (d + 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ f x i ∈ I

Tactic:
classical
    cases nonempty_fintype ι
    rw [pi_eq_sum_univ x]
    simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
    exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) x).1 = x 0

Tactic:
coe_lsum,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (x.sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M)).1 = x 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) x).2 =
    f (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) ((comapDomain.addMonoidHom ⋯) x))

Tactic:
coe_lsum,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (x.sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M)).2 =
    f (((comapDomain.addMonoidHom ⋯) x).sum fun i ↦ ⇑(((inr R P M ∘ₗ f) ^ i) ∘ₗ inl R P M))
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filter = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, p i.1 i.2 ∧ s i.1 i.2 ⊆ t

Tactic:
rw [mem_iInf_of_directed h, Prod.exists]

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p (a, b).1 (a, b).2 ∧ s (a, b).1 (a, b).2 ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s

Tactic:
by
  simp_rw [mem_kernMap_iff_compl, compl_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' (s₁ ∩ s₂) ⊆ t

Tactic:
image_subset_iff,

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ s₁ ∩ s₂ ⊆ m ⁻¹' t
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LE β
l : Filter α
f f' g g' : α → β
H✝ : f ≤ᶠ[l] g
hf✝ : f =ᶠ[l] f'
hg✝ : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
⊢ f' x ≤ g' x

Tactic:
hf,

Goal state after:
α : Type u
β : Type v
inst✝ : LE β
l : Filter α
f f' g g' : α → β
H✝ : f ≤ᶠ[l] g
hf✝ : f =ᶠ[l] f'
hg✝ : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f' x ≤ g x
⊢ f' x ≤ g' x
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

Tactic:
simp only [frequently_atTop'] at h

Goal state after:
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b > a, P n b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeInf α
f g : β → α
F : Filter β
hf : Tendsto f F atTop
hg : Tendsto g F atTop
⊢ Tendsto (fun x ↦ f x ⊓ g x) F atTop

Tactic:
by
  rw [Filter.tendsto_atTop] at *
  simp [eventually_and, hf, hg]

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
obtain ⟨n, f, h⟩ := fg_iff_exists_fin_generating_family.mp hN

Goal state after:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
⊢ ∃ y ∈ f '' s, a ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := hs b

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
c : α
hc : c ∈ s
hc' : b ≤ c
⊢ ∃ y ∈ f '' s, a ≤ y
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
h₁ : 0.2 < _b.2
⊢ _a₁ ≤ _a₂

Tactic:
exact le_of_smul_le_smul_right h.2 h₁

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 < _b₂.1
h₂ : _b₁.2 ≤ _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
exact .inl ⟨smul_lt_smul_of_pos_left h₁ ha, smul_le_smul_of_nonneg_left h₂ ha.le⟩

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α] (hDL : IsLowerSet D) (hs : DirSupClosedOn D s)
    (ht : DirSupClosedOn D t) ⦃d : Set α⦄ (hD : d ∈ D) (hdu : d ⊆ s ∪ t) (hd₀ : d.Nonempty)
    (hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d) ⦃a : α⦄ (ha : IsLUB d a) (hdst : d ∩ s ∪ d ∩ t = d),
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ a ∈ s ∪ t

Tactic:
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

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
⊢ a < b → f a < f b

Tactic:
induction b using SuccOrder.limitRecOn with
  | isMin b hb => exact hb.not_lt.elim
  | succ b hb IH =>
    intro hab
    obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
    · exact hs a
    · exact (IH h).trans (hs b)
  | isSuccLimit b hb IH =>
    intro hab
    have hab' := hb.succ_lt hab
    exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le
      ((hl hb).1 (mem_image_of_mem _ hab'))

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

Goal state before:
pp: ⊢ ∀ (b : Ordinal.{max (u + 1) v}), b ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ b < univ.{u, v}

Tactic:
refine fun b => inductionOn b ?_; intro β s _
    rw [univ, ← lift_umax]; constructor <;> intro h
    · obtain ⟨a, e⟩ := h
      rw [← e]
      refine inductionOn a ?_
      intro α r _
      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩
    · rw [← lift_id (type s)] at h ⊢
      obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h
      obtain ⟨f, a, hf⟩ := f
      exists a
      induction a using inductionOn with | type α r
      refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
      · exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩
      · refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h
      · intro a'
        obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
        exists b
        simp only [RelEmbedding.ofMonotone_coe]
        simp [e]

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

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≼i s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≼i s)
f : r ≼i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ :
  isEquivalent
    { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
      r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
    { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α, r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r,
      wo := ⋯ }
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≃r s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ }

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≺i s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)

Tactic:
refine fun ⟨f⟩ ↦ ⟨?_⟩

Goal state after:
case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≺i s)
f : r ≺i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1

Tactic:
apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Goal state after:
case inl
a c : Ordinal.{u_4}
⊢ a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r

case inr
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
nth_rw 2 [← Fintype.card_fin x]

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

Goal state before:
pp: case not_isMin
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsMin c.ord

Tactic:
simpa using (aleph0_pos.trans_le hc).ne'

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

Goal state before:
pp: case inl
⊢ log 0 0 = 0

Tactic:
exact log_zero_left 0

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

Goal state before:
pp: case a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ y ≤ log b x

Tactic:
rwa [← opow_le_iff_le_log hb hx]

Goal state after: