harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k : α} : containsKey k l = (l.map Sigma.fst).contains k

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : containsKey k tl = (List.map Sigma.fst tl).contains k
⊢ (hd.fst == k || (List.map Sigma.fst tl).contains k) = (k == hd.fst || (List.map Sigma.fst tl).contains k)

Tactic:
rw [BEq.comm]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
⊢ containsKey k [] = (List.map Sigma.fst []).contains k

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
⊢ containsKey k l = (List.map Sigma.fst l).contains k

Tactic:
induction l with
| nil => simp
| cons hd tl ih =>
  rw [containsKey_cons, ih]
  simp only [List.map_cons, List.contains_cons]
  rw [BEq.comm]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : containsKey k tl = (List.map Sigma.fst tl).contains k
⊢ (hd.fst == k || (List.map Sigma.fst tl).contains k) = (List.map Sigma.fst (hd :: tl)).contains k

Tactic:
simp only [List.map_cons, List.contains_cons]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : containsKey k tl = (List.map Sigma.fst tl).contains k
⊢ (hd.fst == k || (List.map Sigma.fst tl).contains k) = (k == hd.fst || (List.map Sigma.fst tl).contains k)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : containsKey k tl = (List.map Sigma.fst tl).contains k
⊢ containsKey k (hd :: tl) = (List.map Sigma.fst (hd :: tl)).contains k

Tactic:
rw [containsKey_cons, ih]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : containsKey k tl = (List.map Sigma.fst tl).contains k
⊢ (hd.fst == k || (List.map Sigma.fst tl).contains k) = (List.map Sigma.fst (hd :: tl)).contains k
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_of_card_lt [Fintype α] (hc : card α < n) : G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬G.CliqueFree n
⊢ False

Tactic:
refine Nat.lt_le_asymm hc ?_

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬G.CliqueFree n
⊢ n ≤ Fintype.card α

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
⊢ G.CliqueFree n

Tactic:
by_contra h

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬G.CliqueFree n
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : ¬G.CliqueFree n
⊢ n ≤ Fintype.card α

Tactic:
rw [cliqueFree_iff, not_isEmpty_iff] at h

Result:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : Nonempty (⊤ ↪g G)
⊢ n ≤ Fintype.card α

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : Fintype α
hc : Fintype.card α < n
h : Nonempty (⊤ ↪g G)
⊢ n ≤ Fintype.card α

Tactic:
simpa only [Fintype.card_fin] using Fintype.card_le_of_embedding h.some.toEmbedding

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma curry_obj_uncurry_obj (F : B ⥤ C ⥤ D) : curry.obj (uncurry.obj F) = F :=
  Functor.ext (fun _ => Functor.ext (by simp) (by simp)) (by aesop_cat)

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B ⥤ C ⥤ D
x✝ : B
⊢ ∀ (X : C), ((curry.obj (uncurry.obj F)).obj x✝).obj X = (F.obj x✝).obj X

Tactic:
simp

Result:
no goals

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B ⥤ C ⥤ D
⊢ ∀ (X Y : B) (f : X ⟶ Y), (curry.obj (uncurry.obj F)).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
aesop_cat

Result:
no goals

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B ⥤ C ⥤ D
x✝ : B
⊢ ∀ (X Y : C) (f : X ⟶ Y), ((curry.obj (uncurry.obj F)).obj x✝).map f = eqToHom ⋯ ≫ (F.obj x✝).map f ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
/-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are sets of vertices such
that each pair is `ε`-uniform and `2 * ε`-dense, then a proportion of at least
`(1 - 2 * ε) * ε ^ 3` of the triples `(a, b, c) ∈ s × t × u` are triangles. -/
lemma triangle_counting'
    (dst : 2 * ε ≤ G.edgeDensity s t) (hst : G.IsUniform ε s t)
    (dsu : 2 * ε ≤ G.edgeDensity s u) (usu : G.IsUniform ε s u)
    (dtu : 2 * ε ≤ G.edgeDensity t u) (utu : G.IsUniform ε t u) :
    (1 - 2 * ε) * ε ^ 3 * #s * #t * #u ≤
      #((s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
          (s ×ˢ t ×ˢ u)))

Tactic:
have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
          (s ×ˢ t ×ˢ u)))
-- Mathlib/Order/Rel/GaloisConnection.lean
theorem rightDual_leftDual_le_of_le {J J' : Set α} (h : J' ∈ R.leftFixedPoints) (h₁ : J ≤ J') :
    R.rightDual (R.leftDual J) ≤ J'

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ (fun b => ∀ ⦃a : α⦄, a ∈ J → R a b) ≤ fun b => ∀ ⦃a : α⦄, a ∈ J' → R a b

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Result:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ J ≤ J'

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Result:
case a
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ (fun b => ∀ ⦃a : α⦄, a ∈ J → R a b) ≤ fun b => ∀ ⦃a : α⦄, a ∈ J' → R a b

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ R.rightDual (R.leftDual J) ≤ J'

Tactic:
rw [← h]

Result:
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')

Proof state:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ≤ J'
⊢ J ≤ J'

Tactic:
exact h₁

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋ = Nat.sqrt a

Proof state:
a : ℕ
⊢ ↑↑a.sqrt ≤ √↑a ∧ √↑a < ↑↑a.sqrt + 1

Tactic:
exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

Result:
no goals

Proof state:
a : ℕ
⊢ ⌊√↑a⌋ = ↑a.sqrt

Tactic:
rw [Int.floor_eq_iff]

Result:
a : ℕ
⊢ ↑↑a.sqrt ≤ √↑a ∧ √↑a < ↑↑a.sqrt + 1
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- There is a character of order `n` on `F` if `#F ≡ 1 mod n` and the target contains
a primitive `n`th root of unity. -/
lemma exists_mulChar_orderOf {n : ℕ} (h : n ∣ Fintype.card F - 1) {ζ : R}
    (hζ : IsPrimitiveRoot ζ n) :
    ∃ χ : MulChar F R, orderOf χ = n

Proof state:
case h.refine_2
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h✝ : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
m : ℕ
hm : m < n
hm₀ : 0 < m
h : ↑ζ' ^ m = 1
⊢ False

Tactic:
exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false

Result:
no goals

Proof state:
case h.refine_1.a.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ↑↑(⟨ζ', ⋯⟩ ^ n) = ↑↑1

Tactic:
push_cast

Result:
case h.refine_1.a.a
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ↑ζ' ^ n = 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ∃ χ, orderOf χ = n

Tactic:
use e.symm ⟨ζ', (mem_rootsOfUnity (Fintype.card Fˣ) ζ').mpr h'⟩

Result:
case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ orderOf (e.symm ⟨ζ', ⋯⟩) = n

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
⊢ ∃ χ, orderOf χ = n

Tactic:
let ζ' : Rˣ := (hζ.isUnit hn₀).unit

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
⊢ ∃ χ, orderOf χ = n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertManyIfNewUnit_list
    {l : List α} {k : α} :
    get! (insertManyIfNewUnit m l) k = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
l : List α
k : α
⊢ get! (insertManyIfNewUnit m l) k = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Height.lean
theorem chainHeight_dual : (ofDual ⁻¹' s).chainHeight = s.chainHeight

Proof state:
case a
α : Type u_1
inst✝ : LT α
s : Set α
⊢ s.chainHeight ≤ (⇑ofDual ⁻¹' s).chainHeight

Tactic:
rw [chainHeight_le_chainHeight_iff]

Result:
case a
α : Type u_1
inst✝ : LT α
s : Set α
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (⇑ofDual ⁻¹' s).subchain, l.length = l'.length

Proof state:
case a
α : Type u_1
inst✝ : LT α
s : Set α
⊢ ∀ l ∈ s.subchain, ∃ l' ∈ (⇑ofDual ⁻¹' s).subchain, l.length = l'.length

Tactic:
rintro l ⟨h₁, h₂⟩

Result:
case a.intro
α : Type u_1
inst✝ : LT α
s : Set α
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
⊢ ∃ l' ∈ (⇑ofDual ⁻¹' s).subchain, l.length = l'.length

Proof state:
case a.intro
α : Type u_1
inst✝ : LT α
s : Set α
l : List α
h₁ : Chain' (fun x1 x2 => x1 < x2) l
h₂ : ∀ i ∈ l, i ∈ s
⊢ ∃ l' ∈ (⇑ofDual ⁻¹' s).subchain, l.length = l'.length

Tactic:
exact ⟨l.reverse, ⟨chain'_reverse.mpr h₁, fun i h ↦ h₂ i (mem_reverse.mp h)⟩,
  (length_reverse _).symm⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem ofReal_normSq_eq_inner_self (x : F) : (normSqF x : 𝕜) = ⟪x, x⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ↑(normSq x) = re ⟪x, x⟫_𝕜 ∧ im ↑(normSq x) = im ⟪x, x⟫_𝕜

Tactic:
exact ⟨by simp only [ofReal_re]; rfl, by simp only [inner_self_im, ofReal_im]⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ↑(normSq x) = re ⟪x, x⟫_𝕜

Tactic:
simp only [ofReal_re]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ normSq x = re ⟪x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ ↑(normSq x) = ⟪x, x⟫_𝕜

Tactic:
rw [ext_iff]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ↑(normSq x) = re ⟪x, x⟫_𝕜 ∧ im ↑(normSq x) = im ⟪x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ im ↑(normSq x) = im ⟪x, x⟫_𝕜

Tactic:
simp only [inner_self_im, ofReal_im]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ normSq x = re ⟪x, x⟫_𝕜

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem norm_fst (a : 𝓜(𝕜, A)) : ‖a.fst‖ = ‖a‖

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.1‖ = ‖a‖

Tactic:
simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem norm_cexp_neg_mul_sq_add_mul_I' (hb : b.re ≠ 0) (c T : ℝ) :
    ‖cexp (-b * (T + c * I) ^ 2)‖ =
      exp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Proof state:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ (b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2) * (b.re ^ 2 * b.re) =
    b.re * (T * b.re - b.im * c) ^ 2 * b.re - b.re ^ 2 * (c ^ 2 * (b.im ^ 2 + b.re * b.re))

Tactic:
ring

Result:
no goals

Proof state:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Tactic:
have :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 =
    b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re) := by
  field_simp; ring

Result:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Proof state:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)
⊢ ‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

Tactic:
rw [norm_cexp_neg_mul_sq_add_mul_I, this]

Result:
no goals

Proof state:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 = b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)

Tactic:
field_simp

Result:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ (b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2) * (b.re ^ 2 * b.re) =
    b.re * (T * b.re - b.im * c) ^ 2 * b.re - b.re ^ 2 * (c ^ 2 * (b.im ^ 2 + b.re * b.re))
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isNormal_beth : IsNormal (ord ∘ beth)

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, (ord ∘ ℶ_ ) b ≤ a
⊢ (ord ∘ ℶ_ ) o ≤ a

Tactic:
rw [comp_apply, beth_limit ho, ord_le]

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, (ord ∘ ℶ_ ) b ≤ a
⊢ ⨆ a, ℶ_ ↑a ≤ a.card

Proof state:
⊢ IsNormal (ord ∘ ℶ_ )

Tactic:
refine (isNormal_iff_strictMono_limit _).2
  ⟨ord_strictMono.comp beth_strictMono, fun o ho a ha ↦ ?_⟩

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, (ord ∘ ℶ_ ) b ≤ a
⊢ (ord ∘ ℶ_ ) o ≤ a

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, (ord ∘ ℶ_ ) b ≤ a
⊢ ⨆ a, ℶ_ ↑a ≤ a.card

Tactic:
exact ciSup_le' fun b => ord_le.1 (ha _ b.2)

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem reverse_foldl {l : List α} : reverse (foldl (fun t h => h :: t) [] l) = l

Proof state:
α : Type u
l : List α
⊢ (foldl (fun t h => h :: t) [] l).reverse = l

Tactic:
simp

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem snd_diag {α : TypeVec n} : TypeVec.prod.snd ⊚ (prod.diag : α ⟹ _) = id

Proof state:
case h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.snd ⊚ prod.diag) i = id i

Tactic:
induction i with
| fz => rfl
| fs _ i_ih => apply i_ih

Result:
no goals

Proof state:
case h.fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
rfl

Result:
no goals

Proof state:
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.snd ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
apply i_ih

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
⊢ prod.snd ⊚ prod.diag = id

Tactic:
funext i

Result:
case h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.snd ⊚ prod.diag) i = id i
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem ofReal_integral_norm_eq_lintegral_enorm {P : Type*} [NormedAddCommGroup P] {f : α → P}
    (hf : Integrable f μ) : ENNReal.ofReal (∫ x, ‖f x‖ ∂μ) = ∫⁻ x, ‖f x‖ₑ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ⊤

Tactic:
exact lt_top_iff_ne_top.mp (hasFiniteIntegral_iff_enorm.mpr hf.2)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ⊤
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem type_cardinal : typeLT Cardinal = Ordinal.univ.{u, u + 1}

Proof state:
⊢ (type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}

Tactic:
rw [Ordinal.univ_id]

Result:
⊢ (type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2

Proof state:
⊢ (type fun x1 x2 => x1 < x2) = type fun x1 x2 => x1 < x2

Tactic:
exact Quotient.sound ⟨preAleph.symm.toRelIsoLT⟩

Result:
no goals
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Iic (a : ℕ) : (↑) '' Iic a = Icc (0 : ℤ) a

Proof state:
a : ℕ
⊢ Icc ↑⊥ ↑a = Icc 0 ↑a

Tactic:
rfl

Result:
no goals

Proof state:
a : ℕ
⊢ Nat.cast '' Iic a = Icc 0 ↑a

Tactic:
rw [← Icc_bot, image_cast_int_Icc]

Result:
a : ℕ
⊢ Icc ↑⊥ ↑a = Icc 0 ↑a
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_openCover (H : ∀ i, P (𝒰.map i ≫ f)) : P f

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
i : 𝒰.J
⊢ P (𝒰.map i ≫ f)

Tactic:
exact H i

Result:
no goals

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
i : 𝒰.J
⊢ P (((fun i => Scheme.Hom.opensRange (𝒰.map i)) i).ι ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.map i) (Scheme.Opens.ι _)
  (congr_arg Opens.carrier (𝒰.map i).opensRange.opensRange_ι.symm), Category.assoc,
  P.cancel_left_of_respectsIso]

Result:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
i : 𝒰.J
⊢ P (𝒰.map i ≫ f)

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
⊢ P f

Tactic:
refine of_iSup_eq_top (fun i ↦ (𝒰.map i).opensRange) 𝒰.iSup_opensRange fun i ↦ ?_

Result:
P : MorphismProperty Scheme
inst✝ : IsLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
i : 𝒰.J
⊢ P (((fun i => Scheme.Hom.opensRange (𝒰.map i)) i).ι ≫ f)
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.gcd_mul_right_cancel (m : ℕ+) {n k : ℕ+} :
    k.Coprime n → (m * k).gcd n = m.gcd n

Proof state:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n

Tactic:
apply Coprime.gcd_mul_left_cancel

Result:
no goals

Proof state:
m n k : ℕ+
⊢ k.Coprime n → (m * k).gcd n = m.gcd n

Tactic:
rw [mul_comm]

Result:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n
-- Mathlib/CategoryTheory/Sites/Canonical.lean
theorem of_isSheaf_yoneda_obj (J : GrothendieckTopology C)
    (h : ∀ X, Presieve.IsSheaf J (yoneda.obj X)) : Subcanonical J where
  le_canonical := le_finestTopology _ _ (by rintro P ⟨X, rfl⟩; apply h)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), Presieve.IsSheaf J (yoneda.obj X)
⊢ ∀ P ∈ Set.range yoneda.obj, Presieve.IsSheaf J P

Tactic:
rintro P ⟨X, rfl⟩

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), Presieve.IsSheaf J (yoneda.obj X)
X : C
⊢ Presieve.IsSheaf J (yoneda.obj X)

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), Presieve.IsSheaf J (yoneda.obj X)
X : C
⊢ Presieve.IsSheaf J (yoneda.obj X)

Tactic:
apply h

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem setLIntegral_preimage_condDistrib (hX : Measurable X) (hY : AEMeasurable Y μ)
    (hs : MeasurableSet s) (ht : MeasurableSet t) :
    ∫⁻ a in X ⁻¹' t, condDistrib Y X μ (X a) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ lintegral (μ.restrict (X ⁻¹' t)) ((fun a => ((condDistrib Y X μ) a) s) ∘ X) = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
rw [lintegral_comp (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, ←
  Measure.fst_map_prod_mk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
  Measure.map_apply_of_aemeasurable (hX.aemeasurable.prod_mk hY) (ht.prod hs), mk_preimage_prod]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
conv_lhs => arg 2; change (fun a => ((condDistrib Y X μ) a) s) ∘ X

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ lintegral (μ.restrict (X ⁻¹' t)) ((fun a => ((condDistrib Y X μ) a) s) ∘ X) = μ (X ⁻¹' t ∩ Y ⁻¹' s)