mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
⊢ ↑(insert b (Icc a (pred b))) = ↑(Icc a b)

Tactic:
by simpa using Set.insert_Icc_pred_right_eq_Icc h

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ ↑(insert a (Ioc a b)) = ↑(Ioc (pred a) b)

Tactic:
by simpa using Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
inst✝² : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u
inst✝³ : Semiring R
ι : Type v
inst✝² : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
val✝ : Fintype ι
⊢ motive' ((i : ι) → M i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type v
inst✝³ : Finite ι
R : Type u_1
inst✝² : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type v
inst✝³ : Finite ι
R : Type u_1
inst✝² : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
val✝ : Fintype ι
⊢ motive' ((i : ι) → M i)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
by rw [he₁₂]

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
⊢ 0 ≤ toZ i0 i

Tactic:
toZ_of_ge hi

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯

Tactic:
by
  apply eq_of_veq
  rw [cons_val, map_val]
  exact Multiset.Nat.antidiagonal_succ'

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + (b * a + b) = 0 + b

Tactic:
← add_left_cancel_iff (a := a),

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a + (a * b + (b * a + b)) = a + (0 + b)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ IsIdempotentElem (b - a)

Tactic:
by
  simp_rw [IsIdempotentElem, sub_mul, mul_sub, hab, hba, ha.eq, hb.eq, sub_self, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - (↑⟨i, hi⟩ + a) ∈ I

Tactic:
sub_add_eq_sub_sub_swap,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - a - ↑⟨i, hi⟩ ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 =
    (∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
      ∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2

Tactic:
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
  have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
  congr 1
  · refine prod_congr rfl fun i hi ↦ ?_
    rw [tsub_add_eq_add_tsub (this _ hi)]
  · refine prod_congr rfl fun i hi ↦ ?_
    rw [choose_symm (this _ hi)]

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)
⊢ (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)

Tactic:
Nat.choose_succ_succ (d + (n + 1)),

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 + (d + n + 1).choose (d + 1) = (d + (n + 1)).choose d + (d + (n + 1)).choose d.succ
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i j : ι
x✝ : ⊥ ≤ j
h : (partialSups f) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) j
⊢ (partialSups f) (Order.succ (Order.succ j)) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) (Order.succ j)

Tactic:
have : (partialSups (f ∘ Order.succ)) (Order.succ j) =
      ((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) := by simp

Goal state after:
ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i j : ι
x✝ : ⊥ ≤ j
h : (partialSups f) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) j
this :
  (partialSups (f ∘ Order.succ)) (Order.succ j) = (partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)
⊢ (partialSups f) (Order.succ (Order.succ j)) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) (Order.succ j)
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:
cases nonempty_fintype ι

Goal state after:
case intro
ι : 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 : ι'
val✝ : Fintype ι
⊢ f x i ∈ I
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
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

Tactic:
by
  classical
  ext x y
  dsimp [splittingOfFunOnFintypeSurjective]
  rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
    (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
  rw [zero_smul]

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

Goal state before:
pp: case a
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
⊢ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Tactic:
simpa using h'

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₂
⊢ t ∈ map m f ⊓ map m g

Tactic:
refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_

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₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
t : Set α
h : InjOn m t
f g : Filter ↑t
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)

Tactic:
replace h : Injective (m ∘ ((↑) : t → α)) := h.injective

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
t : Set α
f g : Filter ↑t
h : Injective (m ∘ Subtype.val)
⊢ map m (map Subtype.val f ⊓ map Subtype.val g) = map m (map Subtype.val f) ⊓ map m (map Subtype.val g)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
la : Filter α
r : α → α → Prop
⊢ (∃ t ∈ la, t ×ˢ t ⊆ {x | (fun x ↦ r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

Tactic:
by simp only [prod_subset_iff, mem_ofPred_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t

Tactic:
rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : pure (m x) = pure (m y)
⊢ x = y

Tactic:
← map_pure,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = pure (m y)
⊢ x = y
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = pure (m y)
⊢ x = y

Tactic:
← map_pure,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ x = y
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:
rw [Filter.tendsto_atTop] at *

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : SemilatticeInf α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a
hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a
Module: Mathlib.RingTheory.Finiteness.Defs

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

Tactic:
rintro ⟨G, _, g, hg⟩

Goal state after:
case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
⊢ N.FG
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFounded fun x1 x2 ↦ x1 > x2

Tactic:
isNoetherian_iff',

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ WellFoundedGT (Submodule R M) ↔ WellFounded fun x1 x2 ↦ x1 > x2
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

Tactic:
isNoetherian_iff',

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ WellFoundedGT (Submodule R M)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ s.Finite

Tactic:
rw [Set.Finite, ← mk_lt_aleph0_iff]

Goal state after:
α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ #↑s < ℵ₀
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Ring α
inst✝⁵ : AddCommGroup β
inst✝⁴ : Module α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsOrderedAddMonoid β
h : ∀ (a : α), 0 ≤ a → ∀ (b : β), 0 ≤ b → 0 ≤ a • b
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
⊢ a₁ ≤ a₂ → a₁ • _b ≤ a₂ • _b

Tactic:
by
    simpa [sub_nonneg, sub_smul] using (h (a₂ - a₁) · _ hb)

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
⊢ s.FG

Tactic:
have ssup : s = u.sup id := by
      suffices u.sup id ≤ s from le_antisymm husup this
      rw [sSup', Finset.sup_id_eq_sSup]
      exact sSup_le_sSup huspan

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
ssup : s = u.sup id
⊢ s.FG
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : 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:
constructor <;> 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

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ (StrictMono fun x ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2

Tactic:
exact ⟨add_right_strictMono, fun _ l _ ↦ (add_le_iff_of_isSuccLimit l).2⟩

Goal state after:
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
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

Tactic:
exact (RelIso.preimage Equiv.ulift r).toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).symm.toInitialSeg)

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False

Tactic:
exact hao.not_ge (Ordinal.iSup_le fun i ↦ le_of_lt_succ <|
    ((Ordinal.le_iSup _ _).lt_of_ne (hf i)).trans_le hoa)

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

Goal state before:
pp: α : 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:
constructor <;> 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

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤
    Cardinal.lift.{(max u v) + 1, max u v} (Cardinal.lift.{v, u} #ι)

Tactic:
Cardinal.lift_lift

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
⊢ type r < type s

pp: case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s

Tactic:
· refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩
    simpa using h (f (Sum.inr PUnit.unit))

Goal state after:
case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.bsup f = o₂.bsup fun a h ↦ f a ⋯

Tactic:
subst ho

Goal state after:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.bsup f = o₁.bsup fun a h ↦ f a ⋯
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsTop x

Tactic:
constructor <;> intro ⟨a, ha⟩

Goal state after:
case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ ∃ x, IsTop x

case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
⊢ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ f ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding default) ⋯ = f 0 ⋯

Tactic:
typein_one_toType

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.blsub f = o₂.blsub fun a h ↦ f a ⋯

Tactic:
subst ho

Goal state after:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.blsub f = o₁.blsub fun a h ↦ f a ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ (a * b + c) / (a * 0) = b / 0

Tactic:
rw [mul_zero, div_zero, div_zero]

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

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))

Tactic:
hc,

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + a ≤ a * (d * succ (b / d))
Module: Mathlib.Data.Nat.Log

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

pp: case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b

Tactic:
exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
    (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]

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

Goal state before:
pp: a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit (a ^ b)

Tactic:
by
  rcases zero_or_succ_or_isSuccLimit b with (e | ⟨b, rfl⟩ | l')
  · exact absurd e hb
  · rw [opow_succ]
    exact isSuccLimit_mul_right (opow_pos _ l.bot_lt) l
  · exact isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

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

Goal state before:
pp: case refine_2
a0 : Ordinal.{u_4}
⊢ IsSuccPrelimit (ω * a0)

Tactic:
exact isSuccPrelimit_mul_left isSuccLimit_omega0

Goal state after: