mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y default) • x = c • y default • x

Tactic:
rw [← smul_assoc]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]

Goal state after:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inl
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n = 0
⊢ k / m * (m / n) = k / n

Tactic:
simp [hn]

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

Goal state before:
pp: n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]

Tactic:
rw [mul_comm a, mul_comm b, mul_comm n]

Goal state after:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
l : ι →₀ R
hl : Finsupp.single i a ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
hn : ¬a = 0
⊢ i ∈ ↑(Finsupp.single i a).support

Tactic:
simp [hn]

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

Goal state before:
pp: m a b c : ℕ
hmc : m.gcd c = 1
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
by simpa [mul_comm] using h

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

Goal state before:
pp: case left.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ n ∣ n.lcm m

pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

pp: case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ m ∣ n.lcm m

Tactic:
· exact dvd_lcm_left n m

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

case right.refine_2
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ m ∣ n.lcm m
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) = ↑n * n.gcdA m + ↑m * n.gcdB m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)

Tactic:
rw [← sub_eq_iff_eq_add] at this

Goal state after:
case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
⊢ Disjoint (span R (range fun x ↦ v ↑x)) (span R (range fun x ↦ v ↑x))

Tactic:
rwa [← image_eq_range, ← image_eq_range]

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

Goal state before:
pp: α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
aux : {x | x ≠ a} ∪ {a} = univ
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
rwa [encard_singleton, aux, encard_univ] at this

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

Goal state before:
pp: case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x s

Tactic:
← sdiff_union_of_subset h,

Goal state after:
case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t \ s ∪ s = insert x s
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case intro
η : Type u_1
f : η → Type u_2
inst✝⁴ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝³ : SetLike S ((i : η) → f i)
inst✝² : SubmonoidClass S ((i : η) → f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H

Tactic:
exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

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

Goal state before:
pp: case neg
α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
h : a ∉ s
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
rw [ncard_insert_of_notMem h hs, if_neg h]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.ncard < t.ncard

Tactic:
← Nat.cast_lt (α := ℕ∞),

Goal state after:
α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ ↑s.ncard < ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ (s ∪ s₁).ncard = k

Tactic:
ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin,

Goal state after:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ s.ncard + s₁.ncard = k
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
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
⊢ (pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ∘ₗ
      codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ =
    id

Tactic:
simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop]

Goal state after:
case refine_2
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
⊢ (pi fun i ↦ if h : True then proj ⟨↑i, ⋯⟩ else 0) = id
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

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

Tactic:
by
  simpa [succ_eq_add_one] using insert_Ioc_succ_left_eq_Ioc h

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
have := hs.to_subtype
  have := hs'.to_subtype
  simp [sSup_eq_iSup', le_iSup_iff_of_directed hs''.directed_val]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂)
⊢ p₁.prod p₂ ≤ q ↔ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

Tactic:
constructor
  · intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, zero_mem p₂⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨zero_mem p₁, hx⟩
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
    have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
    simpa using add_mem h1' h2'

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

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

Tactic:
cons_val,

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (0, n + 1) ::ₘ
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)).val
Module: Mathlib.Data.Finset.NatAntidiagonal

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

Tactic:
cons_val,

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)).val
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
rw [← h]

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹

Tactic:
rw [← h]

Goal state after:
α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊤

Tactic:
rw [← h]

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
h : ⊥ = ⊤
⊢ 1 ∉ ⊥
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
I : Type u_6
⊢ (mapRange.linearMap f).ker = submodule fun x ↦ f.ker

Tactic:
by
  ext x
  simp [Finsupp.ext_iff]

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

Goal state before:
pp: case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

pp: case inr
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : Nonempty ι
⊢ (iInf f).NeBot

Tactic:
· constructor
    simp [iInf_of_empty f, top_ne_bot]

Goal state after:
case inr
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 ↦ x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : Nonempty ι
⊢ (iInf f).NeBot
Module: Mathlib.Order.Filter.Bases.Basic

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

Tactic:
rcases h_dir hi hj with ⟨k, hk, ki, kj⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
i j : ι
hsub : sa i ×ˢ sb j ⊆ t
hi : p ⟨i, j⟩.fst
hj : p ⟨i, j⟩.snd
k : ι
hk : p k
ki : sa k ⊆ sa ⟨i, j⟩.fst
kj : sb k ⊆ sb ⟨i, j⟩.snd
⊢ ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t
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 : m x = m y
⊢ x = y

Tactic:
← pure_injective.eq_iff,

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 : pure (m x) = pure (m y)
⊢ x = y
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right ha hb

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✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
ha : a < 0
hb : 0 < b
⊢ a • b < 0

Tactic:
simpa only [zero_smul] using smul_lt_smul_of_pos_right 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 : α
ha : 0 < _a
_b₁ _b₂ : (i : ι) → β i
hb : _b₁ ≤ _b₂
i : ι
hi : _b₁ i < _b₂ i
⊢ _a • _b₁ ≤ _a • _b₂ ∧ ∃ i, (_a • _b₁) i < (_a • _b₂) i

Tactic:
exact ⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
⊢ f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x))

Tactic:
refine le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)
  obtain hy | rfl := hy.lt_or_eq
  · rw [lt_csSup_iff h₂ h₁] at hy
    obtain ⟨z, hz, hyz⟩ := hy
    exact (hf.strictMono hyz).le.trans hz
  · rw [mem_preimage, hf.map_sSup h₁ h₂]
    apply (csSup_le_csSup bddAbove_Iic _ (image_preimage_subset ..)).trans
    · rw [csSup_Iic]
    · simpa

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
rw [ord_univ] at this

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
by
  rw [← @type_ne_zero_iff_nonempty o.ToType (· < ·), type_toType]

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

Goal state before:
pp: ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ (⨆ i, f i).ord = ⨆ i, (f i).ord

Tactic:
by
  rw [iSup, iSup, sSup_ord, range_comp']

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ✝ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (type r) (type s)
f : r ≼i s
⊢ ∀ (a b : γ ⊕ α),
    Sum.Lex t r a b → Sum.Lex t s (Sum.recOn a Sum.inl (Sum.inr ∘ ⇑f)) (Sum.recOn b Sum.inl (Sum.inr ∘ ⇑f))

Tactic:
simp [f.map_rel_iff]

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ✝ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : (fun x1 x2 ↦ x1 ≤ x2) (type r) (type s)
f : r ≼i s
⊢ ∀ (a b : α ⊕ γ),
    Sum.Lex r t a b → Sum.Lex s t (Sum.recOn a (Sum.inl ∘ ⇑f) Sum.inr) (Sum.recOn b (Sum.inl ∘ ⇑f) Sum.inr)

Tactic:
simp [f.map_rel_iff]

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

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < lsub f, succ a < lsub f

Tactic:
rw [← h]

Goal state after:
case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
⊢ ∀ a < iSup f, succ a < iSup f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case cons.cons.head
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
⊢ b ≤ a

Tactic:
| head as =>

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

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

Tactic:
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
  · rw [le_antisymm_iff, ← Nat.lt_succ_iff, le_log_iff_pow_le, log_lt_iff_lt_pow,
      and_comm] <;> assumption
  have hm : m ≠ 0 := h.resolve_right hbn
  rw [not_and_or, not_lt, Ne, not_not] at hbn
  rcases hbn with (hb | rfl)
  · obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb <;>
      simp only [log_zero_left, log_one_left] <;> lia
  · simp [@eq_comm _ 0, hm]

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

Goal state before:
pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)

Tactic:
· exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

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

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Tactic:
convert! mul_add_mod_mul hx y z using 1 <;>
    rw [add_zero]

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 = log b n / k

Tactic:
rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ (1 + b) = a * a ^ b

Tactic:
opow_add,

Goal state after:
a b : Ordinal.{u_1}
⊢ a ^ 1 * a ^ b = a * a ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
obtain ho | ho := lt_or_ge o ω
  · exact Or.inl <| lt_omega0.1 ho
  · exact Or.inr ho

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

Goal state before:
pp: case succ
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
x✝ : b < n ∨ b ≥ n
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
cases Nat.lt_or_ge b n with

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

Goal state before:
pp: case inr.inr.inr.add_one
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * c + b) = (a ^ b) ^ (c + 1)

Tactic:
opow_add,

Goal state after:
case inr.inr.inr.add_one
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b * c) = (a ^ b) ^ c
⊢ a ^ (b * c) * a ^ b = (a ^ b) ^ (c + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
⊢ b < nfpFamily f a

Tactic:
let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝¹ : Nonempty ι
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : ∀ (i : ι), f i b < nfpFamily f a
l : List ι
hl : f (Classical.arbitrary ι) b < List.foldr f a l
⊢ b < nfpFamily f a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (n + 1) ≤ clog b (n + 1)

Tactic:
exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

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

Goal state before:
pp: case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)

pp: case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y

Tactic:
· rintro rfl
    use opow_log_le_self b hx, lt_opow_succ_log_self hb x

Goal state after:
case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w

Tactic:
opow_add,

Goal state after:
case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * b ^ log b v ≤ b ^ u * v + w
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
exact Or.inl ho₂

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

Goal state before:
pp: case refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
have := lift_cof_congr_of_strictMono this ?_
    · rw [← Cardinal.lift_inj.{_, max (u + 1) v}, Cardinal.lift_lift.{_, _, v},
        Cardinal.lift_umax.{_, u + 1}, Cardinal.lift_umax.{_, u + 1}, this]
      simp
    · intro ⟨b, hb⟩
      rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb
      obtain ⟨i, hi⟩ := hb
      exact ⟨_, Set.mem_range_self i, hi⟩

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

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 < lift.{v, u} c ↔ ℵ_ 1 < c

Tactic:
simpa using lift_lt (a := ℵ₁)

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

Goal state before:
pp: case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c

Tactic:
rw [← h]

Goal state after:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ a + b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℶ_ ↑n ↔ c ≤ ℶ_ ↑n

Tactic:
by
  simpa using lift_le (b := ℶ_ n)

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

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Tactic:
rintro (⟨h1, h2⟩ | h3)

Goal state after:
case refine_2.inl
a b : Cardinal.{u_1}
h1 : ℵ₀ ≤ a
h2 : b ≤ a
⊢ a + b = a

case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a