mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_2
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ toFun R f ∘ ⇑(TensorProduct.lid R M).symm) x =
    (rTensor N (Algebra.ofId R S).toLinearMap) (toFun R f (1 ⊗ₜ[R] x))

Tactic:
simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
    congr

Goal state after:
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
tfae_2_to_3 : IsArtinianRing R → ∃ I, IsAtom I
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R

Tactic:
simp_rw [← isFullyInvariant_iff_isTwoSided] at h

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
x✝ : ∃ I, IsAtom I
I : Ideal R
hI : IsAtom I
left✝ : Nontrivial R
h : ∀ (I : Ideal R), Submodule.IsFullyInvariant I → I = ⊥ ∨ I = ⊤
⊢ IsSemisimpleRing R
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ RingHom.ker (algebraMap R (R ⊗[k] K)) ≤ nilradical R

Tactic:
convert! bot_le

Goal state after:
case e'_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ RingHom.ker (algebraMap R (R ⊗[k] K)) = ⊥

case convert_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ⋯
⊢ OrderBot (Ideal R)
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

Tactic:
let e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] (K ⊗[R] S) ⊗[K] L := Algebra.TensorProduct.comm ..

Goal state after:
K : Type u_2
R : Type u_3
S : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R S
L : Type u_5
inst✝⁴ : Field L
inst✝³ : Algebra R L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R K L
inst✝ : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := (Algebra.TensorProduct.cancelBaseChange R K K L S).symm
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
⊢ IsHomeomorph (comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ a = b

Tactic:
Units.ext_iff,

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ ↑a = ↑b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ 1 (↑r * ↑u) = 1 (↑t * ↑s)

Tactic:
simp [one_apply_posSubmonoid]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

Tactic:
simp [one_apply_posSubmonoid]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0

Tactic:
simp [one_apply_posSubmonoid]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1

Tactic:
apply (Valuation.integer.integers (v := vS)).one_of_isUnit at hr

Goal state after:
case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : vR.HasExtension vS
r : ↥vR.integer
hr : vS ((algebraMap (↥vS.integer) S) ((algebraMap ↥vR.integer ↥vS.integer) r)) = 1
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i = (WittVector.truncate n) (↑p ^ i)

Tactic:
rw [map_pow, map_natCast]

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

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i ↦ inverseCoeff a A ↑i
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)

Tactic:
have H := Units.mul_inv (a ^ p ^ (n + 1))

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k :=
  A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + nthRemainder p n (truncateFun (n + 1) A) fun i ↦ inverseCoeff a A ↑i
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp.out.ne_zero

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp.out.ne_zero

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

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp.out.ne_zero

Goal state after:
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 : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
rw [Finset.sum_eq_single_of_mem 0] <;> simp +contextual

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

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
hf : f x = x
⊢ lfpApprox f x o = x

pp: case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x

Tactic:
· exact (lfpApprox_eq_all_of_fixedPoint f hx).mpr hf o

Goal state after:
case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr

Tactic:
(rw [← opow_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega0_opow)

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

Goal state before:
pp: case zero
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : zero.NFBelow b
⊢ (e.addAux n zero).NFBelow b

pp: case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
· exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt

Goal state after:
case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ ↑(mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x))) ↔ x ∈ s

Tactic:
SetLike.mem_coe,

Goal state after:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) ↔ x ∈ s
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]

Goal state after:
case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ ω ^ e₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑↑n₁ + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: ⊢ toZFSet 0 = ∅

Tactic:
ext; simp [mem_toZFSet_iff]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (V_ o).card = preBeth o

Tactic:
induction o using Ordinal.limitRecOn with

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toZFSet.IsOrdinal

Tactic:
refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
  all_goals
    obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
    obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy
  · exact toZFSet_mem_toZFSet_iff.2 (hb.trans ha)
  · obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz
    exact toZFSet_mem_toZFSet_iff.2 (hc.trans hb)

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

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
h' : o₂ ≠ zero
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
          h', ite_false]

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
h' : o₂ ≠ zero
⊢ zero.NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: β : Type u_1
γ : Type u_2
basis_hd : ℝ → ℝ
basis_tl : Basis
F : β → Option (ℝ × MultiseriesExpansion basis_tl × γ × β)
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ gcorec F op b = nil

Tactic:
unfold gcorec
  rw [Seq.gcorec_nil]
  · simp [nil]
  · simpa

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

Goal state before:
pp: case cons.cons.cons.rel
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ Tendsto (fun x ↦ (basis_hd ^ exp2 * toFun m2 basis_tl) x / (basis_hd ^ exp1 * toFun m1 basis_tl) x) atTop atTop

Tactic:
apply Filter.Tendsto.congr' (f₁ := UnitMonomial.toFun ((exp2 - exp1) ::
      UnitMonomial.mul m2 (UnitMonomial.inv m1)) (basis_hd :: basis_tl))

Goal state after:
case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ toFun ((exp2 - exp1) :: mul m2 (inv m1)) (basis_hd :: basis_tl) =ᶠ[atTop] fun x ↦
    (basis_hd ^ exp2 * toFun m2 basis_tl) x / (basis_hd ^ exp1 * toFun m1 basis_tl) x

case cons.cons.cons.rel.h
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ Tendsto (toFun ((exp2 - exp1) :: mul m2 (inv m1)) (basis_hd :: basis_tl)) atTop atTop
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

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

Goal state before:
pp: x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (√x) sn sd

Tactic:
obtain ⟨_, rfl⟩ := h
  refine ⟨?_, ?out⟩
  · apply invertibleOfNonzero
    rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]
    exact Invertible.ne_zero _
  · simp [← hn, ← hd, Real.sqrt_mul (mul_self_nonneg ↑sn)]

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
⊢ False

Tactic:
rcases List.mem_append.1 h with h | h

Goal state after:
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False
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✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Tactic:
by
  rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← F_eqcont.comap_uniformFun_eq]
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ S4 = (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe

Tactic:
hS4,

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
hS4 : S4 = DFunLike.coe '' S1
h : Equicontinuous fun x ↦ ⇑↑x
⊢ DFunLike.coe '' S1 = (U.pi fun x ↦ W) ∩ Set.range DFunLike.coe
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : ProfiniteGrp.{?u.22}
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ ProfiniteGrp.{?u.22} GrpCat).obj Y✝
⊢ (homEquiv X'✝ Y✝).symm (f ≫ g) = profiniteCompletion.map f ≫ (homEquiv X✝ Y✝).symm g

Tactic:
by
      apply lift_unique
      simp [homEquiv]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ ↑(Subgroup.zpowers x⁻¹).topologicalClosure

Tactic:
SetLike.mem_coe,

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ x ∈ (Subgroup.zpowers x⁻¹).topologicalClosure
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᵈ[0] = s

Tactic:
by
  simp [iteratedDerivedSet, gfpApprox_zero]

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

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this✝ : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
i : cell n
this : n < N
⊢ ↑(map n i) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1

Tactic:
exact subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩)
    fun x ↦
    match x with
    | ⟨m, j⟩ => ⟨↑m, j⟩

Tactic:
by simp [Function.RightInverse, Function.LeftInverse]

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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝² : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst✝ : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ ContinuousGeneratedBy X (g ∘ f)

Tactic:
by
  rw [continuousGeneratedBy_iff]
  exact (hg.continuousMap.comp hf.continuousMap).continuous

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ closedCell 0 j = {↑(map 0 j) ![]}

Tactic:
by
  simp [closedCell, Matrix.empty_eq]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : {↑(map 0 x) ![]} = {↑(map 0 y) ![]}
⊢ x = y

Tactic:
singleton_eq_singleton_iff

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : ↑(map 0 x) ![] = ↑(map 0 y) ![]
⊢ x = y
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
⊢ ∀ {X Y : (Finset I)ᵒᵖ} (f : X ⟶ Y),
    (spanFunctor hC).map f ≫
        (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop Y)) ⋯).hom =
      (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop X)) ⋯).hom ≫
        (indexFunctor hC).map f

Tactic:
rintro ⟨s⟩ ⟨t⟩ ⟨⟨⟨f⟩⟩⟩
        ext x
        have : iso_map C (· ∈ t) ∘ ProjRestricts C f =
            IndexFunctor.map C f ∘ iso_map C (· ∈ s) := by
          ext _ i; exact dif_pos i.prop
        exact congr_fun this x

Goal state after: