mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
j : ℕ
hj : j ≤ i
this : (Ideal.Quotient.mk I) ((coeff j) g) = 0
⊢ (coeff j) g ∈ I

Tactic:
← RingHom.mem_ker,

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
H : f - ↑r = g * q
j : ℕ
hj : j ≤ i
this : (coeff j) g ∈ RingHom.ker (Ideal.Quotient.mk I)
⊢ (coeff j) g ∈ I
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

Tactic:
by
  have hj : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_left) = A.val := by ext; rfl
  have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl
  simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h
  let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq
    (Subalgebra.FG.sup hA hA') h
  use B, le_trans le_sup_left hB_le, le_trans le_sup_right hB_le, hB
  simpa only [← rTensor_comp, ← comp_apply] using! h

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
⊢ ∃ s, (rTensor M φ.toLinearMap) s = t

Tactic:
obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ ∃ s, (rTensor M φ.toLinearMap) s = t
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
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
have := IsSimpleModule.nontrivial R N
  have ⟨_, compl⟩ := exists_isCompl N
  have ⟨m, hm, ne⟩ := exists_ne_zero_of_sSup_eq_top (ne_zero_of_surjective
    (projectionOnto_surjective compl)) _ hs
  have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne
  exact ⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)) =
    ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (zmodEquivTrunc p n).symm.toRingHom).comp (truncate n)

Tactic:
RingHom.comp_assoc

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)) =
    (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n))
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).toRingHom.comp (PadicInt.toZModPow n)).comp (toPadicInt p) =
    (truncate n).comp (RingHom.id (𝕎 (ZMod p)))

Tactic:
RingHom.comp_assoc

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (zmodEquivTrunc p n).toRingHom.comp ((PadicInt.toZModPow n).comp (toPadicInt p)) =
    (truncate n).comp (RingHom.id (𝕎 (ZMod p)))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)

Tactic:
have ha' : a ∈ S := by grind

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
ha' : a ∈ S
⊢ Fin (Nat.succ 0).succ × Fin (n + 1)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case right
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ y = x ++ List.drop x.length y

Tactic:
← List.take_append_drop x.length y

Goal state after:
case right
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ List.take x.length y ++ List.drop x.length y = x ++ List.drop x.length y
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t

Tactic:
refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩

Goal state after:
case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ IsClub (⋂ x, f ↑x ⋯)

case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∃ t, IsClub t ∧ Disjoint (⋃₀ s) t

Tactic:
refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩

Goal state after:
case refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ IsClub (⋂ x, f ↑x ⋯)

case refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]

Tactic:
CNF.ne_zero ho,

Goal state after:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) = [(0, o)]
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
CNF.ne_zero ho,

Goal state after:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)) = o
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x ∈ CNF b o → x.1 ≤ log b o

Tactic:
CNF.ne_zero ho,

Goal state after:
case refine_2
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
H : x ∈ CNF b (o % b ^ log b o) → x.1 ≤ log b (o % b ^ log b o)
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.1 ≤ log b o
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
  generalize h' : Lists'.cons a l₁ = l₁' at h
  obtain - | @⟨a', _, _, _, e, m, s⟩ := h
  · cases a
    cases h'
  cases a; cases a'; cases h'; exact ⟨⟨_, m, e⟩, s⟩

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂
⊢ l₁ ⊆ l₂

Tactic:
induction l₁ using recOfList with | _ l₁
    induction l₁ with
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩

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

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
CNF.ne_zero ho,

Goal state after:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst ((log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)))
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e : Ordinal.{u_1}
h : o < b ^ e
he : ∃ a ∈ CNF b o, a.1 = e
⊢ False

Tactic:
obtain ⟨⟨e, c⟩, he, rfl⟩ := he

Goal state after:
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
⊢ False
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
rw [← bsup_eq_iSup]
    apply H (type_ne_zero_iff_nonempty.2 hι)
    exact fun i hi => hf _

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ ⨆ i, f i ∈ s

Tactic:
rw [← this]

Goal state after:
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ enumOrd s (⨆ i, g i) ∈ s
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ enumOrd s '' Set.Iio a ⊆ s

pp: case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ enumOrd s a ≤ o

Tactic:
· apply (Set.image_subset_range ..).trans_eq
      rw [range_enumOrd hs]

Goal state after:
case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ enumOrd s a ≤ o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
by
  rw [veblenWith_of_ne_zero f h]
  exact isNormal_derivFamily _

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

Goal state before:
pp: n✝ : ZFSet.{u}
x : PSet.{u}
x✝ : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))

Tactic:
rw [ZFSet.sound h]
          rfl

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

Goal state before:
pp: case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
· grw [show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l]
    · simpa using mul_le_mul_left (one_le_iff_ne_zero.2 e0) ω
    · exact omega0_pos

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

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ PiNat.firstDiff ↑s ↑t = 0

Tactic:
simp only [PiNat.firstDiff, ne_eq, Classical.dite_not, dite_eq_left_iff,
      Nat.find_eq_zero]

Goal state after:
case e'_2.e'_6
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ ¬↑s = ↑t → ¬↑s 0 = ↑t 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
⊢ FriendlyOperation op ↔ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t

Tactic:
by
  simp [FriendlyOperation, lipschitzWith_iff_dist_le_mul]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
f : ℝ → ℝ
⊢ ms = mk s f ↔ ms.seq = s ∧ ms.toFun = f

Tactic:
by
  conv => lhs; lhs; rw [eq_mk ms]
  rw [mk_eq_mk_iff]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.toFun (left ++ right) =o[atTop] { coef := coef2, unit := exps2 }.toFun right

Tactic:
rw [← this]

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_coef2 : { coef := coef2, unit := exps2 }.coef ≠ 0
h_lt : t1.unit < List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t1.toFun (left ++ right) =o[atTop] t2'.toFun (left ++ right)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ { coef := coef2, unit := exps2 }.toFun right =o[atTop] t1.toFun (left ++ right)

Tactic:
rw [← this]

Goal state after:
left right : Basis
t1 : Monomial
h_basis : WellFormedBasis (left ++ right)
h1 : List.length t1.unit = List.length left + List.length right
h_coef1 : t1.coef ≠ 0
coef2 : ℝ
exps2 : UnitMonomial
h2 : List.length { coef := coef2, unit := exps2 }.unit = List.length right
h_lt : List.replicate (List.length left) 0 ++ { coef := coef2, unit := exps2 }.unit < t1.unit
t2' : Monomial := { coef := coef2, unit := List.replicate (List.length left) 0 ++ exps2 }
this : t2'.toFun (left ++ right) = { coef := coef2, unit := exps2 }.toFun right
⊢ t2'.toFun (left ++ right) =o[atTop] t1.toFun (left ++ right)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
o : ONote
h : o.NF
⊢ C ⟨o, h⟩

Tactic:
induction o with
  | zero => exact H0
  | oadd e n a IHe IHa => exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)

Goal state after:
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: p q : Nat
⊢ Ordering

Tactic:
exact compare p q

Goal state after:
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSym 0 b = 0

Tactic:
jacobiSym.zero_left ?_

Goal state after:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 0 = 0

b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b
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 → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)

Tactic:
rcases CompactSpace.elim_nhds_subcover Ω (fun x ↦ F_eqcont x V hV) with ⟨A, Acover⟩

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[i]? = ys[j]?

pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < ys.length

Tactic:
· symm; rw [h]
      rw [← List.applyId_zip_eq] <;> assumption

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < ys.length
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ map Sigma.fst (List.toFinmap' (xs.zip ys)) ~ map Sigma.snd (List.toFinmap' (xs.zip ys))

Tactic:
by
      simp only [List.toFinmap', comp_def, List.map_fst_zip, List.map_snd_zip, *,
        List.map_map]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : completion G ⟶ P
⊢ (fun f ↦ lift f) ((fun f ↦ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f) f) = f

Tactic:
by apply lift_unique; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
⊢ IsEmbedding ⇑f

Tactic:
refine ⟨isInducing_of_restrict_nhds_zero V_mem H.isInducing, ?_⟩
  have f_injOn : InjOn f V := injOn_iff_injective.2 H.injective
  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
  intro x hx
  obtain ⟨c, hc, c_ne : c ≠ 0⟩ := absorbent_nhds_zero (𝕜 := 𝕜₁) V_mem
    |>.eventually_nhdsNE_zero x |>.and eventually_mem_nhdsWithin |>.exists
  rw [← smul_eq_zero_iff_right c_ne, ← f_injOn.eq_iff hc (mem_of_mem_nhds V_mem), map_zero,
    map_smulₛₗ, hx, smul_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
⊢ DiscreteTopology (PontryaginDual A)

Tactic:
let V : Set (PontryaginDual A) := {ψ | Set.MapsTo ψ Set.univ (Circle.centeredArc (π / 2))}

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
⊢ DiscreteTopology (PontryaginDual A)
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, closedCell n ↑j ⊆ ↑E

Tactic:
apply union_subset E.base_subset
    exact iUnion₂_subset fun n i ↦ closedCell_subset_of_mem E i.2

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set (WithGeneratedByTopology X Y)
⊢ IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' U)

Tactic:
simp [isClosed_iSup_iff, isClosed_coinduced, equiv, Equiv.refl]

Goal state after: