mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map i (comap f (map f (f.iterateMapComap i n K))) ≤ map i (comap f (map i ((fun K ↦ comap f (map i K))^[n] K)))

Tactic:
by gcongr; exact ih

Goal state after:
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✝ : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x ↦ x ^ (n + 1)) '' s)
⊢ (f x * ↑x) ^ (n + 1) ∈ span {↑x ^ (n + 1)}

Tactic:
mul_pow,

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 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
this : span {↑x ^ (n + 1)} ≤ span ((fun x ↦ x ^ (n + 1)) '' s)
⊢ f x ^ (n + 1) * ↑x ^ (n + 1) ∈ span {↑x ^ (n + 1)}
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
x : α
x✝¹ : M
x✝ : α
⊢ (lcoeFun ∘ₗ lsingle x) x✝¹ x✝ = (LinearMap.single R (fun x ↦ M) x) x✝¹ x✝

Tactic:
simp [single_eq_pi_single]

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

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ioi a

pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
· exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_notMem) hx)

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ici i
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m g = ⊥

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False

Tactic:
replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)

Goal state after:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' f ⁻¹' U

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' (V ∩ W) = f '' (V ∩ W)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ (map Prod.mk f).seq g

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ s.seq t ∈ (map Prod.mk f).seq g
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
⊢ Semigroup α

Tactic:
let mul := e.mul

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
⊢ CommSemigroup α

Tactic:
let mul := e.mul

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

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

Tactic:
let mul := e.mul

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

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

Tactic:
let mul := e.mul

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

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

Tactic:
let mul := e.mul

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

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

Tactic:
let mul := e.mul

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
⊢ Group α
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Preorder α
⊢ atTop.NeBot ↔ Nonempty α ∧ IsDirectedOrder α

Tactic:
by
  refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩
  exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

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

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

Tactic:
let mul := e.mul

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
⊢ ∀ (z : α), (x • y) • z = x • y • z

Tactic:
z

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ (x • y) • z = x • y • z
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ φ r • f x✝¹ = φ r • f x✝

Tactic:
h

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
by
  rw [cof, lift_iInf, le_ciInf_iff']
  simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ¬1 < cof α ↔ ¬NoTopOrder α

Tactic:
not_lt,

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ¬NoTopOrder α
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInacc x
⊢ DirSupInacc (⋃₀ s)

Tactic:
by
  simpa using DirSupInaccOn.sUnion fun x hx ↦ (hs x hx).dirSupInaccOn (D := .univ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp only [Decidable.or_iff_not_not_and_not, not_and, not_le]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : 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
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t

Tactic:
hd₀

Goal state after:
α : 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
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : 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
hds : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s)
hcof : IsCofinalFor (d ∩ t) (d ∩ s)
hcof' : IsCofinalFor d (d ∩ s)
⊢ a ∈ s ∪ t

Tactic:
exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right
    (hcof'.nonempty hd₀) hds (ha.of_isCofinalFor inter_subset_left hcof')

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
⊢ d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
hd₀

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
hS : S.FG
⊢ (span A ↑S).FG

Tactic:
obtain ⟨t, ht⟩ := hS

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R ↑t = S
⊢ (span A ↑S).FG
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : succ (iSup f) < lsub f
⊢ False

Tactic:
heq

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : lsub f < lsub f
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < iSup f

Tactic:
h

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < lsub f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < lsub f
⊢ False

Tactic:
h

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max v u_3}
h : lsub f = 0
i : ι
this : 0 < 0
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.bsup f

Tactic:
h

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < (#α).ord

Tactic:
h

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ ¬n < b ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b

Tactic:
not_lt,

Goal state after:
b n : ℕ
⊢ b ≤ n ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b
Module: Mathlib.Data.Nat.Log

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

Tactic:
not_lt,

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a

Tactic:
exact .inl <| isSuccLimit_sub h.isSuccPrelimit <| lt_add_of_pos_right a h'.pos

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

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
⊢ a ≤ b

Tactic:
by
  rcases h with ⟨b, rfl⟩
  simpa using mul_le_mul_right (one_le_iff_ne_zero.mpr fun h ↦ by simp [h] at b0) a

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

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ ↑0 = 0

Tactic:
Nat.cast_zero

Goal state after:
case inl
m n : ℕ
h : m ≤ n
⊢ 0 = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
· rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
      apply Nat.lt_succ_self

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

Goal state before:
pp: n : ℕ
⊢ ↑n + ω = ω

Tactic:
by
  refine le_antisymm (le_of_forall_lt fun a ha ↦ ?_) le_add_self
  obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha
  obtain ⟨m, rfl⟩ := lt_omega0.1 hb'
  apply hb.trans_lt
  exact_mod_cast natCast_lt_omega0 (n + m)

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

Goal state before:
pp: case cons
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b

Tactic:
exact (H i (IH ab)).trans (h i)

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
a b : Ordinal.{u}
ab : a ≤ b
h : ∀ (i : ι), f i b ≤ b
⊢ nfpFamily f a ≤ b

Tactic:
by
  apply Ordinal.iSup_le fun l ↦ ?_
  induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)

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

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ 0
⊢ c ≤ log b 0

Tactic:
nonpos_iff_eq_zero,

Goal state after:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c = 0
⊢ c ≤ log b 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
· exact log_eq_zero hb

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a < ω ^ succ b ↔ ∃ n, a < ω ^ b * ↑n

Tactic:
refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (opow_mul_lt_opow (natCast_lt_omega0 n) (lt_succ b))⟩

Goal state after:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
⊢ ∃ n, a < ω ^ b * ↑n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b

Tactic:
have := Ordinal.add_sub_cancel_of_le h
    nth_rw 1 [← this]
    rwa [← add_assoc, ← mul_one_add, one_add_omega0]

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

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]
    exact eq_comm

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

Goal state before:
pp: n : ℕ
IH : preOmega ↑n = ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
rw [Nat.cast_lt]

Goal state after:
n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (deriv (fun x ↦ a * x) c)) = a ^ ω * succ c

Tactic:
h

Goal state after:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ¬1 < o.cof ↔ ¬IsSuccLimit o

Tactic:
not_lt,

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof ≤ 1 ↔ ¬IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a < b → preBeth a < preBeth b

Tactic:
h

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < preBeth b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a

Tactic:
rw [add_eq_max ha, max_eq_left hb]

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

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

Tactic:
simpa using lift_lt (a := ℵ_ n)

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

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯

Tactic:
subst H

Goal state after:
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, Uncountable ↑(f ⁻¹' {a})

Tactic:
← Cardinal.aleph0_lt_mk_iff,

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, ℵ₀ < #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : ¬Bounded r s
⊢ (type r).cof ≤ #↑s

Tactic:
not_bounded_iff

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)
  · simp [ha]
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  rcases exists_ord_eq α with ⟨r, wo, hr⟩
  classical
  let := linearOrderOfSTO r
  apply le_antisymm
  · conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · rw [mk_singleton, one_lt_cof_iff]
      exact isSuccLimit_ord h'.aleph0_le
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
⊢ (linearCombination R v') l = (linearCombination R v') l' → l = l'

Tactic:
z

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : (linearCombination R v') l = (linearCombination R v') l'
⊢ l = l'
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
hj : j ∈ ↑s
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
exact Or.inl (Multiset.mem_cons_of_mem hj)

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : i = j
⊢ (f + single i b) j = (single i b + f) j

Tactic:
subst H

Goal state after:
case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
⊢ (f + single i b) i = (single i b + f) i