harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMToPartrec.lean
theorem contSupp_supports {S k} (H : contSupp k ⊆ S) : Supports (contSupp k) S

Proof state:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main (move₂ (fun x => false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S

Tactic:
refine supports_union.2 ⟨codeSupp'_supports H₂, ?_⟩

Result:
case cons₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main (move₂ (fun x => false) aux stack (trNormal f k.cons₂)))) ∪
      codeSupp f k.cons₂ ⊆
    S
H₂ : codeSupp f k.cons₂ ⊆ S
h : codeSupp' f k.cons₂ ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S

Proof state:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
have H₂ := Finset.union_subset_right H'

Result:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Proof state:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp k.cons₂ ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
rw [contSupp_cons₂] at H'

Result:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp k.cons₂) S

Proof state:
case fix
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' f.fix k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S

Tactic:
exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩

Result:
no goals

Proof state:
case cons₂
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp k.cons₂ ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp k.cons₂) S

Tactic:
exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH

Result:
no goals

Proof state:
case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcdB_zero_left {s : ℕ} : gcdB 0 s = 1

Proof state:
s : ℕ
⊢ gcdB 0 s = 1

Tactic:
unfold gcdB

Result:
s : ℕ
⊢ (xgcd 0 s).2 = 1

Proof state:
s : ℕ
⊢ (xgcd 0 s).2 = 1

Tactic:
rw [xgcd, xgcd_zero_left]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
theorem inv_eq_self_iff [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1

Tactic:
simp only [Units.ext_iff]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1

Tactic:
exact mul_self_eq_one_iff

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1

Tactic:
rw [inv_eq_iff_mul_eq_one]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)

Tactic:
push_cast

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
u : Rˣ
⊢ ↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
-- Mathlib/Analysis/Convex/EGauge.lean
/-- If `c • x ∈ s`, then `egauge 𝕜 s x` is at most `‖c‖ₑ⁻¹`.

See also `egauge_le_of_smul_mem_of_ne`. -/
lemma egauge_le_of_smul_mem (h : c • x ∈ s) : egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Proof state:
case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : 0 • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖0‖ₑ⁻¹

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Result:
case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : 0 • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖0‖ₑ⁻¹

case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Proof state:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
exact (egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem Convex.cthickening (hs : Convex ℝ s) (δ : ℝ) : Convex ℝ (cthickening δ s)

Proof state:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_of_nonpos hδ]

Result:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)

Proof state:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)

Tactic:
exact hs.closure

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε s)

Tactic:
exact convex_iInter₂ fun _ _ => hs.thickening _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
obtain hδ | hδ := le_total 0 δ

Result:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)

case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)

Proof state:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
rw [cthickening_eq_iInter_thickening hδ]

Result:
case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem extract_zipWith : (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n)

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
m n : Nat
toList✝ : List α✝²
⊢ (zipWith f { toList := toList✝ } l').extract m n = zipWith f ({ toList := toList✝ }.extract m n) (l'.extract m n)

Tactic:
cases l'

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
toList✝¹ : List α✝²
toList✝ : List α✝¹
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).extract m n =
    zipWith f ({ toList := toList✝¹ }.extract m n) ({ toList := toList✝ }.extract m n)

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Array α✝¹
m n : Nat
⊢ (zipWith f l l').extract m n = zipWith f (l.extract m n) (l'.extract m n)

Tactic:
cases l

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
m n : Nat
toList✝ : List α✝²
⊢ (zipWith f { toList := toList✝ } l').extract m n = zipWith f ({ toList := toList✝ }.extract m n) (l'.extract m n)

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
m n : Nat
toList✝¹ : List α✝²
toList✝ : List α✝¹
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).extract m n =
    zipWith f ({ toList := toList✝¹ }.extract m n) ({ toList := toList✝ }.extract m n)

Tactic:
simp [List.drop_zipWith, List.take_zipWith]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem pretransitive_iff_unique_quotient_of_nonempty [Nonempty α] :
    IsPretransitive G α ↔ Nonempty (Unique <| orbitRel.Quotient G α)

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

Tactic:
rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]

Result:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ Subsingleton (orbitRel.Quotient G α) → Nonempty (orbitRel.Quotient G α)

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ Subsingleton (orbitRel.Quotient G α) → Nonempty (orbitRel.Quotient G α)

Tactic:
exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
    (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r)))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ i + r ≥ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r)))

Tactic:
simp [rotateLeftAux, getMsbD_or, show i + r ≥ w by omega, show ¬i < w - r by omega]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ w - r
⊢ ¬i < w - r

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Category/TopCat/EpiMono.lean
theorem mono_iff_injective {X Y : TopCat.{u}} (f : X ⟶ Y) : Mono f ↔ Function.Injective f

Proof state:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rw [this, CategoryTheory.mono_iff_injective]

Result:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ((forget TopCat).map f) ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
suffices Mono f ↔ Mono ((forget TopCat).map f) by
  rw [this, CategoryTheory.mono_iff_injective]
  rfl

Result:
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget TopCat).map f)

Proof state:
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ((forget TopCat).map f) ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f

Tactic:
apply Functor.mono_of_mono_map

Result:
no goals

Proof state:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Mono f
⊢ Mono ((forget TopCat).map f)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget TopCat).map f)

Tactic:
constructor

Result:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)

case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f

Proof state:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)

Tactic:
intro

Result:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Mono f
⊢ Mono ((forget TopCat).map f)
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem ord_cof (hf : IsFundamentalSequence a o f) :
    IsFundamentalSequence a a.cof.ord fun i hi => f i (hi.trans_le (by rw [hf.cof_eq]))

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ a.cof.ord ≤ o

Tactic:
rw [hf.cof_eq]

Result:
no goals

Proof state:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯

Tactic:
have H := hf.cof_eq

Result:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
⊢ a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯

Proof state:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
⊢ a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯

Tactic:
subst H

Result:
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯

Proof state:
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi => f i ⋯

Tactic:
exact hf

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem map_comp_C (f : R →+* S) : (map f).comp (C : R →+* MvPolynomial σ R) = C.comp f

Proof state:
case a
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x✝ : R
⊢ ((map f).comp C) x✝ = (C.comp f) x✝

Tactic:
apply map_C

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (map f).comp C = C.comp f

Tactic:
ext1

Result:
case a
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x✝ : R
⊢ ((map f).comp C) x✝ = (C.comp f) x✝
-- Mathlib/NumberTheory/GaussSum.lean
theorem FiniteField.two_pow_card {F : Type*} [Fintype F] [Field F] (hF : ringChar F ≠ 2) :
    (2 : F) ^ (Fintype.card F / 2) = χ₈ (Fintype.card F)

Proof state:
case intro.intro
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
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
have hq : IsQuadratic χ := isQuadratic_χ₈.comp _

Result:
case intro.intro
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
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
/-- If the topology on `α` is generated by its restrictions to compact sets, then the space of
continuous maps `C(α, β)` is complete (wrt the compact convergence uniformity).

Sufficient conditions on `α` to satisfy this condition are (weak) local compactness (see
`ContinuousMap.instCompleteSpaceOfWeaklyLocallyCompactSpace`) and sequential compactness (see
`ContinuousMap.instCompleteSpaceOfSequentialSpace`). -/
lemma completeSpace_of_restrictGenTopology (h : RestrictGenTopology {K : Set α | IsCompact K}) :
    CompleteSpace C(α, β)

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
h : RestrictGenTopology {K | IsCompact K}
⊢ CompleteSpace C(α, β)

Tactic:
rw [completeSpace_iff_isComplete_range
  isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing,
  range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete]

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
h : RestrictGenTopology {K | IsCompact K}
⊢ CompleteSpace ↑{f | Continuous f}

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
h : RestrictGenTopology {K | IsCompact K}
⊢ CompleteSpace ↑{f | Continuous f}

Tactic:
exact (UniformOnFun.isClosed_setOf_continuous h).completeSpace_coe

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma coweightEquiv_comp_toLin {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
    coweightEquiv P P (Equiv.comp x y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : N
⊢ (coweightEquiv P P (x.comp y)) x✝ = (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
⊢ coweightEquiv P P (x.comp y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : N
⊢ (coweightEquiv P P (x.comp y)) x✝ = (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) x✝
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.inl_map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.inl ≫ biprod.map f g = f ≫ biprod.inl

Proof state:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map f g = f ≫ inl

Tactic:
rw [biprod.map_eq_map']

Result:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map' f g = f ≫ inl

Proof state:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map' f g = f ≫ inl

Tactic:
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem disjoint_iff_comap_eq_bot {p q : Submodule R M} : Disjoint p q ↔ comap p.subtype q = ⊥

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ comap p.subtype q = ⊥

Tactic:
rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
  map_comap_subtype, map_bot, disjoint_iff]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma IsOfFinOrder.pow {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n)

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ (a ^ n) ^ m = 1

Tactic:
simp [pow_right_comm _ n, ha]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder a → IsOfFinOrder (a ^ n)

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]

Result:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ (∃ n, 0 < n ∧ a ^ n = 1) → ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ (∃ n, 0 < n ∧ a ^ n = 1) → ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Tactic:
rintro ⟨m, hm, ha⟩

Result:
case intro.intro
G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Proof state:
case intro.intro
G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Tactic:
exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
lemma vecMul_swap (i j : n) (a : n → R) :
    a ᵥ* swap R i j = a ∘ Equiv.swap i j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ a ᵥ* swap R i j = a ∘ ⇑(Equiv.swap i j)

Tactic:
simp [swap, PEquiv.vecMul_toMatrix_toPEquiv]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.real_toNNReal {f : α → ℝ} (hf : Integrable f μ) :
    Integrable (fun x => ((f x).toNNReal : ℝ)) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ < ⊤

Tactic:
refine lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x => ↑(f x).toNNReal) μ

Tactic:
refine
  ⟨hf.aestronglyMeasurable.aemeasurable.real_toNNReal.coe_nnreal_real.aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x => ↑(f x).toNNReal) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Tactic:
apply lintegral_mono

Result:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ (fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) ≤ fun a => ENNReal.ofReal ‖f a‖

Proof state:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ (fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x

Tactic:
simp [ENNReal.ofReal_le_ofReal, abs_le, le_abs_self]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x => ↑(f x).toNNReal) μ

Tactic:
rw [hasFiniteIntegral_iff_norm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ < ⊤

Proof state:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ (fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) ≤ fun a => ENNReal.ofReal ‖f a‖

Tactic:
intro x

Result:
case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ (fun a => ENNReal.ofReal ‖↑(f a).toNNReal‖) x ≤ (fun a => ENNReal.ofReal ‖f a‖) x