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

Goal state before:
pp: α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
aux : {x | x ≠ a} ∪ {a} = univ
⊢ {x | x ≠ a}.encard + 1 = ENat.card α

Tactic:
encard_singleton,

Goal state after:
α : Type u_1
a : α
this : {x | x ≠ a}.encard + 1 = ({x | x ≠ a} ∪ {a}).encard
aux : {x | x ≠ a} ∪ {a} = univ
⊢ {x | x ≠ a}.encard + 1 = ENat.card α
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
← rank_top R M

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t \ s = ∅
⊢ s = t

Tactic:
sdiff_eq_empty

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : (t \ s).encard + s.encard ≤ 0 + s.encard
hdiff : t ⊆ s
⊢ s = t
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

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

Tactic:
classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
  constructor
  · rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
  · rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Bijective f
t : Set β
⊢ t ⊆ range f

Tactic:
by simp [hf.surjective.range_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
⊢ y ∈ f '' s → {x | x ∈ s ∧ f x = y}.ncard ≠ 0

Tactic:
rintro ⟨z, hz, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
z : α
hz : z ∈ s
⊢ {x | x ∈ s ∧ f x = f z}.ncard ≠ 0
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
⊢ m ∈ span R (range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)

Tactic:
refine
    ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩,
      fun h => ?_⟩

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : IsTorsionFree R S
b : Basis ι S M
m : M
h : ∀ (i : ι), (b.repr m) i ∈ range ⇑(algebraMap R S)
⊢ m ∈ span R (range ⇑b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card

Tactic:
by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ (i.insertNth (x / y) fun i_1 ↦ p i_1 / p i_1) = i.insertNth (x / y) 1

Tactic:
div_self',

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ (i.insertNth (x / y) fun i_1 ↦ 1) = i.insertNth (x / y) 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_3
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
rw [hs.ncard]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t \ s = ∅

Tactic:
sdiff_eq_empty

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t ⊆ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
exact ncard_union_le s t

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
⊢ ∀ (a₁ a₂ : M), c.toSetoid a₁ a₂ ↔ d.toSetoid (↑e a₁) (↑e a₂)

Tactic:
apply Con.ext_iff.mp h

Goal state after:
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
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))

Tactic:
rintro rfl; exact ⟨QuotientTop.unique⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
⊢ (f.coprod g).ker = f.ker.prod g.ker

Tactic:
apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)
  rintro ⟨y, z⟩ h
  simp only [mem_ker, mem_prod, coprod_apply] at h ⊢
  have : f y ∈ (range f) ⊓ (range g) := by
    simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
    use -z
    rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
  rw [hd.eq_bot, mem_bot] at this
  rw [this] at h
  simpa [this] using h

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ x ∈ ⨆ i, map (single R φ i) (p i)

Tactic:
← Finset.univ_sum_single x

Goal state after:
case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ ∑ i, Pi.single i (x i) ∈ ⨆ i, map (single R φ i) (p i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
k : ι'
⊢ x (Sum.inr k) = 0

Tactic:
induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]

Goal state after:
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
p₂ : Submodule R M₂
⊢ p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, map_top, range_fst, range_snd]

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i

Tactic:
rw [le_isGLB_iff (succFn_spec i), mem_lowerBounds]

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i ≤ j
⊢ ∃ n, succ^[n] i = j

Tactic:
rw [le_iff_lt_or_eq] at hij

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ i = j

Tactic:
rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

pp: case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
· rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max
      rw [hn_max]
      exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)

Goal state after:
case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ (n + 1) ∈ I
⊢ r ∈ I

Tactic:
rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0

Tactic:
rw [sub_mul, one_mul, sub_eq_zero, eq_comm, IsIdempotentElem]

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} →
      y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} → x ∩ y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩
        refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
        ac_rfl

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

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

Tactic:
intro t
    simp_rw [mem_sup, hl.mem_iff, hl'.mem_iff, PProd.exists, union_subset_iff,
       ← exists_and_right, ← exists_and_left]
    simp only [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨆ i, l i ↔ ∃ i, (∀ (i_1 : ι), p i_1 (i i_1)) ∧ ⋃ i_1, s i_1 (i i_1) ⊆ t

Tactic:
by
    simp only [(hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
      mem_iSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
⊢ ∀ s ∈ l₂, (fun x ↦ if p x then f x else g x) ⁻¹' s ∈ l₁

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
⊢ (fun x ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Tactic:
rw [disjoint_comm, disjoint_principal_right]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Tactic:
refine sets_of_superset (map g f) (image_mem_map ht) ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ s.seq t
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid M
e : α ≃ β
inst✝ : MulAction M β
⊢ ∀ (b : α), 1 • b = b

Tactic:
by simp [smul_def]

Goal state after:
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 N
inst✝² : SMul M β
inst✝¹ : SMul N β
e : α ≃ β
inst✝ : IsScalarTower M N β
this✝ : SMul M α := Equiv.smul M e
this : SMul N α := Equiv.smul N e
⊢ ∀ (x : M) (y : N) (z : α), (x • y) • z = x • y • z

Tactic:
simp [smul_def, smul_assoc]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsLeftCancelMul β
⊢ IsLeftCancelMul α

Tactic:
let := e.mul; exact e.injective.isLeftCancelMul _ fun _ _ ↦ e.apply_symm_apply _

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

Goal state before:
pp: case inr
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop

Tactic:
· rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]

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

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : span ℕ ↑S = P
⊢ AddSubmonoid.closure ↑S = P.toAddSubmonoid

Tactic:
simpa [← span_nat_eq_addSubmonoidClosure]

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
⊢ IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Tactic:
refine .trans ?_ ((CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3).symm
  exact
    ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h =>
      ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩

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 : M
hx : (f ^ m) x ∈ ↑(LinearMap.ker (f ^ n))
⊢ x ∈ LinearMap.ker (f ^ (n + m))

Tactic:
simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx

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 : 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

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 : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module S M
inst✝ : Module S N
f : M →ₗ[S] N
hf : Function.Surjective ⇑f
s : S
x✝ : ModuleCon.Quotient M (ker f.toDistribMulActionHom)
a✝ : M
⊢ (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
      (s • Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝) =
    (RingHom.id S) s •
      (AddCon.quotientKerEquivOfSurjective f.toAddMonoidHom hf).toFun
        (Quot.mk (⇑(ker f.toDistribMulActionHom).toSetoid) a✝)

Tactic:
apply map_smul f

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

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

Tactic:
constructor <;> intro h b hb

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False
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 β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

Tactic:
intro s hs

Goal state after:
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
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 α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
intro s hs

Goal state after:
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
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ ↑S ⊆ ↑(N (S.attach.sup f))

Tactic:
intro s hs

Goal state after:
case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
s : M
hs : s ∈ ↑S
⊢ s ∈ ↑(N (S.attach.sup f))
Module: Mathlib.Order.DirSupClosed

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

Tactic:
simpa [not_iff_not] using hs.compl.mem_iff_of_antisymmRel h

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (s : Set Ordinal.{u_2}), IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s

Tactic:
intro s hs

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : IsCofinal s
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α.ToType <i β.ToType

Tactic:
apply Classical.choice (type_lt_iff.mp _)
  rwa [type_toType, type_toType]

Goal state after:
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:
rw [← Iio_union_right]
  infer_instance

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ∀ (i : α ⊕ β), f i ≤ max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Tactic:
rintro (i | i)
    · exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)
    · exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

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

Goal state before:
pp: α✝ : 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
f : s ≺i r
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)

Tactic:
use typein r f.top

Goal state after:
case h
α✝ : 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
f : s ≺i r
⊢ (RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1) ((typein r).toRelEmbedding f.top) = type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f < lsub f
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

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

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub f
hf : ∀ (i : ι), f i ≠ iSup f
this : (∀ (a : ι), f a ≠ ⨆ i, f i) ↔ ∀ (a : ι), f a < ⨆ i, f i
⊢ False

Tactic:
exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))

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

Goal state before:
pp: b n : ℕ
hb : n < b
⊢ log b n = 0

Tactic:
fun_cases log with
  | case1 => rfl
  | case2 => fun_cases log.go with grind

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

Goal state before:
pp: case inl
⊢ 1 - 0 = 1

Tactic:
Ordinal.sub_zero

Goal state after:
case inl
⊢ 1 = 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m

Tactic:
by
  rcases eq_or_ne m 0 with (rfl | hm)
  · rw [Nat.pow_one] at h₂
    exact log_of_lt h₂
  · exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩

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 = 0
⊢ 0 ^ 1 ≤ 0 ^ b

Tactic:
zero_opow one_ne_zero

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

Goal state before:
pp: case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_

Goal state after:
case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, ((fun x ↦ a ^ x) ∘ fun x ↦ b + x) a' ≤ d) ↔ a ^ b * a ^ c ≤ d
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
← opow_le_iff_le_log hb (mul_ne_zero hx hy),

Goal state after:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ (log b x + log b y) ≤ x * y
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[(List.replicate n ()).length] a ≤ nfp f a

Tactic:
← List.foldr_const f a

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x ↦ f) a (List.replicate n ()) ≤ nfp f a