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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p.1 = n
⊢ p = (n, 0)

Tactic:
Finset.HasAntidiagonal.antidiagonal_congr hp (by simp)

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p.1 = n
⊢ p.1 = (n, 0).1
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ g.IsWeierstrassFactorization (Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - r) ↑⋯.unit⁻¹

Tactic:
by
  have H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat := H.1
  set n := (g.map (IsLocalRing.residue A)).order.toNat
  set f := Polynomial.X ^ n - r
  replace H1 : r.degree < (Polynomial.X (R := A) ^ n).degree := by rwa [Polynomial.degree_X_pow]
  have hfdeg : f.natDegree = n := by
    suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
    rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
  refine ⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩
  · rw [hfdeg] at hi
    simp_rw [f, Polynomial.coeff_sub, Polynomial.coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff]
    have := H.coeff_f_sub_r_mem hi
    rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
  · have := congr($(H.2) * ↑(H.isUnit_of_map_ne_zero hg).unit⁻¹)
    rw [add_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, ← sub_eq_iff_eq_add] at this
    simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
this : Module.Finite R₀ (Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
classical exact ⟨n, hn, _, _, _, .of_surjective
    (Matrix.entryLinearMap R₀ _ (0 : Fin n) (0 : Fin n)) fun f ↦ ⟨fun _ _ ↦ f, rfl⟩, ⟨e⟩⟩

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

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

Tactic:
commutes _ _ hm

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
zpow_sub₀ (FractionRing.p_nonzero p k)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq'' : (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ ↑m / ↑p ^ ↑n * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: 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, a ≠ 0 ∧ Φ(p, k) x = a • x

Tactic:
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim
    obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)
    refine ⟨a, ?_, ha.symm⟩
    intro ha'
    apply this
    simp only [← ha, ha', zero_smul]

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

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
⊢ IsStationary s

Tactic:
intro t ht

Goal state after:
α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
t : Set α
ht : IsClub t
⊢ (s ∩ t).Nonempty
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
by
  have h_ninj := not_injective_limitation_set <| lfpApprox f x
  rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
  let ⟨a, b, h_fab, h_nab⟩ := h_ninj
  use a.val; apply And.intro a.prop
  use b.val; apply And.intro b.prop
  apply And.intro
  · intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq
  · exact h_fab

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
simp only [cmp]

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x} = {y, z} ↔ x = y ∧ x = z

Tactic:
rw [eq_comm, pair_eq_singleton_iff]
  simp_rw [eq_comm]

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

Goal state before:
pp: 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
⊢ veblenWith f o 0 ≤ a

Tactic:
veblenWith_of_ne_zero f ho.ne_bot,

Goal state after:
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
⊢ derivFamily (fun x ↦ veblenWith f ↑x) 0 ≤ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr.inr
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∈ range (veblen o) ↔ o ≤ x.invVeblen₁

Tactic:
apply iff_of_false _ h.not_ge

Goal state after:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
⊢ ω ^ x ∉ range (veblen o)
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
· rw [← mem_range_veblen_iff_le_invVeblen₁]
    obtain rfl | ho := eq_zero_or_pos o
    · simp
    · rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (o₁ ^ o₂).NF

Tactic:
· simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]
    have := na.fst
    rcases k with - | k
    · infer_instance
    · cases k <;> cases m <;> infer_instance

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

Goal state before:
pp: case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr + ↑m)

Tactic:
← pow_succ,

Goal state after:
case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ (k + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.nil
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
hF : h_opf.unfold s.head = none
⊢ (op nil).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
simp only [hF, Option.map_map]

Goal state after:
case h.nil
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
hF : h_opf.unfold s.head = none
⊢ (op nil).destruct =
    Option.map ((fun x ↦ (x.1, ↑x.2 s.tail)) ∘ fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.cons.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hd : α
opf' : Stream'.Seq α → Stream'.Seq α
op' : FriendlyOperation opf'
hF : s_hd = hd ∧ s_tl = opf' s.tail
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some (hd, ⟨opf', op'⟩) with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
simp only [hF, Option.map_map]

Goal state after:
case h.cons.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hd : α
opf' : Stream'.Seq α → Stream'.Seq α
op' : FriendlyOperation opf'
hF : s_hd = hd ∧ s_tl = opf' s.tail
⊢ (op (Seq.cons hd (opf' s.tail))).destruct =
    Option.map ((fun x ↦ (x.1, ↑x.2 s.tail)) ∘ fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ opf', ⋯⟩)) (T (some hd))
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case cons
a b : S
iha : S.decode a.encode = a
ihb : S.decode b.encode = b
⊢ S.decode (a.cons b).encode = a.cons b

Tactic:
| cons a b iha ihb =>

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

Goal state before:
pp: ⊢ fastGrowing 1 = fun n ↦ 2 * n

Tactic:
rw [@fastGrowing_succ 1 0 rfl]

Goal state after:
⊢ (fun i ↦ (fastGrowing 0)^[i] i) = fun n ↦ 2 * n
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: ⊢ Ordering

Tactic:
exact .eq

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

Goal state before:
pp: a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r

Tactic:
by
  rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]

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

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ y.Coprime x

Tactic:
apply Nat.Coprime.symm

Goal state after:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := ⋯
y : ℕ := ⋯
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : a * y ^ d = b * x ^ d
⊢ x.Coprime y
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case refine_1
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ ∀ (p : ℚ), (↑x_num / ↑x_den) ^ y_num ≠ p ^ y_den

pp: case refine_2
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ 0 ≤ ↑x_num / ↑x_den

Tactic:
· simp only [div_pow, ← Nat.cast_pow]
    apply not_power_rat_of_num
    · apply Nat.Coprime.pow _ _ hx_coprime
    · apply not_power_nat_pow_of_bounds hy_den_pos hy_coprime hn1 hn2

Goal state after:
case refine_2
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ 0 ≤ ↑x_num / ↑x_den
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 0 = ∅

Tactic:
simp only [Icc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 1 = {1}

Tactic:
simp only [Icc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 2 = {1, 2}

Tactic:
simp only [Icc_ofNat_ofNat]

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case e_opt.cons
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
p : (_ : α) × β
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (p :: m)) = List.dlookup x (p :: m)

Tactic:
rcases p with ⟨fst, snd⟩

Goal state after:
case e_opt.cons
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : 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

Tactic:
rintro ⟨od, hval, hod⟩

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 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 → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ comap (Prod.map F F) (𝓤 (X → α)) ≤ 𝓤 ι

Tactic:
Pi.uniformity,

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
⊢ comap (Prod.map F F) (⨅ i, comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 α)) ≤ 𝓤 ι
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case 𝔖_compact
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, IsCompact K

pp: case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

Tactic:
· exact fun _ ↦ id

Goal state after:
case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ TopCat.generatedBy X ((toTopCat X).obj Y)

Tactic:
rw [TopCat.generatedBy_def]
    exact inferInstanceAs (IsGeneratedBy X (WithGeneratedByTopology X ↑Y))

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
C0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
C1 : ssu := ⋯
C2 : Set (Set (Ultrafilter X.A)) := ⋯
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
⊢ ↑T ⊆ finiteInterClosure C1

Tactic:
intro t ht

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
t : Set (Ultrafilter X.A)
ht : t ∈ ↑T
⊢ t ∈ finiteInterClosure C1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
⊢ IsClosed (cl A)

Tactic:
rw [isClosed_iff]

Goal state after:
X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), cl A ∈ F → X.str F ∈ cl A
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC)))

Tactic:
refine ⟨fun a b h ↦ ?_, fun a ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a b : (fun X ↦ ↑X.toTop) (indexCone hC).pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a =
    (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) b
⊢ a = b

case refine_2
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit (indexFunctor hC)).lift (indexCone hC))) a_1 = a