mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p

Tactic:
;

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p

Tactic:
;

Goal state after:
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field K'
inst✝³ : Fintype K
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ 2 * ↑π * I * ↑j.val / ↑N = 2 * ↑π * (↑j.val / ↑N) * I

Tactic:
;

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ 2 * ↑π * I * ↑j.val / ↑N = 2 * ↑π * (↑j.val / ↑N) * I
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑↑(toUnits (toCircle x) ^ n) = ↑↑1

Tactic:
;

Goal state after:
N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑↑(toUnits (toCircle x) ^ n) = ↑↑1
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ZMod n
⊢ ↑↑↑⟨toUnits (toCircle (x✝¹ + x✝)), ⋯⟩ = ↑↑↑(⟨toUnits (toCircle x✝¹), ⋯⟩ * ⟨toUnits (toCircle x✝), ⋯⟩)

Tactic:
;

Goal state after:
N : ℕ
inst✝¹ : NeZero N
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ZMod n
⊢ ↑↑↑⟨toUnits (toCircle (x✝¹ + x✝)), ⋯⟩ = ↑↑↑(⟨toUnits (toCircle x✝¹), ⋯⟩ * ⟨toUnits (toCircle x✝), ⋯⟩)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ y = (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ⟨y, ⋯⟩

Tactic:
;

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ y = (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ⟨y, ⋯⟩
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) χ₁
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ₁

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) χ₁
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ₁
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝¹).toFun a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom✝).toFun a = 0
h :
  (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ ↦ (↑χ.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
a✝ : (ZMod m)ˣ
⊢ (ofUnitHom ((toUnitHom 1).comp (ZMod.unitsMap hm))) ↑a✝ = 1 ↑a✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
a✝ : (ZMod m)ˣ
⊢ (ofUnitHom ((toUnitHom 1).comp (ZMod.unitsMap hm))) ↑a✝ = 1 ↑a✝
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
a✝ : (ZMod m)ˣ
⊢ (ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm))) ↑a✝ =
    (ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm))) ↑a✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
a✝ : (ZMod m)ˣ
⊢ (ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm))) ↑a✝ =
    (ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm))) ↑a✝
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x y : MulChar R R''
a✝ : (↥T)ˣ
⊢ (domRestrict T (x * y)) ↑a✝ = (domRestrict T x * domRestrict T y) ↑a✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x y : MulChar R R''
a✝ : (↥T)ˣ
⊢ (domRestrict T (x * y)) ↑a✝ = (domRestrict T x * domRestrict T y) ↑a✝
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ ↑(Int.negSucc 0) = -1

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ ↑(Int.negSucc 0) = -1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ ⇑C.val '' {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
;

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
h : IsCyclotomicExtension S A ↥C
this : Subalgebra.map C.val (adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ ⇑C.val '' {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
⊢ 0 < orderOf χ

Tactic:
cases nonempty_fintype Mˣ
  apply IsOfFinOrder.orderOf_pos
  exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : NeZero n
d : ℕ
a✝ b✝ : DirichletCharacter R n
hχ : a✝ ∈ {χ | d.Coprime χ.conductor}
hψ : b✝ ∈ {χ | d.Coprime χ.conductor}
⊢ a✝ * b✝ ∈ {χ | d.Coprime χ.conductor}

Tactic:
by
    apply Nat.Coprime.of_dvd_right (conductor_mul_dvd_lcm_conductor _ _)
    exact (Nat.Coprime.mul_right hχ hψ).coprime_div_right <| Nat.gcd_dvd_mul _ _

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
| χ x * ψ x * (φ x_1 * ψ x_1)

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
| χ x * ψ x * (φ x_1 * ψ x_1)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: x p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2) * x = ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) 1

Tactic:
;

Goal state after:
x p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2) * x = ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) 1
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ auxDFT (fun j ↦ Φ (-j)) k = auxDFT Φ (-k)

Tactic:
;

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
k : ZMod N
⊢ auxDFT (fun j ↦ Φ (-j)) k = auxDFT Φ (-k)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
rw [fderiv_norm_rpow x hp, norm_smul, norm_mul]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = (c • auxDFT Φ) x✝

Tactic:
;

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = (c • auxDFT Φ) x✝
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (Φ₁ + Φ₂) x✝ = (auxDFT Φ₁ + auxDFT Φ₂) x✝

Tactic:
;

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ₁ Φ₂ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (Φ₁ + Φ₂) x✝ = (auxDFT Φ₁ + auxDFT Φ₂) x✝
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s

Tactic:
;

Goal state after:
α : Type u_1
s : Multiset α
a : α
⊢ s ⋖ a ::ₘ s
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = ((RingHom.id ℂ) c • auxDFT Φ) x✝

Tactic:
;

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
c : ℂ
Φ : ZMod N → E
x✝ : ZMod N
⊢ auxDFT (c • Φ) x✝ = ((RingHom.id ℂ) c • auxDFT Φ) x✝
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card

Tactic:
;

Goal state after:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1

Tactic:
;

Goal state after:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ s.card + 1
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin ⊥.card

Tactic:
;

Goal state after:
α : Type u_1
s✝ t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin ⊥.card
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
x✝ : Multiset α
hx✝ : x✝ ∈ Set.range val
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x✝ s.val
⊢ t ∈ Set.range val

Tactic:
;

Goal state after:
α : Type u_1
x✝ : Multiset α
hx✝ : x✝ ∈ Set.range val
s : Finset α
t : Multiset α
ht : t ∈ Set.Icc x✝ s.val
⊢ t ∈ Set.range val
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range SetLike.coe

Tactic:
;

Goal state after:
α : Type u_1
x✝ : Set α
hx✝ : x✝ ∈ Set.range SetLike.coe
s : Finset α
t : Set α
ht : t ∈ Set.Icc x✝ ↑s
⊢ t ∈ Set.range SetLike.coe
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
⊢ s ⋖ cons a s ha
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∈ t, t.erase a = s

Tactic:
simpa only [← coe_inj, coe_erase] using! h.finset_coe.exists_set_sdiff_singleton

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin ⊥.val

Tactic:
;

Goal state after:
α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin ⊥.val
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #⊥

Tactic:
;

Goal state after:
α : Type u_1
s✝ t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #⊥
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
⊢ ↑↑8 = 2 ^ 3

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
⊢ ↑↑8 = 2 ^ 3
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Icc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊆ u}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Icc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊆ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ico s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊆ u}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ico s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊆ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊂ u}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioc s t ↔ a✝ ∈ {u ∈ t.powerset | s ⊂ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioo s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊂ u}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t a✝ : Finset α
⊢ a✝ ∈ Ioo s t ↔ a✝ ∈ {u ∈ t.ssubsets | s ⊂ u}
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iic s ↔ a✝ ∈ s.powerset

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iic s ↔ a✝ ∈ s.powerset
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iio s ↔ a✝ ∈ s.ssubsets

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s a✝ : Finset α
⊢ a✝ ∈ Iio s ↔ a✝ ∈ s.ssubsets
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ ↑(χ₈ x✝) * τ ^ ↑x✝ = χ x✝ * ψ₈char x✝

Tactic:
;

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ ↑(χ₈ x✝) * τ ^ ↑x✝ = χ x✝ * ψ₈char x✝
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ τ = IsCyclotomicExtension.zeta (↑8) F (CyclotomicField (↑8) F)

Tactic:
;

Goal state after:
case e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ τ = IsCyclotomicExtension.zeta (↑8) F (CyclotomicField (↑8) F)
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: case hbc
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := ⋯
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := ⋯
⊢ ∑ i ∈ r, (1 / 2) ^ i ≤ 2

Tactic:
;

Goal state after:
case hbc
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := ⋯
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := ⋯
⊢ ∑ i ∈ r, (1 / 2) ^ i ≤ 2