mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (Ideal.Quotient.mk 𝔭) (x.coeff n) = 0
⊢ (Ideal.Quotient.mk (𝔭 ^ (n + 1))) ((ghostComponent n) x) = 0

Tactic:
simp only [ghostComponent]

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℕ
x : 𝕎 R
h : ∀ (n : ℕ), (Ideal.Quotient.mk 𝔭) (x.coeff n) = 0
⊢ (Ideal.Quotient.mk (𝔭 ^ (n + 1))) (((Pi.evalRingHom (fun a ↦ R) n).comp ghostMap) x) = 0
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : 𝕎 R♭
this : (Ideal.Quotient.mk (𝔭 ^ 1)) ((fontaineTheta R p) x) = (fontaineThetaModPPow R p 0) x
⊢ (Ideal.Quotient.mk 𝔭) ((fontaineTheta R p) x) = (PreTilt.coeff 0) (x.coeff 0)

Tactic:
apply_fun Ideal.quotEquivOfEq (pow_one (p : R) ▸ Ideal.span_singleton_pow (p : R) 1) at this

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : 𝕎 R♭
this :
  (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (𝔭 ^ 1)) ((fontaineTheta R p) x)) =
    (quotEquivOfEq ⋯) ((fontaineThetaModPPow R p 0) x)
⊢ (Ideal.Quotient.mk 𝔭) ((fontaineTheta R p) x) = (PreTilt.coeff 0) (x.coeff 0)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 0 1 = X ^ 1

Tactic:
simp only [dickson_one, pow_one]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
⊢ (hermite n).coeff (n + k + 1) = 0

Tactic:
induction n generalizing k with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hnk : Odd (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
induction n generalizing k with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (aeval x) (hermite n) * ((-1) ^ n) ^ 2

Tactic:
rw [← pow_mul]

Goal state after:
n : ℕ
x : ℝ
⊢ (aeval x) (hermite n) = (aeval x) (hermite n) * (-1) ^ (n * 2)
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ C (p.coeff 0) + C (p.coeff 1) * X + C (p.coeff 2) * X ^ 2 = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
abel

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ constantCoeff ((expand p hp) φ) = constantCoeff φ

Tactic:
conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (coeff 0) φ = constantCoeff φ
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
⊢ (coeff i) (f - g * (q + s₁ * ↑⋯.unit⁻¹)) ∈ I ^ (k + 1)

Tactic:
set q' := q + s₁ * H.isUnit_shift.unit⁻¹

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
⊢ (coeff i) (f - g * q') ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L n)) → HasProjectiveDimensionLT M n
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))
⊢ HasProjectiveDimensionLT M (n + 1)

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
reg : IsWeaklyRegular (↑M) rs
mem : ∀ r ∈ rs, r ∈ maximalIdeal R
len : rs.length = n + 1
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
| succ n hn =>

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

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], Nonempty (↥m ≃ₗ[R] S)

Tactic:
Subtype.forall',

Goal state after:
R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔ ∀ (x : { a // a ≤ N }) [IsSimpleModule R ↥↑x], Nonempty (↥↑x ≃ₗ[R] S)
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
⊢ IsIsotypic R ↥N ↔ ∀ m ≤ N, ∀ [IsSimpleModule R ↥m], IsIsotypicOfType R ↥N ↥m

Tactic:
Subtype.forall',

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ IsIsotypic R ↥N ↔ ∀ (x : { a // a ≤ N }) [IsSimpleModule R ↥↑x], IsIsotypicOfType R ↥N ↥↑x
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE

Tactic:
tfae_have 2 → 3 := fun _ ↦ IsAtomic.exists_atom _

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
tfae_1_to_2 : IsSemisimpleRing R → IsArtinianRing R
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, imageOfDf ↑i)

Tactic:
exact isOpen_iUnion fun f => isOpen_imageOfDf

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l

Tactic:
cases l <;> simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec,
    true_or, add_pos_iff, zero_lt_one]

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

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun x ↦ veblenWith f ↑x

Tactic:
by
  rw [veblenWith, if_neg h]

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

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h✝ : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
h : o₁ < o₂
⊢ veblenWith f o₁ a = a

Tactic:
← h',

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h✝ : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
h : o₁ < o₂
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o a ∈ range f

Tactic:
obtain rfl | h := eq_zero_or_pos o
  · simp
  · rw [← veblenWith_veblenWith_of_lt hf h]
    simp

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

Goal state before:
pp: case inl
p : ZFSet.{u} → Prop
x : ZFSet.{u}
IH : ∀ y ∈ ∅, Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

pp: case inr
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ ↑y
⊢ p ∅

Tactic:
· exact h.self

Goal state after:
case inr
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ ↑y
⊢ p ∅
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (Γ_ o).invVeblen₁ = Γ_ o

Tactic:
by
  rw [← veblen_gamma_zero, invVeblen₁_veblen veblen_pos, veblen_gamma_zero]

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

Goal state before:
pp: ⊢ IsOrdinal ∉ Class.univ

Tactic:
rintro ⟨x, hx, -⟩
  suffices IsOrdinal x by
    apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]
  refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩ <;> rw [← Class.coe_apply, hx] at *
  exacts [hy.mem hz, hwx.mem_trans hyz hzw]

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

Goal state before:
pp: case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ 2 ^ (V_ (⨆ i, (V_ ↑i).card).ord).card ≤ ⨆ i, (V_ ↑i).card

Tactic:
rw [← card_powerset, ← vonNeumann_add_one]

Goal state after:
case limit.refine_2
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ i, (V_ ↑i).card < o.card
⊢ (V_ ((⨆ i, (V_ ↑i).card).ord + 1)).card ≤ ⨆ i, (V_ ↑i).card
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (o + 1).toZFSet = insert o.toZFSet o.toZFSet

Tactic:
by
  aesop (add simp [mem_toZFSet_iff, le_iff_eq_or_lt])

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

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

Tactic:
· simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr,
        ONote.mulNat_eq_mul, ONote.opowAux, ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add,
        Ordinal.opow_mul, ONote.zero_add]

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

Goal state before:
pp: f g b : ℝ → ℝ
exp : ℝ
h_eq : g =ᶠ[atTop] f
h : Majorized f b exp
⊢ Majorized g b exp

Tactic:
simp only [Majorized] at *
  intro exp' h_exp
  exact EventuallyEq.trans_isLittleO h_eq (h exp' h_exp)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ s (n + 1) = none

Tactic:
← PiNat.apply_eq_of_dist_lt hts (by rfl)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
t : Stream' (Option α)
hn : t n = none
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ t (n + 1) = none
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist nil (Seq.cons x s) = 1

Tactic:
rw [dist_comm]
  simp

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

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

Tactic:
rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at h
  simpa using h s t

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
⊢ (op (Seq.cons s_hd nil)).head = (op (Seq.cons s_hd s_tl)).head

Tactic:
FriendlyOperation.op_cons_head_eq h

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
⊢ (op (Seq.cons s_hd ?m.117)).head = (op (Seq.cons s_hd s_tl)).head

α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
t : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = t
⊢ Stream'.Seq α
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : b + (a - b) < b + o
h' : b ≤ a
⊢ ∃ i, a < b + f i

Tactic:
add_lt_add_iff_left

Goal state after:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
⊢ ∃ i, a < b + f i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H✝ : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
⊢ b + (a - b) < b + f i

Tactic:
add_lt_add_iff_left

Goal state after:
case inr
α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H✝ : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a - b < o
h' : b ≤ a
i : α
H : a - b < f i
⊢ a - b < f i
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : ↑i < ω
h' : a < o * ↑i
⊢ ∃ i, a < o * ↑i + o

Tactic:
exact ⟨i, h'.trans_le le_self_add⟩

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ ms = cons exp coef tl

Tactic:
apply Stream'.Seq.destruct_eq_cons

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Seq.destruct ms = some ((exp, coef), tl)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
⊢ dist s t ≤ 2⁻¹ ^ n

Tactic:
induction n generalizing s t with
  | zero => simp
  | succ n ih =>
    obtain step | ⟨hd, u, v, c, rfl, rfl, h_next⟩ := step s t base
    · simp [step]
    simp only [dist_cons_cons]
    specialize ih h_next
    calc
      _ ≤ 2⁻¹ * dist u v := by
        gcongr
        exact (FriendlyOperationClass.friend _).dist_le
      _ ≤ _ := by
        grw [ih, pow_succ']

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

Goal state before:
pp: case a
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a

Tactic:
exact eq_of_mul_eq_mul_of_coprime_aux (x := b) hxy.symm (by rw [mul_comm, ← h, mul_comm])

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

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

Tactic:
contrapose! hnd

Goal state after:
case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
ha : IsNNRat a n d
hnd : ↑d ≤ 0
⊢ n.gcd d ≠ 1
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

Tactic:
contrapose! hnd

Goal state after:
case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
ha : IsNNRat a n d
hnd : ↑d ≤ 0
⊢ n.gcd d ≠ 1
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s

Tactic:
rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]

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

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s

Tactic:
rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]

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

Goal state before:
pp: case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ (if x' = x then head✝ else applyId (xs.zip tail✝) x) = y ↔ tail✝[n✝]? = some y

Tactic:
rw [if_neg]

Goal state after:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x
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
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Equicontinuous (id ∘ Subtype.val)

Tactic:
equicontinuous_iff_range

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 Subtype.val
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Equicontinuous (id ∘ Subtype.val)
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : 𝓕₁ = 𝓕₂
⊢ t₁ = t₂

Tactic:
by rwa [IsTopologicalAddGroup.ext_iff] <;> infer_instance

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit⁻¹ = ↑this.unit⁻¹ * (-(1 + x) + 1)

Tactic:
rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ∃ a, sᵈ[a] ∈ fixedPoints ⇑relDerivedSet

Tactic:
refine ⟨(Order.succ #(Set X)).ord,
    gfpApprox_ord_mem_fixedPoint relDerivedSet relDerivedSet_subset⟩

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 := 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
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
⊢ P.Nonempty

Tactic:
rcases this P hP with h | h

Goal state after:
case inl
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
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : P ∈ C0
⊢ P.Nonempty

case inr
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
this : ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q
P : Set (Ultrafilter X.A)
hP : P ∈ C2
h : ∃ Q ∈ C0, P = AA ∩ Q
⊢ P.Nonempty