mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case pos
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

pp: case neg
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
· have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
      grind

Goal state after:
case neg
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2.inr
ι : 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
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)
A : ∑ c ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl c) = 0
i : ι'
hi : Sum.inr i ∈ s
⊢ g (Sum.inr i) = 0

Tactic:
· rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(f ⁻¹' range f) = Nat.card α

Tactic:
simp [Nat.card_univ]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = t.encard - s.encard

Tactic:
by
  rw [← @Set.encard_sdiff_add_encard_of_subset _ s t h]
  exact (ENat.addLECancellable_of_ne_top <| encard_ne_top_iff.mpr hs).eq_tsub_of_add_eq rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0) →
    ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

Tactic:
rintro hv f hf i hi

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
hv : ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0
f : ι → R
hf : ∑ i ∈ s, f i • v i = 0
i : ι
hi : i ∈ s
⊢ f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.ncard = s.toFinset.card

Tactic:
by
  simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.ncard ≤ k

Tactic:
ncard_def,

Goal state after:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.encard.toNat ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Even (insert a s).ncard ↔ Odd s.ncard

Tactic:
by
  rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
⊢ rightRel (s.prod s') = (rightRel s).prod (rightRel s')

Tactic:
refine Setoid.ext fun x y ↦ ?_
  rw [Setoid.prod_apply]
  simp_rw [rightRel_apply]
  rfl

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

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥A ⧸ A'.subgroupOf A)

Tactic:
ext ⟨x, hx⟩

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥A ⧸ A'.subgroupOf A)).comp (mk' (A'.subgroupOf A))) ⟨x, hx⟩
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥B ⧸ B'.subgroupOf B)

Tactic:
ext ⟨x, hx⟩

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ (((quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩ =
    ((MonoidHom.id (↥B ⧸ B'.subgroupOf B)).comp (mk' (B'.subgroupOf B))) ⟨x, hx⟩
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x < succ b ↔ x ∈ Iic b

Tactic:
mem_Iic,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x < succ b ↔ x ≤ b
Module: Mathlib.Order.Interval.Set.SuccPred

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

Tactic:
mem_Iic,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ≤ pred b ↔ x ∈ Iio b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q✝ : Submodule R₂ M₂
x✝ : ↑(Set.Ici p)
q : Submodule R M
hq : q ∈ Set.Ici p
⊢ ↑((fun p' ↦ ⟨comap p.mkQ p', ⋯⟩) ((fun q ↦ map p.mkQ ↑q) ⟨q, hq⟩)) = ↑⟨q, hq⟩

Tactic:
simpa [comap_map_mkQ p]

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

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

Tactic:
simpa using Set.Ico_succ_succ_eq_Ioc_of_not_isMax hb _

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range.mkQ.ker

Tactic:
Submodule.ker_mkQ,

Goal state after:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range
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₂
⊢ comap (inl R M M₂) (⊥.prod ⊥) = ⊥

Tactic:
prod_comap_inl

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₂
⊢ ⊥ = ⊥
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i) ∈ antidiagonal n

Tactic:
rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ i ≤ n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
· rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
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
hy : ∃ x, (∃ y_1 ∈ I, ∃ z, y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
⊢ False

Tactic:
obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy

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₂
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S T U : Ideal R
inst✝² : S.IsTwoSided
inst✝¹ : T.IsTwoSided
inst✝ : U.IsTwoSided
H1 : S ≤ T
H2 : T ≤ U
x : R ⧸ S
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
by
  rw [← RingHom.comp_apply]
  simp

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
h : P.IsPrime
⊢ ∃ p, Prime p ∧ P = span {p}

Tactic:
by
    obtain ⟨p, rfl⟩ := Submodule.IsPrincipal.principal P
    exact ⟨p, (span_singleton_prime (by simp [·] at hP)).mp h, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x y : α →₀ M
⊢ ⇑(x + y) = ⇑x + ⇑y

Tactic:
by
    ext
    simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
x : R
y : α →₀ M
⊢ ⇑(x • y) = (RingHom.id R) x • ⇑y

Tactic:
by
    ext
    simp

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

Goal state before:
pp: α : Type u_1
s : Set (Filter α)
⊢ sSup (lowerBounds s) = sInf s

Tactic:
by
  simp [sInf, Filter.sInf]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x

Tactic:
simpa using! hl.mem_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g

Tactic:
refine le_antisymm hφ (le_trans ?_ (map_mono hψ))
  rw [map_map, eq, map_id]

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

Goal state before:
pp: α : Type u_1
x y : α
⊢ Disjoint (pure x) (pure y) ↔ x ≠ y

Tactic:
by
  simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

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

Goal state before:
pp: case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)

Tactic:
mem_Iic,

Goal state after:
case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ≤ 𝓟 s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)

Tactic:
mem_Iic,

Goal state after:
case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ≤ 𝓟 s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this : ∀ (x : α), f x ≤ M
⊢ ∅ = f ⁻¹' Ioi M

Tactic:
aesop (add forward safe not_le_of_gt)

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

Goal state before:
pp: case inl
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 : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : m ≤ l
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
rw [← hn _ (hm.trans h), hn _ hm]

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

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α

Tactic:
rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]

Goal state after:
case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ Nonempty α
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) ⋯
N : Submodule R M
hN : N.FG
⊢ motive N hN

Tactic:
obtain ⟨s, rfl⟩ := hN
  induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ b ∈ s

Tactic:
apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a)

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
⊢ f a = g a

Tactic:
apply (hf.isLUB_image_Iio_of_isSuccLimit ha).unique

Goal state after:
case mpr.isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsSuccLimit a
IH : ∀ b < a, f b = g b
⊢ IsLUB (f '' Iio a) (g a)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} ↑(Iic o)

Tactic:
by
  rw [← Iio_union_right]
  infer_instance

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
⊢ succ a < iSup f

Tactic:
by
  by_contra! hoa
  exact hao.not_ge (Ordinal.iSup_le fun i ↦ le_of_lt_succ <|
    ((Ordinal.le_iSup _ _).lt_of_ne (hf i)).trans_le hoa)

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

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

Tactic:
· rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]
      simp

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

Goal state before:
pp: case mp
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds ((fun x ↦ x + 1) '' s)
⊢ BddAbove s

pp: case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
· exact ⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩

Goal state after:
case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
constructor <;> rintro ⟨a, ha⟩
  · exact ⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩
  · use a + 1
    simpa [upperBounds]

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o.card ↔ ↑n ≤ o

Tactic:
← Cardinal.ord_le,

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ (↑n).ord ≤ o ↔ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
· simp [hb, isSuccLimit_iff]

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

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)

Tactic:
by
  obtain rfl | hx := eq_zero_or_pos x
  · simp
  · convert! mul_add_mod_mul hx y z using 1 <;>
    rw [add_zero]

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

Tactic:
grind [lt_mul_iff]

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

Tactic:
grind [lt_mul_iff]

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

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [lt_one_iff] at a0

Goal state after:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
have := hb.ne'
    by_cases c = 0 <;> simp_all

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

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

Tactic:
by
  contrapose!; exact apply_lt_nfpFamily_iff H

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

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

Tactic:
by
  obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb] at h
    exact (h.not_gt (pos_iff_ne_zero.2 hc)).elim
  · rwa [opow_le_iff_le_log' hb hc]

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

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap op) o ↔ IsPrincipal op o

Tactic:
constructor <;> exact fun h a b ha hb => h hb ha

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o + o % 2 ^ log 2 o = o

Tactic:
convert! div_add_mod .. using 2

Goal state after:
case e'_2.e'_5
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o = 2 ^ log 2 o * (o / 2 ^ log 2 o)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ n, f^[n] a

Tactic:
· apply Ordinal.iSup_le
    intro l
    rw [List.foldr_const f a l]
    exact Ordinal.le_iSup _ _

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

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ nfp (fun x ↦ a + x) b

Tactic:
← nfp_add_zero

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) 0 ≤ nfp (fun x ↦ a + x) b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : max a b < ℵ₀
⊢ max a b * max a b < c

pp: case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c

Tactic:
· exact (mul_lt_aleph0 h h).trans_le hc

Goal state after:
case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof

Tactic:
cases a using limitRecOn with

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

Goal state before:
pp: a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)

Tactic:
apply le_antisymm
  · have hbl := isSuccLimit_of_isPrincipal_mul hb₂ hb
    rw [(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,
      Ordinal.iSup_le_iff]
    intro ⟨c, hcb⟩
    have hb₁ : 1 < b := one_lt_two.trans hb₂
    have hbo₀ : b ^ log b a ≠ 0 := pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
    apply (mul_le_mul_left (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans
    rw [mul_assoc, opow_succ]
    gcongr
    refine (hb (hbl.succ_lt ?_) hcb).le
    rw [← lt_mul_iff_div_lt hbo₀, ← opow_succ]
    exact lt_opow_succ_log_self hb₁ _
  · grw [opow_succ, opow_log_le_self b ha]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
i : ι
⊢ f i + c ≤ (⨆ i, f i) + c

Tactic:
le_ciSup hf i

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
i : ι
⊢ iSup f + c ≤ (⨆ i, f i) + c