mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case coe.coe
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
n : ℕ
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑↑n ↔ projectiveDimension M + 1 ≤ ↑↑n

Tactic:
simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯

Tactic:
have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ c' ∈ {isotypicComponent R M ↥S}

Tactic:
eq_isotypicComponent_of_le hc'.1 le'

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ isotypicComponent R M ↥S' ∈ {isotypicComponent R M ↥S}
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_2.smul
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
r : R
hr : r ∈ I
m : M
hm : m ∈ f.ker
⊢ r • m ∈ f.ker ⊓ I • ⊤

Tactic:
simpa [LinearMap.mem_ker.mp hm] using Submodule.smul_mem_smul hr Submodule.mem_top

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (wittMul p (n + 1) + C (↑p ^ (n + 1)) * X (0, n + 1) * X (1, n + 1) -
          X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
        X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))).vars =
    (C (↑p ^ (n + 1)) *
        (wittMul p (n + 1) + C (↑p ^ (n + 1)) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
vars_C_mul

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (wittMul p (n + 1) + C (↑p ^ (n + 1)) * X (0, n + 1) * X (1, n + 1) -
          X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
        X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))).vars =
    (wittMul p (n + 1) + C (↑p ^ (n + 1)) * X (0, n + 1) * X (1, n + 1) -
          X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
        X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))).vars

case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) ≠ 0
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (b • F₀ c) = b • F₀ (↑p ^ m • φ(p, k) c)

Tactic:
LinearMap.toSpanSingleton_apply K(p, k) V x c,

Goal state after:
case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (b • c • x) = b • F₀ (↑p ^ m • φ(p, k) c)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
⊢ IsClub (Function.fixedPoints f)

Tactic:
cases isEmpty_or_nonempty α; · simp
  refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
  · rwa [image_congr hs, image_id']
  · cases topOrderOrNoTopOrder α with
    | inl => use ⊤; simpa using! hf.strictMono.id_le ⊤
    | inr h =>
      rw [noTopOrder_iff_noMaxOrder] at h
      suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)

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

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
⊢ ¬InjOn g (Iio (succ #α).ord)

Tactic:
intro h_inj
  have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj
  have mk_initialSeg_subtype :
      #(Iio (ord <| succ #α)) = lift.{u + 1} (succ #α) := by
    simpa only [coe_ofPred, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)
  rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
  exact not_le_of_gt (Order.lt_succ #α) h

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).SortedGT

Tactic:
sortedGT_iff_pairwise

Goal state after:
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_3
s t : Set Ordinal.{u}
ht : t ⊆ s
ht₀ : t.Nonempty
ht₁ : Small.{u, u + 1} ↑t
tfae_1_to_2 : sSup t ∈ closure s → sSup t ∈ closure (s ∩ Iic (sSup t))
tfae_2_to_3 : sSup t ∈ closure (s ∩ Iic (sSup t)) → (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t
tfae_3_to_4 :
  (s ∩ Iic (sSup t)).Nonempty ∧ sSup (s ∩ Iic (sSup t)) = sSup t →
    ∃ t_1 ⊆ s, t_1.Nonempty ∧ BddAbove t_1 ∧ sSup t_1 = sSup t
⊢ ⨆ i, (Subtype.val ∘ ⇑(equivShrink ↑t).symm) i = sSup t

Tactic:
· simp [(equivShrink t).symm.iSup_comp, ← sSup_eq_iSup']

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

Goal state before:
pp: case single_add
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ e' < e

pp: b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x < b

pp: b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ ∀ (e' : Ordinal.{u_1}), f e' < b

Tactic:
· apply he e' _
      simp [hx]

Goal state after:
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ x < b

b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ ∀ (e' : Ordinal.{u_1}), f e' < b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)

Tactic:
by
  rw [deriv_eq_enumOrd (isNormal_veblenWith hf o),
    veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne', derivFamily_eq_enumOrd]
  · apply congr_arg
    ext a
    rw [mem_iInter]
    use fun ha ↦ ha ⟨o, lt_succ o⟩
    rintro (ha : _ = _) ⟨b, hb : b < _⟩
    obtain rfl | hb := lt_succ_iff_eq_or_lt.1 hb
    · rw [Function.mem_fixedPoints_iff, ha]
    · rw [← ha]
      exact veblenWith_veblenWith_of_lt hf hb _
  · exact fun o ↦ isNormal_veblenWith hf o.1

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

Goal state before:
pp: case cons.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < succ (max (↑a) b)

Tactic:
rw [lt_succ_iff]

Goal state after:
case cons.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a ≤ max (↑a) b
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
⊢ ∃ y, succ (A✝ y).rank = x✝

Tactic:
obtain ⟨b, h'⟩ := αβ a
      exists b
      rw [← h, rank_congr h']

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

Goal state before:
pp: case inr
o a : Ordinal.{u}
h : a.invVeblen₁ ≤ o
⊢ a < veblen o a ↔ a.invVeblen₁ ≤ o

Tactic:
simpa [(lt_veblen_invVeblen₁ a).trans_le (veblen_left_monotone _ h)]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
← rank_powerset

Goal state after:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x → p ∅

Tactic:
apply @ZFSet.inductionOn _ x

Goal state after:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y : ZFSet.{u_1}
⊢ (x ∪ y).rank = max x.rank y.rank

Tactic:
by
  apply le_antisymm
  · simp_rw [rank_le_iff, mem_union, lt_max_iff]
    intro
    apply Or.imp <;> apply rank_lt_of_mem
  · apply max_le <;> apply rank_mono <;> intro _ h <;> simp [h]

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
conv_lhs => dsimp only [HSub.hSub, Sub.sub]; dsimp only [sub]

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
⊢ (match e₁.cmp e₂ with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
← rank_powerset

Goal state after:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
⊢ -b + -b = -2 • b

Tactic:
have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm
  rw [h, ← add_zsmul]; norm_num

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz

Goal state after:
case refine_2
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
c : Ordinal.{u_1}
hc : c < b
hz : c.toZFSet ∈ b.toZFSet
⊢ c.toZFSet ∈ a.toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
ω00 : 0 < ω0 ^ ↑0
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (0 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) 0 0).repr
IH : (0 ≠ 0 → R < ω0 ^ succ ↑0) ∧ ω0 ^ ↑0 * α' + R = (α' + ↑0) ^ succ ↑0
RR : R' = ω0 ^ ↑0 * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑0)
⊢ R = 0

Tactic:
simp [R, opowAux]

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

Goal state before:
pp: case succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
n✝ : ℕ
ω00 : 0 < ω0 ^ ↑(n✝ + 1)
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1) 0).repr
IH : (n✝ + 1 ≠ 0 → R < ω0 ^ succ ↑(n✝ + 1)) ∧ ω0 ^ ↑(n✝ + 1) * α' + R = (α' + ↑0) ^ succ ↑(n✝ + 1)
RR : R' = ω0 ^ ↑(n✝ + 1) * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑(n✝ + 1))
⊢ R = 0

Tactic:
simp [R, opowAux]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ LipschitzWith 1 (op ∘ op')

Tactic:
convert! h.comp h'

Goal state after:
α : Type u_1
op op' : Stream'.Seq α → Stream'.Seq α
h : LipschitzWith 1 op
h' : LipschitzWith 1 op'
⊢ 1 = 1 * 1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
· simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
          repr]
        simp [opow_add, opow_mul]

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (x : ℝ),
    0 < basis_hd x ∧
        (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis_tl).prod) x =
          (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) exps basis_tl).prod⁻¹) x →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) (basis_hd :: basis_tl)).prod)
          x =
        (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)).prod⁻¹) x

Tactic:
intro x ⟨h_pos, ih⟩

Goal state after:
case cons.cons
exp : ℝ
exps : List ℝ
ih✝ :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
h_pos : 0 < basis_hd x
ih :
  (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis_tl).prod) x =
    (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) exps basis_tl).prod⁻¹) x
⊢ (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) (basis_hd :: basis_tl)).prod) x =
    (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)).prod⁻¹) x
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑(e' % ↑n') = ↑r

Tactic:
h₂.out,

Goal state after:
e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑↑r = ↑r
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) ↔ ¬(withDefault A 0).apply a = 0

Tactic:
apply_eq_dlookup

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) ↔ ¬(List.dlookup a A).getD 0 = 0
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap (((fun x ↦ x) ∘ i.domRestrict ∘ ⇑(UniformOnFun.ofFun 𝔖).symm) ∘ F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)

Tactic:
UniformOnFun.ofFun,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap
        (((fun x ↦ x) ∘
            i.domRestrict ∘ ⇑{ toFun := fun x ↦ x, invFun := fun x ↦ x, left_inv := ⋯, right_inv := ⋯ }.symm) ∘
          F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
⊢ U • {x} ∈ 𝓝 x

Tactic:
let K : ℕ → Set G := compactCovering G

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
⊢ U • {x} ∈ 𝓝 x