mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ s.ncard ≤ (insert a s).ncard

Tactic:
refine
    s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
  rw [ncard_insert_eq_ite h]; split_ifs <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s

Tactic:
exact mem_own_rightCoset s a

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
⊢ LeftInverse (fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) fun a ↦
    (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)

Tactic:
refine Quotient.ind' fun a => ?_

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ (fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2)
      ((fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        (Quotient.mk'' a)) =
    Quotient.mk'' a
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
⊢ ∀ (fst : α ⧸ t) (snd : ↥t ⧸ s.subgroupOf t),
    (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (fst, snd)) =
      (fst, snd)

Tactic:
refine Quotient.ind' fun a => ?_

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ ∀ (snd : ↥t ⧸ s.subgroupOf t),
    (fun a ↦ (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a))
        ((fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, snd)) =
      (Quotient.mk'' a, snd)
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ x ∈ g • ⇑(mk' N) ⁻¹' U ↔ x ∈ ⇑(mk' N) ⁻¹' U

Tactic:
simp only [Set.mem_preimage, Set.mem_smul_set_iff_inv_smul_mem]

Goal state after:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
x : G
⊢ (mk' N) (g⁻¹ • x) ∈ U ↔ (mk' N) x ∈ U
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
f✝ f : M →* P
g : P → M
hf : RightInverse g ⇑f
x : (ker f).Quotient
⊢ (kerLift f) ((toQuotient ∘ g) ((kerLift f) x)) = (kerLift f) x

Tactic:
by rw [Function.comp_apply, kerLift_mk, hf]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝
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₃
S : Submodule R M
S' : Submodule R M₂
⊢ ⇑(f.coprod g) '' ↑(S.prod S') = Set.image2 (fun a b ↦ f a + g b) ↑S ↑S'

Tactic:
exact Set.image_prod fun m m₂ => f m + g m₂

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid 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₄
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)

Tactic:
← prodMap_comap_prod,

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid 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₄
⊢ Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) (⊥.prod ⊥)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
h1' : (inl R M M₂) x1 ∈ q
h2' : (inr R M M₂) x2 ∈ q
⊢ (x1, x2) ∈ q

Tactic:
simpa using add_mem h1' h2'

Goal state after:
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₄
c : R
x : M × M₂
hx : x.2 = f x.1
⊢ c • x ∈ {p | p.2 = f p.1}

Tactic:
by
    change _ • _ = f (_ • _)
    rw [map_smul, hx]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioc i j) i

Tactic:
rw [h_succFn_eq] at h

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
mul_prod_Ioo_eq_prod_Ioc h

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ ∏ x ∈ Ioc a b, f x = ∏ x ∈ Ioc a b, f x
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
s : Finset ι
⊢ p (f i \ s.sup f)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
partialSups_disjointed

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (partialSups f) i = (partialSups f) i
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} < span {y} ↔ DvdNotUnit y x

Tactic:
rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂

Tactic:
rw [← hr₁, ← hr₂]

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * (i₂ + y * r₂)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) a₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (a₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)

Tactic:
intro c₁

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
⊢ ∀ (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) c₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (c₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support).Nonempty

Tactic:
contrapose! ne; simp_all [-comapDomain_support]

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

Goal state before:
pp: α : Type u
f : Filter α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u

Tactic:
constructor
  · rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
    exact
      ⟨u ∩ v, inter_mem huf hvf, hP inter_subset_left hPu, hQ inter_subset_right hQv⟩
  · rintro ⟨u, huf, hPu, hQu⟩
    exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩

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

Goal state before:
pp: α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
exact forall_congr' fun s =>
    ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t

Tactic:
by
  simp only [le_def, hl.mem_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ generate ((fun x ↦ f ⁻¹' x) '' U) ≤ comap f (generate U)

Tactic:
rw [← map_le_iff_le_comap, le_generate_iff]

Goal state after:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ U ⊆ (map f (generate ((fun x ↦ f ⁻¹' x) '' U))).sets
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq t ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
← ht

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq (u.seq v) ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_4
β : Type u_5
inst✝² : SMul M β
inst✝¹ : SMul N β
e : α ≃ β
inst✝ : SMulCommClass M N β
this✝ : SMul M α := Equiv.smul M e
this : SMul N α := Equiv.smul N e
⊢ ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a

Tactic:
simp [smul_def, smul_comm]

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

Goal state before:
pp: P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k

Tactic:
by simp [eventually_atTop, h]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0

Tactic:
or_iff_not_imp_left

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMul R M
⊢ (∀ {c : R} {x : M}, c • x = 0 → ¬c = 0 → x = 0) ↔ ∀ (r : R), r ≠ 0 → ∀ (m : M), r • m = 0 → m = 0
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
⊢ let this := e.zero;
  let this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α

Tactic:
extract_lets
  refine ⟨fun {r} m ↦ ?_⟩
  simpa [smul_def, zero_def, Equiv.eq_symm_apply] using eq_zero_or_eq_zero_of_smul_eq_zero

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG ↔ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
constructor
  · intro ⟨s'', hs''⟩
    obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span
    refine ⟨s', hs's, ?_⟩
    apply le_antisymm
    · rwa [← hs'', span_le]
    · rw [span_le]
      exact le_trans hs's subset_span
  · intro ⟨s', _, h⟩
    exact ⟨s', h.symm⟩

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
⊢ ∃ y ∈ t, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a

Goal state after:
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ t, a ≤ y
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 : M →ₗ[R] M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → ker (f ^ n) = ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩
  refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)
  rcases le_or_gt m l with h | h
  · rw [← hn _ (hm.trans h), hn _ hm]
  · exact f.iterateKer.monotone h.le

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
⊢ a ∈ s

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
⊢ a ∈ s
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ∃ x, ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
obtain ⟨x, h⟩ := h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s
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
ι : Type u_3
s : Finset ι
N : ι → Submodule R M
h : ∀ i ∈ s, (N i).FG
⊢ (⨆ i ∈ s, N i).FG

Tactic:
simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by
    obtain ha | ha := ha.eq_or_lt
    · simp [← ha] at h
    · exact h₀ _ ha _ _ h

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯

Tactic:
induction s using Finset.induction with

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✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by
  obtain ha | rfl | ha := lt_trichotomy a 0
  · refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonpos_of_nonneg ha.le hb
  · rw [zero_smul] at hab
    exact hab.false.elim
  · refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯

Tactic:
induction s using Finset.induction with

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 : ι), SMulPosReflectLT α (β i)
b : (i : ι) → β i
hb : 0 ≤ b
_a₁ _a₂ : α
i : ι
hi : (_a₁ • b) i < (_a₂ • b) i
⊢ _a₁ < _a₂

Tactic:
exact lt_of_smul_lt_smul_right hi <| hb _

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

Goal state before:
pp: a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b

Tactic:
by simpa [← add_assoc] using add_le_add_iff_right n

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

Goal state before:
pp: case inr
s : Set Cardinal.{u_3}
hn : s.Nonempty
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
by_cases hs : BddAbove s

Goal state after:
case pos
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

case neg
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Ordinal.{v} ≤i Ordinal.{max u v}

Tactic:
refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp),
    fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : type s < (RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1) (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u_3}
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
by_cases hs : BddAbove s

Goal state after:
case pos
s : Set Ordinal.{u_3}
hs : BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)

pp: case inr.inr
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
· rw [mul_succ]
    exact isSuccLimit_add _ l

Goal state after:
case inr.inr
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ (succ c') ≤ a * c

Tactic:
succ_le_of_lt <| l.succ_lt h

Goal state after:
a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * c ≤ a * c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
· rw [ord_le, ← lift_card, card_ord]

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} ↑(s ∪ sᶜ)
⊢ False

Tactic:
rw [union_compl_self, small_univ_iff] at this

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o + ↑n = o + iSup Nat.cast

Tactic:
Ordinal.add_iSup

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ n, o + ↑n = ⨆ i, o + ↑i
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)

Goal state after:
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
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0

Tactic:
rw [log]

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ sSup ((fun x ↦ b ^ x) ⁻¹' Iic 0) = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
⊢ IsPrincipal op (sSup s)

Tactic:
by_cases hs : BddAbove s

Goal state after:
case pos
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
⊢ IsPrincipal op (sSup s)

case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup s)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a

Tactic:
simpa only [nfp_fp H] using H.monotone h

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
or_iff_not_imp_left

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
⊢ ¬b = 0 → a ^ ω ≤ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

Tactic:
or_iff_not_imp_left

Goal state after:
case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → ¬o = 0 → o ∈ Set.range fun x ↦ ω ^ x