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

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : b ∈ ⨅ i ∈ J, (proj i).ker
⊢ b ∈ ⨆ i ∈ ↑I, (single R φ i).range

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at hb

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
⊢ b ∈ ⨆ i ∈ ↑I, (single R φ i).range
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

Tactic:
mapQ_comp,

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ mapQ ?succ.p₂ p (f ^ k) ?succ.hg ∘ₗ p.mapQ ?succ.p₂ f ?succ.hf = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h

case succ.p₂
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ Submodule R M

case succ.hf
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p ≤ comap f ?succ.p₂

case succ.hg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ ?succ.p₂ ≤ comap (f ^ k) p
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
⊢ (p.liftQ f h).ker = ⊥

Tactic:
ker_liftQ,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
⊢ map p.mkQ f.ker = ⊥
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
⊢ Iic (pred b) = Iio b

Tactic:
by
  ext x; rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ (f.prod g).range ≤ f.range.prod g.range

Tactic:
simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp]

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ ∀ ⦃x : M₂ × M₃⦄ (x_1 : M), Function.prod (⇑f) (⇑g) x_1 = x → (∃ y, f y = x.1) ∧ ∃ y, g y = x.2
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
⊢ map (inl R M M₂) p = p.prod ⊥

Tactic:
ext ⟨x, y⟩

Goal state after:
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
x : M
y : M₂
⊢ (x, y) ∈ map (inl R M M₂) p ↔ (x, y) ∈ p.prod ⊥
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₂
q : Submodule R M₂
⊢ map (inr R M M₂) q = ⊥.prod q

Tactic:
ext ⟨x, y⟩

Goal state after:
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₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ map (inr R M M₂) q ↔ (x, y) ∈ ⊥.prod q
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
⊢ comap (fst R M M₂) p = p.prod ⊤

Tactic:
ext ⟨x, y⟩

Goal state after:
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
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤
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₂
q : Submodule R M₂
⊢ comap (snd R M M₂) q = ⊤.prod q

Tactic:
ext ⟨x, y⟩

Goal state after:
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₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a✝ b✝ : M × M₂
ha : a✝.2 = f a✝.1
hb : b✝.2 = f b✝.1
⊢ a✝ + b✝ ∈ {p | p.2 = f p.1}

Tactic:
change _ + _ = f (_ + _)
    rw [map_add, ha, hb]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ (fun x ↦ x + d) (a + c) = a + d + c

Tactic:
add_right_comm

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a ≤ a + c
⊢ (fun x ↦ x + d) (a + c) = a + c + d
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ (fun x ↦ x + d) (a + c) = a + d + c

Tactic:
add_right_comm

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a < a + c
⊢ (fun x ↦ x + d) (a + c) = a + c + d
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
⊢ mulAntidiagonal 1 = {(1, 1)}

Tactic:
ext ⟨x, y⟩

Goal state after:
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
x y : A
⊢ (x, y) ∈ mulAntidiagonal 1 ↔ (x, y) ∈ {(1, 1)}
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ ∏ i ∈ Icc a b, f i.succ / f i.castSucc = f b.succ / f a.castSucc

Tactic:
by
  rw [prod_fin_Icc_eq_prod_nat_Icc]
  convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)
  · simp_all
    grind
  · grind
  · simp only [Order.lt_add_one_iff, is_le', ↓reduceDIte]
    rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ 0 * x✝ ∈ ⊥

Tactic:
zero_mul

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ 0 ∈ ⊥
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ 0 * a = 0

Tactic:
zero_mul

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
rintro ⟨ya, hya, b, hb, rfl⟩
    obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
    exact ⟨a, b, hb, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y + x * z, x} = span {x, y}

Tactic:
span_pair_add_right_mul,

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y, x} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ (mk I) x - (mk I) y = 0

Tactic:
sub_eq_zero

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ (mk I) x = (mk I) y
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case a
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ a ∣ a * (c * d)

Tactic:
· apply dvd_mul_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ ∀ {x y : Set α}, x ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} → x ⊆ y → y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
by
        rintro x y ⟨a, ha, b, hb, rfl⟩ xy
        refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩
        rw [← inter_union_distrib_right, union_eq_self_of_subset_left xy]

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

Goal state before:
pp: α : Type u
f g : Filter α
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Tactic:
by simp_rw [le_def, not_forall, exists_prop]

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

Goal state before:
pp: R : Type u_5
M : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
X : Type u_7
Y : Type u_8
inst✝³ : Finite X
inst✝² : Finite Y
inst✝¹ : DecidableEq X
inst✝ : DecidableEq Y
f : X → Y
x : X
m : M
⊢ (linearMap R M f) (Pi.single x m) = Pi.single (f x) m

Tactic:
apply map_piSingle

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap f (comap g F) = F

Tactic:
rw [comap_comap, hfg.comp_eq_id, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ ∀ {x y : Set β}, x ∈ kernImage m '' f.sets → x ⊆ y → y ∈ kernImage m '' f.sets

Tactic:
by
    rintro _ t ⟨s, hs, rfl⟩ hst
    refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩
    rw [kernImage_union_preimage, union_eq_right.mpr hst]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : ι → Filter α
y : Filter β
⊢ Tendsto f (⨆ i, x i) y ↔ ∀ (i : ι), Tendsto f (x i) y

Tactic:
by simp only [Tendsto, map_iSup, iSup_le_iff]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M

Tactic:
· intro H
    let f : α ↪o Submodule R M := OrderEmbedding.subtype _
    exact OrderEmbedding.wellFoundedLT f.dual

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ map f ⊤

Tactic:
exact map_mono le_top

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

Goal state before:
pp: 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 ↑u ≤ sSup (sp '' ↑s)

Tactic:
exact sSup_le_sSup huspan

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

Goal state before:
pp: case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯)

Tactic:
intro a'

Goal state after:
case mpr.type.refine_3
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
⊢ ∃ a, (RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯) a = a'
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ type r✝ * type s✝ = 0 ↔ type r✝ = 0 ∨ type s✝ = 0

Tactic:
simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b✝ : α
hb✝ : ∀ b < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
⊢ ↑((enum s hs) b) < sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb
      refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩
      simpa

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

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{u_3}
⊢ range (familyOfBFamily' r ho f) = range (familyOfBFamily' r' ho' f)

Tactic:
by simp_rw [range_familyOfBFamily']

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

Goal state before:
pp: case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (0 * b)

Tactic:
zero_mul

Goal state after:
case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit 0
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
simpa using card_eq_nat (n := 0)

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ (c + 1) ↔ log b (n / b) + 1 < c + 1

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
Nat.add_lt_add_iff_right,

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n < b ^ (c + 1) ↔ log b (n / b) < c

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case cons.cons
α : 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)
⊢ ∀ i ∈ b :: bs, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
| cons b bs =>

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

Goal state before:
pp: case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

Tactic:
rw [log_zero_right, log_zero_right]

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]
    · simp
    exact fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩

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

Goal state before:
pp: x : Ordinal.{u_1}
h : 0 ≤ 1
hb : BddAbove ((fun x ↦ 0 ^ x) ⁻¹' Iic x)
a : Ordinal.{u_1}
⊢ a ∈ Ici 1 → a ∈ (fun x ↦ 0 ^ x) ⁻¹' Iic x

Tactic:
simp +contextual [one_le_iff_ne_zero]

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

Goal state before:
pp: b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
by
  obtain hb | hb := le_or_gt b 1
  · rw [← one_le_iff_ne_zero] at hx
    obtain rfl | rfl := le_one_iff.1 hb <;> simpa
  · rw [opow_le_iff_le_log hb hx]

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o

Tactic:
· exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

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

Goal state before:
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 ⟨hx₁, hx₂⟩

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

Goal state before:
pp: case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 * b)

Tactic:
zero_mul

Goal state after:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x ↦ a * x) (a ^ ω * b + c) ≤ a ^ ω * succ b

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone
    · rw [mul_succ]
      gcongr
    · rw [← mul_assoc, ← opow_one_add, one_add_omega0]

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

Goal state before:
pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
· simp_rw [isPrincipal_add_iff_add_self_lt, ← Ordinal.mul_two]
    exact fun a ha ↦ ho ha ho₂

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

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 * b < o

Tactic:
zero_mul

Goal state after:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
by
  apply le_antisymm
  · rw [← h]
    apply self_le_add_left
  rw [← not_lt]; intro hb
  have : a + b < c := add_lt_of_lt hc ha hb
  simp [h] at this

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

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : ∃ n, a = ↑n
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
⊢ b = c

Tactic:
rcases ha with ⟨n, rfl⟩

Goal state after:
case inr
b c : Cardinal.{u_1}
hb : ∃ n, b = ↑n
hc : ∃ n, c = ↑n
n : ℕ
h : ↑n + b = ↑n + c
⊢ b = c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ max a.card b.card

Tactic:
· exact card_opow_le_of_omega0_le_left ha b

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

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o.card.ord

Tactic:
apply isPrincipal_add_ord

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ℵ_ 1).ord.cof

Tactic:
rw [isRegular_aleph_one.cof_ord]

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < ℵ_ 1
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'
x✝ : b i ∈ range v
k : κ
p : v k = b i
⊢ False

Tactic:
by simpa [w] using congr(b.repr $p i)

Goal state after: