mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)

Tactic:
have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)

Goal state after:
R : Type u_2
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[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
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

Tactic:
have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)

Goal state after:
R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsAtom S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal

Tactic:
rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ f y ∈ q.asIdeal ↔ f y ∈ q'.asIdeal
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
hab.moebius_eq,

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
hab : Squarefree (a * b)
⊢ (-1) ^ (factors (a * b)).card = moebius a * moebius b
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝³ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP✝ : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝² : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝¹ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this✝ : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
this : IsScalarTower P.Ring P'.Ring S'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
infeq : IP ⊓ J = IP * J
⊢ RingHom.ker (algebraMap S S') = Ideal.map (algebraMap P.Ring S) (RingHom.ker (algebraMap P.Ring P'.Ring))

Tactic:
simp [kerP, ← ISeq, eqmap, IS, I]

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ⊆ univ ×ˢ range n

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
· apply Subset.trans (vars_pow _ _)
    have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
    rw [this, vars_C]
    apply empty_subset

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
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
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)

Tactic:
rw [← sub_eq_zero]
  have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂
  simp only [Polynomial.eval_X, Polynomial.eval_C,
    Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add,
    Polynomial.eval_sub, Polynomial.IsRoot.def]
    at this
  convert! this using 1
  ring

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

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
⊢ ¬IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t

Tactic:
simp [IsStationary, disjoint_iff, not_nonempty_iff_eq_empty]

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

Goal state before:
pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : ℵ₀ < cof α
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

Tactic:
apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _)

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : ℵ₀ < cof α
⊢ #↑s ≤ ℵ₀
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
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)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rcases le_or_gt b 1 with hb | hb

Goal state after:
case refine_2.inl
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 : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

case refine_2.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
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
⊢ a₁ ∈ l₁.toList → a₁ ∈ l₂✝

Tactic:
m₁

Goal state after:
case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
⊢ a₁ ∈ l₂✝
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
intro e₂

Goal state after:
case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
⊢ e₂ ∈ (f₁ + f₂).support → e₂ ≤ e₁
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
assumption

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ (StrictMono fun x ↦ veblenWith f x 0) ∧
    ∀ (o : Ordinal.{u}), IsSuccLimit o → ∀ (a : Ordinal.{u}), (∀ b < o, veblenWith f b 0 ≤ a) → veblenWith f o 0 ≤ a

Tactic:
refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩

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
⊢ veblenWith f o 0 ≤ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ f a < veblenWith f o (f a) ↔ a < veblenWith f o a

Tactic:
by
  simpa using veblenWith_lt_veblenWith_veblenWith_iff hf zero_le

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

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o

Tactic:
exact h (Mem.mk A a)

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

Goal state before:
pp: case a
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

Tactic:
assumption

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

Goal state before:
pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ w✝ ∈ x

Tactic:
assumption

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

Goal state before:
pp: case a
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x✝

Tactic:
assumption

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

Goal state before:
pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ w✝ ∈ x

Tactic:
assumption

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

Goal state before:
pp: case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
· rintro ⟨w, hwx, z, rfl, hwz⟩
    exact ⟨z, rfl, w, hwx, hwz⟩

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
x✝ : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left✝ : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
⊢ z = f y

Tactic:
rw [← fw, wy]

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
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).repr

Tactic:
simp [(· * ·)]

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
| (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n (a', m').1 = o' ∧ (a', m').2 = m → e.oadd n a.split.1 = scale 1 o' ∧ a.split.2 = m

Tactic:
simp only [split_eq_scale_split' h', and_imp]

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝ : e.NF
this : a.NF
⊢ (e - 1).oadd n a' = o' → m' = m → e.oadd n (scale 1 a') = scale 1 o' ∧ m' = m
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 1 / 2
⊢ x✝ = x✝¹

Tactic:
grind [dist_cons_cons_eq_one]

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

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ tl_exp < exp

Tactic:
replace h_step := (h_step exp coef tl h).right.left

Goal state after:
case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
h_step : leadingExp tl < ↑exp
⊢ tl_exp < exp
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' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
hx' : x' = ↑x
h : ↑a * ↑y ^ d = ↑x ^ d * ↑b
⊢ ↑a * ↑y ^ d = ↑x ^ d * ↑b

Tactic:
assumption

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

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
by_cases hb_zero : b = 0
  · subst hb_zero
    contrapose! ha
    simp only [Nat.coprime_zero_right] at h_coprime
    subst h_coprime
    use 1
    simp
  by_contra! h
  rw [← Rat.num_div_den q] at h
  set x' := q.num
  set y := q.den
  obtain ⟨x, hx'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ x' by rwa [Rat.num_nonneg])
  rw [hx'] at h
  specialize ha x
  simp only [Int.cast_natCast, div_pow] at h
  rw [div_eq_div_iff] at h
  rotate_left
  · simpa
  · simp [y]
  replace h : a * y ^ d = x ^ d * b := by
    qify
    assumption
  apply ha
  conv at h => rhs; rw [mul_comm]
  apply eq_of_mul_eq_mul_of_coprime h_coprime _ h
  apply Nat.Coprime.pow_left
  apply Nat.Coprime.pow_right
  apply Nat.Coprime.symm
  simpa [hx'] using (show x'.natAbs.Coprime y from Rat.reduced q)

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

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

Tactic:
simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃

Goal state after:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
h₃ : ∃ a b, (a, b) ∈ xs.zip ys ∧ ⟨a, b⟩ = ⟨x, val⟩
⊢ val ∈ ys
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a.h₀
α : 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
⊢ xs.Nodup

Tactic:
assumption

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

Goal state before:
pp: case pos.e_a.h₁
α : 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
⊢ xs.length = ys.length

Tactic:
assumption

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

Goal state before:
pp: case pos.e_a.h₂
α : 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
⊢ xs[j]? = some y

Tactic:
assumption

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

Goal state before:
pp: case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ y ∉ xs

Tactic:
assumption

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

Goal state before:
pp: case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x ∉ xs

Tactic:
assumption

Goal state after:
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
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty

Tactic:
rw [smul_assoc, interior_smul] at I

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
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (g • interior (V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ ∀ᵇ (x : α), x ∈ closure[inst✝] s ↔ x ∈ s

Tactic:
filter_upwards [coborder_mem_residual hs] with x hx

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure[inst✝] s ↔ x ∈ s
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : IsGeneratedBy X Y
⊢ TopCat.generatedBy X (TopCat.of Y)

Tactic:
assumption

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
hn : n ≠ 0
j : cell C n
this : NeZero n := ⋯
⊢ ↑(map n j) (Pi.single 0 1) ∈ cellFrontier n j

Tactic:
simp only [cellFrontier, mem_image, mem_sphere_iff_norm, sub_zero]

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
hn : n ≠ 0
j : cell C n
this : NeZero n := { out := hn }
⊢ ∃ x, ‖x‖ = 1 ∧ ↑(map n j) x = ↑(map n j) (Pi.single 0 1)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
as : List I
ih :
  List.IsChain (fun x1 x2 ↦ x1 > x2) as →
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) as).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ as})
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) as

Tactic:
rw [List.isChain_cons] at ha; exact ha.2

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i

Tactic:
rcases a with ⟨_, c, hc, rfl⟩
      rcases b with ⟨_, d, hd, rfl⟩
      simp only [Proj, if_neg hi]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
hi : i ∈ ↑l
h' : ¬J i
this : eval (π C J) l = 0
⊢ eval (π C J) l ∈ Submodule.span ℤ (eval (π C J) '' {m | m < l})

Tactic:
by
    rw [this]
    exact Submodule.zero_mem _

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
this : L l
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
assumption

Goal state after: