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

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i✝ : ι ⊕ ι'
hi : i✝ ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
i : ι'
x✝ : i ∈ s.preimage Sum.inr ⋯
⊢ (fun x ↦ g x • v x) (Sum.inr i) ∈ span R (v '' range Sum.inr)

Tactic:
· exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)

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

Goal state before:
pp: case inr.inl.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Finite β
⊢ card (α → β) = card β ^ card α

pp: case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card (α → β) = card β ^ card α

Tactic:
· let := Fintype.ofFinite α
      let := Fintype.ofFinite β
      simp

Goal state after:
case inr.inl.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝¹ : Finite α
h✝ : Infinite β
⊢ card (α → β) = card β ^ card α
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ finrank R M = finrank R N

Tactic:
by
  unfold finrank
  rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ InjOn f s

Tactic:
rw [injOn_iff_invFunOn_image_image_eq_self]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ Function.invFunOn f s '' f '' s = s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y ↦ x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝

Tactic:
exact (leftCoset_eq_iff s).symm

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ b⁻¹ * (f ↑c * ((f ↑c)⁻¹ * c)) ∈ s

Tactic:
mul_inv_cancel_left,

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ b⁻¹ * c ∈ s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a : ↥s
⊢ ∀ (a₂ : ↥s),
    Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a) = Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a₂) →
      Quotient.mk'' a = Quotient.mk'' a₂

Tactic:
b

Goal state after:
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a) = Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' b) →
    Quotient.mk'' a = Quotient.mk'' b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
by
  rw [← ncard_inter_add_ncard_sdiff_eq_ncard s t hs, ← ncard_inter_add_ncard_sdiff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [← encard_eq_four, ncard_def]
  simp

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
by
      simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a : α
⊢ ∀ (b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
b

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
⊢ ∀ (b : α), (∀ (x : β), g x ≠ b) → a = b

Tactic:
b

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
a : α
ha : ∀ (x : β), g x ≠ a
b : α
⊢ (∀ (x : β), g x ≠ b) → a = b
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a : M
⊢ ∀ ⦃y : M⦄, (comap ⇑f ⋯ (conGen rel)) a y → (conGen (rel on ⇑f)) a y

Tactic:
b

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
⊢ (comap ⇑f ⋯ (conGen rel)) a b → (conGen (rel on ⇑f)) a b
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1

Tactic:
apply existsUnique_of_exists_of_unique

Goal state after:
case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (succ a) (succ b) = Ioc a b

Tactic:
Ico_succ_left_eq_Ioo,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (succ b) = Ioc a b
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₂
x : M × M₂
⊢ x ∈ (inl R M M₂).range ↔ x ∈ (snd R M M₂).ker

Tactic:
simp only [mem_ker, mem_range]

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₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) ↔ (snd R M M₂) x = 0
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₂
x : M × M₂
⊢ x ∈ (inr R M M₂).range ↔ x ∈ (fst R M M₂).ker

Tactic:
simp only [mem_ker, mem_range]

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₂
x : M × M₂
⊢ (∃ y, (inr R M M₂) y = x) ↔ (fst R M M₂) x = 0
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
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ map f (comap f (span R₂ s)) ≤ span R₂ (⇑f '' ⇑f ⁻¹' s)

Tactic:
map_comap_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ Set.range ⇑f
hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ f.ker
⊢ f.range ⊓ span R₂ s ≤ span R₂ (⇑f '' ⇑f ⁻¹' s)
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 (Ico (a + 1) b) = Ico a b

Tactic:
by
  simpa [succ_eq_add_one] using insert_Ico_succ_left_eq_Ico h

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case h₂
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₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
· exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : k ∈ lowerBounds (Set.Ioi i) ∧ k ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ k ∈ lowerBounds (Set.Ioc i j) ∧ k ∈ upperBounds (lowerBounds (Set.Ioc i j))

Tactic:
mem_upperBounds,

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : k ∈ lowerBounds (Set.Ioi i) ∧ ∀ x ∈ lowerBounds (Set.Ioi i), x ≤ k
⊢ k ∈ lowerBounds (Set.Ioc i j) ∧ ∀ x ∈ lowerBounds (Set.Ioc i j), x ≤ k
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False

Tactic:
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ (Iic i).sup f \ f i ≤ (Iio i).sup f

Tactic:
simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]

Goal state after:
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
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.1 ≤ n

Tactic:
le_iff_exists_mul

Goal state after:
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ ∃ c, n = kl.1 * c
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
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ kl.2 ≤ n

Tactic:
le_iff_exists_mul

Goal state after:
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ mulAntidiagonal n
⊢ ∃ c, n = kl.2 * c
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (partialSups t) n

Tactic:
rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]

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

Goal state before:
pp: n : ℕ
⊢ map Prod.swap (antidiagonal n) = (antidiagonal n).reverse

Tactic:
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
    range_eq_range', map_map]

Goal state after:
n : ℕ
⊢ map (Prod.swap ∘ fun i ↦ (i, n - i)) (range (n + 1)) =
    map ((fun i ↦ (i, n - i)) ∘ fun x ↦ 0 + (n + 1) - 1 - x) (range (n + 1))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝¹ : Ring R
f : ι → R
inst✝ : (span (range f)).IsTwoSided
i : ι
⊢ (mk (span (range f))) (f i) = 0

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.subset_span ⟨i, rfl⟩

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
⊢ ∀ (x_1 : ι), y ∈ (f x_1).sets → ∃ i, x ∩ y ∈ (f i).sets

Tactic:
b

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
⊢ y ∈ (f b).sets → ∃ i, x ∩ y ∈ (f i).sets
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ ∅ ∈ f ⊓ 𝓟 s ↔ sᶜ ∈ f

Tactic:
mem_inf_principal

Goal state after:
α : Type u
f : Filter α
s : Set α
⊢ {x | x ∈ s → x ∈ ∅} ∈ f ↔ sᶜ ∈ f
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x

Tactic:
simp [imp_iff_not_or]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
⊢ ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Tactic:
V

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
⊢ ∀ B ∈ F, f ⁻¹' B ⊆ V → x ∈ V
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f ⊓ 𝓟 s).NeBot

Tactic:
rw [neBot_inf_comap_iff_map', map_principal, ← frequently_mem_iff_neBot]
  exact Eventually.frequently hs

Goal state after:
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
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
⊢ ∀ x ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0

Tactic:
rintro - ⟨hx, ⟨x, rfl⟩⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : (f ^ m) x ∈ ↑(LinearMap.ker (f ^ n))
⊢ (f ^ m) x = 0
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
⊢ IsSuccPrelimit a

Tactic:
b

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
⊢ ¬b ⋖ a
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
⊢ IsSuccPrelimit (f a)

Tactic:
b

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
⊢ ¬b ⋖ f a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
have H (x : s) : ∃ y : α, x ≤ f y := by simpa using hf' x
    choose g hg using H
    refine (lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift
    obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' (f a)
    obtain ⟨c, hc, hc'⟩ := hs (f b)
    refine ⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩
    rw [← hf.le_iff_le]
    exact hb.trans (hc'.trans (hg ⟨c, hc⟩))

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
hs : IsCofinal s
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
exact (lift_le.2 <| cof_le (hs.image hf.monotone hf')).trans mk_image_le_lift

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a_1 : α⦄, IsLUB d a_1 → a_1 ∈ {a}

Tactic:
b

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
⊢ IsLUB d b → b ∈ {a}
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
hb : b₁ < b₂
⊢ a • b₁ < a • b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
⊢ f c ≤ b

Tactic:
mem_upperBounds,

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ x ∈ f '' s, x ≤ b
⊢ f c ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : b ∈ upperBounds ((fun a ↦ g (f a)) '' Iio a✝)
⊢ (g ∘ f) a✝ ≤ b

Tactic:
mem_upperBounds,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ x ∈ (fun a ↦ g (f a)) '' Iio a✝, x ≤ b
⊢ (g ∘ f) a✝ ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ (StrictMono fun x ↦ ⟨f ↑x, ⋯⟩) ∧
    ∀ (o : ↑(Iio a)), IsSuccLimit o → ∀ (a_2 : ↑(Iio (f a))), (∀ b < o, ⟨f ↑b, ⋯⟩ ≤ a_2) → ⟨f ↑o, ⋯⟩ ≤ a_2

Tactic:
refine ⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
b : ↑(Iio a)
hb : IsSuccLimit b
c : ↑(Iio (f a))
hc : ∀ b_1 < b, ⟨f ↑b_1, ⋯⟩ ≤ c
⊢ ↑c ∈ upperBounds (f '' Iio ↑b)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
obtain ⟨a, e⟩ := h
      rw [← e]
      refine inductionOn a ?_
      intro α r _
      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩

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

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ c = lift.{max (u + 1) v, u} c'

Tactic:
by simp only [e.symm, lift_lift]

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

Goal state before:
pp: ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ sSup (ord '' range fun i ↦ f i) = sSup (range fun i ↦ (f i).ord)

Tactic:
range_comp'

Goal state after:
ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ sSup (ord '' range fun i ↦ f i) = sSup (ord '' range f)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
⊢ ∀ (b : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
b

Goal state after:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: a : Ordinal.{u}
f : ↑(Iio a) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
this : NoMaxOrder ↑(Iio a)
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
exact iSup_add_one hf

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

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).bsup (bfamilyOfFamily' r f) = (type r').bsup (bfamilyOfFamily' r' f)

Tactic:
rw [bsup'_eq_iSup, bsup'_eq_iSup]

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

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
⊢ False

Tactic:
by
  suffices ∀ a b, Prod.Lex s r (b, a) (enum _ ⟨_, l⟩) from irrefl _ (this _ _)
  intro a b
  rw [← typein_lt_typein (Prod.Lex s r), typein_enum]
  have := H _ (h.succ_lt (typein_lt_type s b))
  rw [mul_succ] at this
  have := ((add_lt_add_iff_left _).2 (typein_lt_type _ a)).trans_le this
  refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this
  · rcases a with ⟨⟨b', a'⟩, h⟩
    by_cases e : b = b'
    · exact .inr ⟨a', by grind [asymm_of s]⟩
    · exact .inl (⟨b', by grind⟩, a')
  · grind [subrel_val, Sum.Lex.sep, asymm_of s]

Goal state after: