mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
iInf,

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_5
f : ι → RingCon R
⊢ ⇑(sInf (Set.range f)) = ⨅ i, ⇑(f i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
⊢ ∑ i ∈ I, Pi.single i (b i) = b

Tactic:
ext i
      rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]
      refine Finset.sum_eq_single i (fun j _ ne => Pi.single_eq_of_ne ne.symm _) ?_
      intro hiI
      rw [Pi.single_eq_same]
      exact hb _ ((hIJ.top_le trivial).resolve_left hiI)

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

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

Tactic:
by
  by_cases ha : IsMax a
  · rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
  · ext x
    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

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

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

Tactic:
ext x; rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]

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₂
⊢ (inr R M M₂).range = (fst R M M₂).ker

Tactic:
by
  ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

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
S : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
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₄
inst✝³ : Module R M₅
inst✝² : Module R M₆
f✝ : M →ₗ[R] M₂
inst✝¹ : Module S M₃
inst✝ : SMulCommClass R S M₃
f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (fun f ↦ (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) ((fun f ↦ f.1.coprod f.2) f) = f

Tactic:
by simp only [coprod_inl, coprod_inr]

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
y : M
z : M₂
h : f y + g z = 0
this : f y ∈ f.range ⊓ g.range
⊢ f y = 0 ∧ g z = 0

Tactic:
rw [hd.eq_bot, mem_bot] at this

Goal state after:
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
y : M
z : M₂
h : f y + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0
Module: Mathlib.Order.Interval.Finset.SuccPred

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

Tactic:
by simpa using Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
partialSups_apply,

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
⊢ ⇑(partialSups (⇑g ∘ f)) = ⇑g ∘ ⇑(partialSups f)

Tactic:
by
  funext _; simp [partialSups]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n] i0)
⊢ toZ i0 (pred^[n] i0) = -↑n

Tactic:
rcases n with - | n

Goal state after:
case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
hn : ¬IsMin (pred^[0] i0)
⊢ toZ i0 (pred^[0] i0) = -↑0

case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ ⋃ i ∈ range (n + 1), disjointed f i = (partialSups f) n

Tactic:
rw [Nat.range_succ_eq_Iic, biUnion_Iic_disjointed]

Goal state after:
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 (disjointed t)) n

Tactic:
partialSups_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (Iic n).sup' ⋯ (disjointed t)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (partialSups f) i

Tactic:
partialSups_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ f (succ i) \ (Iio (succ i)).sup f = f (succ i) \ (Iic i).sup' ⋯ f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : CompleteBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i ⊓ ⨅ j, ⨅ (_ : j < i), (f j)ᶜ

Tactic:
simp only [disjointed_apply, Finset.sup_eq_iSup, mem_Iio, sdiff_eq, compl_iSup]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: 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 : ℕ
⊢ i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
h_mem

Goal state after:
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
⊢ t n.succ i.succ = x * t n i + y * t n i.succ
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
⊢ y ∈ I

Tactic:
obtain ⟨_, oJ⟩ := isMaximal_iff.1 H

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ y ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Tactic:
have := (add_pow 1 1 n).symm
  simpa [one_add_one_eq_two] using this

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

Goal state before:
pp: case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ¬IsUnit a

Tactic:
intro ha

Goal state after:
case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
ha : IsUnit a
⊢ False
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n m : ℕ
⊢ ∑ k ∈ range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)

Tactic:
by
  induction m with
  | zero => simp
  | succ m hm =>
    rw [sum_range_succ, hm, choose_succ_succ]
    grind

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:
obtain ⟨p, rfl⟩ := Submodule.IsPrincipal.principal P

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
p : α
hP : α ∙ p ≠ ⊥
h : IsPrime (α ∙ p)
⊢ ∃ p_1, Prime p_1 ∧ α ∙ p = span {p_1}
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i ↦ f i ^ (n + 1)) '' ↑s)

Tactic:
by
  classical
  simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map,
    Finset.coe_image, Finset.val_toFinset] using! pow_multiset_sum_mem_span_pow (s.1.map f) n

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ n) '' s)

Tactic:
rcases n with - | n

Goal state after:
case zero
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' s)

case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' ∅)

Tactic:
Set.image_empty,

Goal state after:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ∅
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
⊢ ∀ (a : R ⧸ I) (x y : (ι → R) ⧸ pi fun x ↦ I), a • (x + y) = a • x + a • y

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (smul_add _ _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ (s : Set α), s ⊆ t → p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
x✝ y✝ : Set α
ht₁ : x✝ ∈ {t | p tᶜ}
ht₂ : y✝ ∈ {t | p tᶜ}
⊢ x✝ ∩ y✝ ∈ {t | p tᶜ}

Tactic:
by simp [compl_inter, hunion _ ht₁ _ ht₂]

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

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

Tactic:
rintro x y ⟨a, ha, b, hb, rfl⟩ xy

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
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 ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ x = y

Tactic:
← x.single_add_erase 0,

Goal state after:
case inr.h
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 ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (x 0) + erase 0 x = y
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s

Tactic:
by
  simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

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

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

Tactic:
← empty_mem_iff_bot,

Goal state after:
α : Type u
f : Filter α
s : Set α
⊢ ∅ ∈ f ⊓ 𝓟 s ↔ sᶜ ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ map m f = ⊥ → f = ⊥

Tactic:
← empty_mem_iff_bot,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → f = ⊥
Module: Mathlib.Order.Filter.Map

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

Tactic:
exact seq_mem_seq hw (seq_mem_seq hv ht)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (map Subtype.val atTop) l

Tactic:
tendsto_map'_iff,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f (map Subtype.val atTop) l

Tactic:
tendsto_map'_iff,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Tactic:
rintro ⟨n, s, hs⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
n : ℕ
s : Fin n → M
hs : span R (range s) = N
⊢ ∃ S, S.Finite ∧ span R S = N
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬BddAbove s
⊢ IsCofinal s

Tactic:
contrapose h
  exact .of_not_isCofinal h

Goal state after:
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
⊢ f a ≤ b

Tactic:
have ha' := hs.isSuccLimit_of_notMem hs' ha
      rw [le_iff_forall_le hf ha']
      intro c hc
      obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
      simp_rw [mem_upperBounds, forall_mem_image] at hb
      exact (hf.strictMono hcd).le.trans (hb hd)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : y < sSup (f ⁻¹' Iic x)
⊢ y ∈ f ⁻¹' Iic x

Tactic:
lt_csSup_iff h₂ h₁

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : ∃ b ∈ f ⁻¹' Iic x, y < b
⊢ y ∈ f ⁻¹' Iic x
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ f (sSup (f ⁻¹' Iic x)) ∈ Iic x

Tactic:
hf.map_sSup h₁ h₂

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f '' f ⁻¹' Iic x) ∈ Iic x
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this : Nonempty β
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
let := WellFoundedLT.toOrderBot β

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝ : Nonempty β
this : OrderBot β := WellFoundedLT.toOrderBot β
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r = 0 ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ type_eq_zero_of_empty r⟩
  let ⟨s⟩ := type_eq.1 h
  exact s.toEquiv.isEmpty

Goal state after:
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 : α ≤ β
⊢ typeLT α.ToType ≤ typeLT β.ToType

Tactic:
type_toType,

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α ≤ typeLT β.ToType
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
Subtype.mk_lt_mk

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)
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 : α < β
⊢ typeLT α.ToType < typeLT β.ToType

Tactic:
type_toType,

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α < β
⊢ α < typeLT β.ToType
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove (range fun i ↦ f i + 1) ↔ BddAbove (range f)

Tactic:
rw [range_comp' (· + 1), bddAbove_add_one_image_iff]

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

Goal state before:
pp: case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
t : Set Ordinal.{u} := {b_1 | enumOrd s b ≤ enumOrd s b_1}
⊢ enumOrd s b ∈ s

Tactic:
exact enumOrd_mem hs b

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

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ s → a ∈ range (enumOrd s)

Tactic:
intro ha

Goal state after:
case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o

Tactic:
simpa [Iio_def] using ho.sSup_Iio

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

Goal state before:
pp: ⊢ ∀ {a : Cardinal.{u_1}}, IsSuccLimit a → a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
intro a ha

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
simpa using nat_le_card (n := 1)

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

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ blsub 0 f = 0

Tactic:
rw [blsub_eq_zero_iff]

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

Goal state before:
pp: case inr.inr
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
l' : IsSuccLimit b
⊢ IsSuccLimit (a ^ b)

Tactic:
· exact isSuccLimit_opow (one_lt_of_isSuccLimit l) l'

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
      rw [a0, zero_opow one_ne_zero]
      exact zero_le

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

Goal state before:
pp: case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)

pp: case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x

Tactic:
· rwa [mul_add_one, add_lt_add_iff_left]

Goal state after:
case hbc
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * (v + 1) ≤ b ^ u * x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
⊢ f i (derivFamily f o) = derivFamily f o

Tactic:
induction o using limitRecOn with

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a

Tactic:
induction o using limitRecOn with

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o

Tactic:
intro a ha

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
⊢ a + a < ω ^ o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
by
  rw [← opow_natCast] at ho
  rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]
  apply left_lt_opow one_lt_omega0
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ preAleph o ↔ ω ≤ o

Tactic:
by
  rw [← preAleph_omega0, preAleph_le_preAleph]

Goal state after: