harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem ofAIG_find_unique {aig : AIG α} (a : α) (ha : (ofAIG aig)[a]? = some n) :
    ∀ a', (ofAIG aig)[a']? = some n → a = a'

Proof state:
case intro
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig)[a]? = some n✝
a' : α
ha' : (ofAIG aig)[a']? = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'

Tactic:
apply Inv1.property <;> assumption

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig)[a]? = some n
⊢ ∀ (a' : α), (ofAIG aig)[a']? = some n → a = a'

Tactic:
intro a' ha'

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig)[a]? = some n
a' : α
ha' : (ofAIG aig)[a']? = some n
⊢ a = a'

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig)[a]? = some n
a' : α
ha' : (ofAIG aig)[a']? = some n
⊢ a = a'

Tactic:
rcases ofAIG.Inv1 aig with ⟨n, hn⟩

Result:
case intro
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig)[a]? = some n✝
a' : α
ha' : (ofAIG aig)[a']? = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_eq_two_iff (n : ℕ) : minFac n = 2 ↔ 2 ∣ n

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : succ 0 = n.minFac
⊢ False

Tactic:
rw [eq_comm, Nat.minFac_eq_one_iff] at this

Result:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : n = 1
⊢ False

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ n.minFac = 2

Tactic:
have lb := minFac_pos n

Result:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2

Proof state:
n : ℕ
⊢ n.minFac = 2 ↔ 2 ∣ n

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ n.minFac = 2 → 2 ∣ n

case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2

Tactic:
refine ub.eq_or_lt.resolve_right fun h' => ?_

Result:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ False

Proof state:
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False

Tactic:
exact not_lt_of_le (le_of_dvd lb h) h'

Result:
no goals

Proof state:
case mp
n : ℕ
h : n.minFac = 2
⊢ 2 ∣ n

Tactic:
rw [← h]

Result:
case mp
n : ℕ
h : n.minFac = 2
⊢ n.minFac ∣ n

Proof state:
case mp
n : ℕ
h : n.minFac = 2
⊢ n.minFac ∣ n

Tactic:
exact minFac_dvd n

Result:
no goals

Proof state:
case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Tactic:
intro h

Result:
case mpr
n : ℕ
h : 2 ∣ n
⊢ n.minFac = 2

Proof state:
case mp
n : ℕ
⊢ n.minFac = 2 → 2 ∣ n

Tactic:
intro h

Result:
case mp
n : ℕ
h : n.minFac = 2
⊢ 2 ∣ n

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ False

Tactic:
have := le_antisymm (Nat.succ_le_of_lt lb) (Nat.lt_succ_iff.mp h')

Result:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : succ 0 = n.minFac
⊢ False

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
this : n = 1
⊢ False

Tactic:
subst this

Result:
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False

Proof state:
case mpr
n : ℕ
h : 2 ∣ n
⊢ n.minFac = 2

Tactic:
have ub := minFac_le_of_dvd (le_refl 2) h

Result:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
⊢ n.minFac = 2
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma toAffine_slope_of_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) :
    W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
      (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))

Tactic:
field_simp [mul_ne_zero (mul_ne_zero hPz hQz) <| sub_ne_zero.mpr hx,
  mul_ne_zero (mul_ne_zero (pow_ne_zero 3 hPz) (pow_ne_zero 3 hQz)) <| sub_ne_zero.mpr hx]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - P z ^ 3 * Q y) * (P z ^ 2 * Q z ^ 2) * (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) * (P z ^ 3 * Q z ^ 3 * (P x * Q z ^ 2 - Q x * P z ^ 2))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ P x / P z ^ 2 ≠ Q x / Q z ^ 2

Tactic:
rwa [ne_eq, ← X_eq_iff hPz hQz]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Tactic:
rw [Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz],
  div_sub_div _ _ (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz), mul_comm <| _ ^ 2, addZ]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - P z ^ 3 * Q y) * (P z ^ 2 * Q z ^ 2) * (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) * (P z ^ 3 * Q z ^ 3 * (P x * Q z ^ 2 - Q x * P z ^ 2))

Tactic:
ring1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_false_of_not_eq_true {a : Prop} (h : (Not a) = True) : a = False

Proof state:
a : Prop
h : (¬a) = True
⊢ a = False

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem coe_spanSingleton (x : P) : (spanSingleton S x : Submodule R P) = span R {x}

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ ↑⟨span R {x}, ⋯⟩ = span R {x}

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ ↑(spanSingleton S x) = span R {x}

Tactic:
rw [spanSingleton]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ ↑⟨span R {x}, ⋯⟩ = span R {x}
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem gfpApprox_mono_left : Monotone (gfpApprox : (α →o α) → _)

Proof state:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
this : OrderHom.dual g ≤ OrderHom.dual f
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
exact lfpApprox_mono_left this

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
have : g.dual ≤ f.dual := h

Result:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
this : OrderHom.dual g ≤ OrderHom.dual f
⊢ gfpApprox f ≤ gfpApprox g

Proof state:
α : Type u
inst✝ : CompleteLattice α
⊢ Monotone gfpApprox

Tactic:
intro f g h

Result:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem half_le_self_iff : a / 2 ≤ a ↔ 0 ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
⊢ a / 2 ≤ a ↔ 0 ≤ a

Tactic:
rw [div_le_iff₀ (zero_lt_two' α), mul_two, le_add_iff_nonneg_left]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.eq_of_subset_indep (hB : M.IsBase B) (hI : M.Indep I) (hBI : B ⊆ I) : B = I :=
  let ⟨B', hB', hB'I⟩ := hI.exists_isBase_superset
  hBI.antisymm (by rwa [hB.eq_of_subset_isBase hB' (hBI.trans hB'I)])

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hB : M.IsBase B
hI : M.Indep I
hBI : B ⊆ I
B' : Set α
hB' : M.IsBase B'
hB'I : I ⊆ B'
⊢ I ⊆ B

Tactic:
rwa [hB.eq_of_subset_isBase hB' (hBI.trans hB'I)]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- Exactness of `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`. -/
lemma L₁'_exact : S.L₁'.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f

Tactic:
intro A₀ x₃ hx₃

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₁'.X₂
hx₃ : x₃ ≫ S.L₁'.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
-- Mathlib/Data/Finset/Image.lean
theorem mem_range_iff_mem_finset_range_of_mod_eq [DecidableEq α] {f : ℤ → α} {a : α} {n : ℕ}
    (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
    a ∈ Set.range f ↔ a ∈ (Finset.range n).image (fun (i : ℕ) => f i) :=
  suffices (∃ i, f (i % n) = a) ↔ ∃ i, i < n ∧ f ↑i = a by simpa [h]
  have hn' : 0 < (n : ℤ) := Int.ofNat_lt.mpr hn
  Iff.intro
    (fun ⟨i, hi⟩ =>
      have : 0 ≤ i % ↑n := Int.emod_nonneg _ (ne_of_gt hn')
      ⟨Int.toNat (i % n), by
        rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]; exact ⟨Int.emod_lt_of_pos i hn', hi⟩⟩)
    fun ⟨i, hi, ha⟩ =>
    ⟨i, by rw [Int.emod_eq_of_lt (Int.ofNat_zero_le _) (Int.ofNat_lt_ofNat_of_lt hi), ha]⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ i % ↑n < ↑n ∧ f (i % ↑n) = a

Tactic:
exact ⟨Int.emod_lt_of_pos i hn', hi⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ f (↑i % ↑n) = a

Tactic:
rw [Int.emod_eq_of_lt (Int.ofNat_zero_le _) (Int.ofNat_lt_ofNat_of_lt hi), ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
this : (∃ i, f (i % ↑n) = a) ↔ ∃ i < n, f ↑i = a
⊢ a ∈ Set.range f ↔ a ∈ image (fun i => f ↑i) (range n)

Tactic:
simpa [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ (i % ↑n).toNat < n ∧ f ↑(i % ↑n).toNat = a

Tactic:
rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]

Result:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ i % ↑n < ↑n ∧ f (i % ↑n) = a
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticWithinAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} {t : Set F} {s : Set E}
    (hg : AnalyticWithinAt 𝕜 g t y) (hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t)
    (hy : f x = y) :
    AnalyticWithinAt 𝕜 (g ∘ f) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact hg.comp hf h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t y
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
rw [← hy] at hg

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem children_mk {a} (x : F.B a → M F) (i : F.B (head (M.mk ⟨a, x⟩))) :
    children (M.mk ⟨a, x⟩) i = x (cast (by rw [head_mk]) i)

Proof state:
case H
F : PFunctor.{u}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ ∀ (i_1 : ℕ), ((M.mk ⟨a, x⟩).children i).approx i_1 = (x (cast ⋯ i)).approx i_1

Tactic:
intro n

Result:
case H
F : PFunctor.{u}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
n : ℕ
⊢ ((M.mk ⟨a, x⟩).children i).approx n = (x (cast ⋯ i)).approx n

Proof state:
F : PFunctor.{u}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ (M.mk ⟨a, x⟩).children i = x (cast ⋯ i)

Tactic:
apply ext'

Result:
case H
F : PFunctor.{u}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ ∀ (i_1 : ℕ), ((M.mk ⟨a, x⟩).children i).approx i_1 = (x (cast ⋯ i)).approx i_1

Proof state:
case H
F : PFunctor.{u}
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
n : ℕ
⊢ ((M.mk ⟨a, x⟩).children i).approx n = (x (cast ⋯ i)).approx n

Tactic:
rfl

Result:
no goals

Proof state:
F : PFunctor.{u}
X : Type u_1
f : X → ↑F X
a : F.A
x : F.B a → F.M
i : F.B (M.mk ⟨a, x⟩).head
⊢ F.B (M.mk ⟨a, x⟩).head = F.B a

Tactic:
rw [head_mk]

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
lemma gammaCDFReal_eq_lintegral {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (x : ℝ) :
    gammaCDFReal a r x = ENNReal.toReal (∫⁻ x in Iic x, gammaPDF a r x)

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ((gammaMeasure a r) (Iic x)).toReal = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal

Tactic:
simp only [gammaMeasure, measurableSet_Iic, withDensity_apply, gammaPDF]

Result:
no goals

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ↑(gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal

Tactic:
simp only [gammaPDF, gammaCDFReal, cdf_eq_toReal]

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ((gammaMeasure a r) (Iic x)).toReal = (∫⁻ (x : ℝ) in Iic x, ENNReal.ofReal (gammaPDFReal a r x)).toReal

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ ↑(gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal

Tactic:
have : IsProbabilityMeasure (gammaMeasure a r) := isProbabilityMeasureGamma ha hr

Result:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ↑(gammaCDFReal a r) x = (∫⁻ (x : ℝ) in Iic x, gammaPDF a r x).toReal
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem setIntegral_condExpIndSMul (hs : MeasurableSet[m] s) (ht : MeasurableSet t)
    (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) (x : G') :
    ∫ a in s, (condExpIndSMul hm ht hμt x) a ∂μ = (μ (t ∩ s)).toReal • x :=
  calc
    ∫ a in s, (condExpIndSMul hm ht hμt x) a ∂μ =
        ∫ a in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) a • x ∂μ :=
      setIntegral_congr_ae (hm s hs)
        ((condExpIndSMul_ae_eq_smul hm ht hμt x).mono fun _ hx _ => hx)
    _ = (∫ a in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) a ∂μ) • x :=
      (integral_smul_const _ x)
    _ = (μ (t ∩ s)).toReal • x

Proof state:
α : Type u_1
G' : Type u_6
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : CompleteSpace G'
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
x : G'
⊢ (∫ (a : α) in s, ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)) a ∂μ) • x = (μ (t ∩ s)).toReal • x

Tactic:
rw [setIntegral_condExpL2_indicator hs ht hμs hμt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_reverse {l : List α} : l.reverse.any f = l.any f

Proof state:
α : Type u_1
f : α → Bool
l : List α
⊢ l.reverse.any f = l.any f

Tactic:
induction l <;> simp_all [Bool.or_comm]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem identical_of_isEmpty (x y : PGame)
    [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves]
    [IsEmpty y.LeftMoves] [IsEmpty y.RightMoves] : x ≡ y :=
  identical_iff.2 (by simp [biTotal_empty])

Proof state:
x y : PGame
inst✝³ : IsEmpty x.LeftMoves
inst✝² : IsEmpty x.RightMoves
inst✝¹ : IsEmpty y.LeftMoves
inst✝ : IsEmpty y.RightMoves
⊢ (Relator.BiTotal fun x1 x2 => x.moveLeft x1 ≡ y.moveLeft x2) ∧
    Relator.BiTotal fun x1 x2 => x.moveRight x1 ≡ y.moveRight x2

Tactic:
simp [biTotal_empty]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma density_fst_univ (κ : Kernel α (γ × β)) [IsFiniteKernel κ] (a : α) :
    ∀ᵐ x ∂(fst κ a), density κ (fst κ) a x univ = 1

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
x : γ
hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1
⊢ κ.density κ.fst a x univ = 1

Tactic:
simp [density, hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
rw [← ae_all_iff] at h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
have h := fun n ↦ densityProcess_fst_univ_ae κ n a

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ (n : ℕ), ∀ᵐ (x : γ) ∂κ.fst a, κ.densityProcess κ.fst n a x univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
filter_upwards [h] with x hx

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
x : γ
hx : ∀ (i : ℕ), κ.densityProcess κ.fst i a x univ = 1
⊢ κ.density κ.fst a x univ = 1
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem le_insertNth_iff {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
    q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j => q (i.succAbove j)) ≤ p

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toPlus_apply {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : Meq P S) (I : S.Arrow) :
    (J.toPlus P).app _ (x I) = (J.plusObj P).map I.f.op (mk x)

Proof state:
case h.h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) (↑x I) = ↑x (Cover.Arrow.base i)

Tactic:
simpa using (x.condition (Cover.Relation.mk' (I.precompRelation i.f))).symm

Result:
no goals

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯)) (↑x I)) =
    (ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x)

Tactic:
apply Concrete.multiequalizer_ext (C := D)

Result:
case h.h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ ∀ (t : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L),
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t))
        ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
          ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 => P.map I_1.f.op) ⋯))
            (↑x I))) =
      (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) t))
        ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mul_left (m₁ m₂ n : ℕ) : qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

Proof state:
m₁ m₂ n : ℕ
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

Tactic:
simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]

Result:
no goals