mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ LinearMap.range 0 ≤ isotypicComponent R N ↥S

Tactic:
LinearMap.range_zero,

Goal state after:
case inr
R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
eq : f ∘ₗ S.subtype = 0
⊢ ⊥ ≤ isotypicComponent R N ↥S
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

Tactic:
convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm
    simp [sSup_image, OrderIso.setIsotypicComponents, OrderIso.symm]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius (a * b) = moebius a * moebius b

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
· rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
⊢ moebius (a * b) = 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 := ⋯ }
⊢ FormallySmooth R S

Tactic:
let P' := Gen.toExtension

Goal state after:
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
⊢ FormallySmooth R S
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
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
hr0 : r ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Tactic:
obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hq0 : q ≠ 0
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m_1, φ b * Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 = ↑p ^ m_1 * b
Module: Mathlib.SetTheory.Lists

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

pp: case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
h' : cons a l₁ = cons a' l✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
· cases a
    cases h'

Goal state after:
case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
h' : cons a l₁ = cons a' l✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
hx : x ≤ f x
hab : a < b
hac : a ≤ c
hf : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a

Tactic:
exact (lfpApprox_mono_right f).eq_of_ge_of_le
      hf (lt_add_one a).le (add_one_le_of_lt hab)

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

Goal state before:
pp: b : Ordinal.{u_1}
⊢ eval b 0 = 0

Tactic:
simp [eval]

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ IsOpen[inst✝³] {a} ↔ ¬IsSuccLimit a

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
⊢ IsOpen[inst✝³] {a} ↔ ¬IsSuccLimit a
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
obtain (ha | ha) := not_isSuccLimit_iff.mp ha

Goal state after:
case refine_2.inl
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst✝³] {a}

case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
⊢ (e.oadd n a).NFBelow b

Tactic:
by (obtain - | ⟨h₁, h₂, h₃⟩ := h; exact NFBelow.oadd' h₁ h₂ H)

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

Goal state before:
pp: n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ out f xs ≈ out f ys

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
n : ℕ
f : (Fin n → ZFSet.{u}) → ZFSet.{u}
inst✝ : Definable n f
xs ys : Fin n → PSet.{u}
h : ∀ (i : Fin n), xs i ≈ ys i
⊢ ⟦out f xs⟧ = ⟦out f ys⟧
Module: Mathlib.SetTheory.ZFC.Basic

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

Tactic:
by
  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}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
obtain h | rfl | h := lt_trichotomy o₁ o₂
  on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]
  all_goals
    conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
    simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]

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

Goal state before:
pp: α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ x✝.rank < (mk α✝ A✝).rank

Tactic:
rw [rank_congr h, ← succ_le_iff]

Goal state after:
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = ⨆ a, preBeth ↑a

Tactic:
← fun i : Set.Iio o => ih i i.2,

Goal state after:
case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = ⨆ a, (V_ ↑a).card
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'
⊢ lift.{u, u + 1} #↑(Set.Iio o) ≤ lift.{u + 1, u} (⨆ i, (V_ ↑i).card)

Tactic:
rw [mk_Iio_ordinal, lift_lift, lift_le]

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

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

Tactic:
add_mul_succ

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

case succ.refine_2.e_a.succ.ba
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) (k + 1) (n✝ + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ R + ω0 ^ ↑k * α' = ω0 ^ ↑k * α'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
c : ℝ
⊢ (const (basis_hd :: basis_tl) c).seq = Multiseries.const basis_hd basis_tl c

Tactic:
simp [const, Multiseries.const]

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

Goal state before:
pp: case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ (monomialRpow (basis_hd :: basis_tl) (↑0) r).toFun = (basis_hd :: basis_tl)[0] ^ r

Tactic:
simp [monomialRpow]

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

Goal state before:
pp: case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
i✝ : Fin basis_tl.length
⊢ (monomialRpow (basis_hd :: basis_tl) (↑i✝.succ) r).toFun = (basis_hd :: basis_tl)[i✝.succ] ^ r

Tactic:
simp [monomialRpow]

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

Goal state before:
pp: case oadd
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
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
have := N₁.fst

Goal state after:
case oadd
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
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
n : ℕ
r : ℝ
⊢ (monomialRpow (basis_hd :: basis_tl) n r).seq = Multiseries.monomialRpow basis_hd basis_tl n r

Tactic:
simp [monomialRpow]

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

Goal state before:
pp: case inl
α : 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 : a < b
⊢ ∃ i, a < b + f i

Tactic:
obtain ⟨i⟩ := id hα
    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
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : mk s f = mk t g
⊢ s = t ∧ f = g

Tactic:
mk,

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : (s, f) = mk t g
⊢ s = t ∧ f = g
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : (s, f) = mk t g
⊢ s = t ∧ f = g

Tactic:
mk,

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
s t : Multiseries basis_hd basis_tl
f g : ℝ → ℝ
h : (s, f) = (t, g)
⊢ s = t ∧ f = g
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a (b % 2 + 2 * (b / 2)) = r

Tactic:
hb,

Goal state after:
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a (0 + 2 * (b / 2)) = r
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
if_neg (by simp [hb])

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a / 2) b = jacobiSym (↑a / 2) b

a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
if_neg (by simp [hb])

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a / 2) b = jacobiSym (↑a / 2) b

a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : 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 = y

Tactic:
rw [List.mem_iff_getElem?] at hx hy
    obtain ⟨i, hx⟩ := hx
    obtain ⟨j, hy⟩ := hy
    suffices some x = some y by injection this
    have h₂ := h₁.length_eq
    rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h
    rw [← hx, ← hy]; congr
    apply (List.getElem?_inj _ (h₁.nodup_iff.1 h₀)).mp
    · symm; rw [h]
      rw [← List.applyId_zip_eq] <;> assumption
    · rw [← h₁.length_eq]
      rw [List.getElem?_eq_some_iff] at hx
      obtain ⟨hx, hx'⟩ := hx
      exact hx

Goal state after:
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 ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
g : ↑G
⊢ ↑((ConcreteCategory.hom (eta G)) g) = ↑1 ↔ ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H

Tactic:
funext_iff

Goal state after:
G : GrpCat
g : ↑G
⊢ (∀ (x : FiniteIndexNormalSubgroup ↑G), ↑((ConcreteCategory.hom (eta G)) g) x = ↑1 x) ↔
    ∀ (H : FiniteIndexNormalSubgroup ↑G), g ∈ H
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✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsInducing F
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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ ∀ (a : ↑(⋃₀ 𝔖) → α), MapClusterPt a ⊤ ((⋃₀ 𝔖).domRestrict ∘ F) → a ∈ range ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
mapClusterPt_iff_ultrafilter,

Goal state after:
case inr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))
h✝ : Nonempty α
⊢ ∀ (a : ↑(⋃₀ 𝔖) → α), (∃ U, ↑U ≤ ⊤ ∧ Tendsto ((⋃₀ 𝔖).domRestrict ∘ F) (↑U) (𝓝 a)) → a ∈ range ((⋃₀ 𝔖).domRestrict ∘ F)
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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ (∀ (a : X →ᵤ[𝔖] α), MapClusterPt a ⊤ (⇑(UniformOnFun.ofFun 𝔖) ∘ F) → a ∈ range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔
    ∀ (a : X → α), MapClusterPt a ⊤ F → a ∈ range F

Tactic:
mapClusterPt_iff_ultrafilter,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ (∀ (a : X →ᵤ[𝔖] α),
      (∃ U, ↑U ≤ ⊤ ∧ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (↑U) (𝓝 a)) → a ∈ range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔
    ∀ (a : X → α), (∃ U, ↑U ≤ ⊤ ∧ Tendsto F (↑U) (𝓝 a)) → a ∈ range F
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
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ x ∈ interior (g'⁻¹ • V • {x})

Tactic:
interior_smul,

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 : (interior ((g • V) • {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (V • {x})
⊢ x ∈ g'⁻¹ • interior (V • {x})
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
x : ↑(completion G).toProfinite.toTop
⊢ ⇑(Hom.hom f) ∘ etaFn G = ⇑(Hom.hom g) ∘ etaFn G

Tactic:
funext y

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f g : completion G ⟶ P
h : eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f = eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map g
x : ↑(completion G).toProfinite.toTop
y : ↑G
⊢ (⇑(Hom.hom f) ∘ etaFn G) y = (⇑(Hom.hom g) ∘ etaFn G) y