harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_sub_Y_add_Y_sub_negY {P Q : Fin 3 → R} (hx : P x * Q z = Q x * P z) :
    (P y * Q z - Q y * P z) + (P y * Q z - W'.negY Q * P z) = (P y - W'.negY P) * Q z

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - W'.negY P) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
rw [negY, negY]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - W'.negY Q * P z) = (P y - W'.negY P) * Q z

Tactic:
linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblXYZ_of_Y_eq {P Q : Fin 3 → F} (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) :
    W.dblXYZ P = W.dblU P • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.dblXYZ P = W.dblU P • ![1, 1, 0]

Tactic:
erw [dblXYZ_of_Y_eq' hQz hx hy hy', smul_fin3, mul_one, mul_one, mul_zero]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem coprodᵢ_eq_bot_iff' : Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥

Tactic:
simpa only [not_neBot, not_and_or, funext_iff, not_forall, not_exists, not_nonempty_iff]
  using coprodᵢ_neBot_iff'.not

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mul_right_eq_zero (u : M₀ˣ) {a : M₀} : ↑u * a = 0 ↔ a = 0 :=
  ⟨fun h => by simpa using mul_eq_zero_of_right (↑u⁻¹) h, mul_eq_zero_of_right (u : M₀)⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : ↑u * a = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_right (↑u⁻¹) h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Iio {a : ℝ} : volume (Iio a) = ∞ :=
  top_unique <|
    le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n =>
      calc
        (n : ℝ≥0∞) = volume (Ioo (a - n) a)

Proof state:
a : ℝ
n : ℕ
⊢ ↑n = volume (Ioo (a - ↑n) a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem Subsingleton.of_oneHomClass [Subsingleton M] [OneHomClass F M N] :
    Subsingleton F where
  allEq f g := DFunLike.ext _ _ fun x ↦ by simp [Subsingleton.elim x 1]

Proof state:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝⁴ : One M
inst✝³ : One N
inst✝² : FunLike F M N
inst✝¹ : Subsingleton M
inst✝ : OneHomClass F M N
f g : F
x : M
⊢ f x = g x

Tactic:
simp [Subsingleton.elim x 1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    get! m a = getD m a default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ get! m a = getD m a default

Tactic:
simp_to_raw using Raw₀.Const.get!_eq_getD_default

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem getElem?_idxOf [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) :
    l[idxOf a l]? = some a

Proof state:
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l[idxOf a l]? = some a

Tactic:
rw [getElem?_eq_getElem, getElem_idxOf (idxOf_lt_length_iff.2 h)]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasStrictFDerivAt_add_const_iff (c : F) :
    HasStrictFDerivAt (f · + c) f' x ↔ HasStrictFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun x => f x + c) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simp [hasStrictFDerivAt_iff_isLittleO]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Prime.pow_dvd_iff_dvd_ordProj {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ^ k ∣ n ↔ p ^ k ∣ ordProj[p] n

Proof state:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p

Tactic:
rw [pow_dvd_pow_iff_le_right pp.one_lt, pp.pow_dvd_iff_le_factorization hn]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_le_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b ≤ c ↔ a / c ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
this : MulPosMono G₀
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
rw [div_le_iff₀ hb, div_le_iff₀' hc]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
this : MulPosMono G₀
⊢ a / b ≤ c ↔ a / c ≤ b
-- Mathlib/Topology/PartitionOfUnity.lean
theorem continuous_toPOUFun (i : ι) : Continuous (f.toPOUFun i)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - (f i) x

Tactic:
simp only [mulSupport_one_sub]

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support ⇑(f i)

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support ⇑(f i)

Tactic:
exact f.locallyFinite

Result:
no goals

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ Continuous (f.toPOUFun i)

Tactic:
refine (f i).continuous.mul <|
  continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) ?_

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - (f i) x
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem neg {x y : S} (h : IsConjRoot K x y) :
    IsConjRoot K (-x) (-y)

Proof state:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
h : IsConjRoot K x y
⊢ IsConjRoot K (-x) (-y)

Tactic:
rw [isConjRoot_def, minpoly.neg x, minpoly.neg y, h]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
protected lemma add_eq_zero : ∀ {x y : PGame}, x + y ≡ 0 ↔ x ≡ 0 ∧ y ≡ 0
  | mk xl xr xL xR, mk yl yr yL yR => by
    simp_rw [identical_zero_iff, leftMoves_add, rightMoves_add, isEmpty_sum]
    tauto

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ mk xl xr xL xR + mk yl yr yL yR ≡ 0 ↔ mk xl xr xL xR ≡ 0 ∧ mk yl yr yL yR ≡ 0

Tactic:
simp_rw [identical_zero_iff, leftMoves_add, rightMoves_add, isEmpty_sum]

Result:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ (IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk yl yr yL yR).LeftMoves) ∧
      IsEmpty (mk xl xr xL xR).RightMoves ∧ IsEmpty (mk yl yr yL yR).RightMoves ↔
    (IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves) ∧
      IsEmpty (mk yl yr yL yR).LeftMoves ∧ IsEmpty (mk yl yr yL yR).RightMoves

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ (IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk yl yr yL yR).LeftMoves) ∧
      IsEmpty (mk xl xr xL xR).RightMoves ∧ IsEmpty (mk yl yr yL yR).RightMoves ↔
    (IsEmpty (mk xl xr xL xR).LeftMoves ∧ IsEmpty (mk xl xr xL xR).RightMoves) ∧
      IsEmpty (mk yl yr yL yR).LeftMoves ∧ IsEmpty (mk yl yr yL yR).RightMoves

Tactic:
tauto

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp₂Measurable_eq_mk (g : β → γ → δ) (hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β)
    (f₂ : α →ₘ[μ] γ) :
    comp₂Measurable g hg f₁ f₂ =
      mk (fun a => g (f₁ a) (f₂ a))
        (hg.comp_aemeasurable (f₁.aemeasurable.prod_mk f₂.aemeasurable)).aestronglyMeasurable

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ comp₂Measurable g hg f₁ f₂ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rw [comp₂Measurable_eq_pair, pair_eq_mk, compMeasurable_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x => (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
theorem exists_lt_rieszContentAux_add_pos (K : Compacts X) {ε : ℝ≥0} (εpos : 0 < ε) :
    ∃ f : C_c(X, ℝ≥0), (∀ x ∈ K, (1 : ℝ≥0) ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

Proof state:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ α < rieszContentAux Λ K + ε

Tactic:
exact α_hyp

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ Λ f < rieszContentAux Λ K + ε

Tactic:
rw [f_hyp.right]

Result:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ α < rieszContentAux Λ K + ε

Proof state:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

Tactic:
refine ⟨f, f_hyp.left, ?_⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ Λ f < rieszContentAux Λ K + ε

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

Tactic:
obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
  exists_lt_of_csInf_lt (rieszContentAux_image_nonempty Λ K)
    (lt_add_of_pos_right (rieszContentAux Λ K) εpos)

Result:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma leftUnitor_naturality (φ : X ⟶ X') :
    tensorHom (𝟙 (tensorUnit)) φ ≫ (leftUnitor X').hom =
      (leftUnitor X).hom ≫ φ

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X X' : GradedObject I C
φ : X ⟶ X'
⊢ tensorHom (𝟙 tensorUnit) φ ≫ (leftUnitor X').hom = (leftUnitor X).hom ≫ φ

Tactic:
apply mapBifunctorLeftUnitor_naturality

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_rev {x : BitVec w} {i : Fin w}:
    x[i.rev] = x.getMsbD i

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x[w - (↑i + 1)] = x.getLsbD (w - 1 - ↑i)

Tactic:
congr 1

Result:
case e_i
w : Nat
x : BitVec w
i : Fin w
⊢ w - (↑i + 1) = w - 1 - ↑i

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x[i.rev] = x.getMsbD ↑i

Tactic:
simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_true, Bool.true_and]

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ x[w - (↑i + 1)] = x.getLsbD (w - 1 - ↑i)

Proof state:
case e_i
w : Nat
x : BitVec w
i : Fin w
⊢ w - (↑i + 1) = w - 1 - ↑i

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
@[simp] lemma add_self_div_two (a : K) : (a + a) / 2 = a

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : NeZero 2
a : K
⊢ (a + a) / 2 = a

Tactic:
rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.lt_one_iff (a : BitVec n) (h : 0 < n) : (BitVec.ult a 1#n) = (a == 0#n)

Proof state:
n : Nat
a : BitVec n
h : 0 < n
⊢ a.ult 1#n = (a == 0#n)

Tactic:
rw [Bool.eq_iff_iff, beq_iff_eq, ← BitVec.lt_ult]

Result:
n : Nat
a : BitVec n
h : 0 < n
⊢ a < 1#n ↔ a = 0#n

Proof state:
n : Nat
a : BitVec n
h : 0 < n
⊢ a < 1#n ↔ a = 0#n

Tactic:
exact _root_.BitVec.lt_one_iff h

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
Relation between the completed L-function and the usual one (odd case).
We state it this way around so it holds at the poles of the gamma factor as well.
-/
lemma LFunction_eq_completed_div_gammaFactor_odd (hΦ : Φ.Odd) (s : ℂ) :
    LFunction Φ s = completedLFunction Φ s / Gammaℝ (s + 1)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ LFunction Φ s = completedLFunction Φ s / (s + 1).Gammaℝ

Tactic:
simp only [LFunction_def_odd hΦ, completedLFunction_def_odd hΦ, hurwitzZetaOdd, mul_div_assoc,
  sum_div]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Int.lean
theorem norm_natCast (n : ℕ) : ‖(n : ℤ)‖ = n

Proof state:
n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
simp [Int.norm_eq_abs]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem commutes' {m : ℕ} (hm : n ≤ m) (x : ZMod (p ^ m)) :
    truncate hm (zmodEquivTrunc p m x) = zmodEquivTrunc p n (ZMod.castHom (pow_dvd_pow p hm) _ x) :=
  show (truncate hm).comp (zmodEquivTrunc p m).toRingHom x = _ by rw [commutes _ _ hm]; rfl

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((truncate hm).comp (zmodEquivTrunc p m).toRingHom) x = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

Tactic:
rw [commutes _ _ hm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))) x =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : ZMod (p ^ m)
⊢ ((zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))) x =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem quasiSeparated_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] :
    QuasiSeparated f ↔ QuasiSeparatedSpace X

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ QuasiSeparated f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @QuasiSeparated)]

Result:
no goals
-- Mathlib/Algebra/Group/Prod.lean
theorem coprod_comp_inr : (f.coprod g).comp (inr M N) = g :=
  ext fun x => by simp [coprod_apply]

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ((f.coprod g).comp (inr M N)) x = g x

Tactic:
simp [coprod_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem _root_.CategoryTheory.Functor.ranges_directed (F : C ⥤ Type*) (j : C) :
    Directed (· ⊇ ·) fun f : Σ'i, i ⟶ j => Set.range (F.map f.2) := fun ⟨i, ij⟩ ⟨k, kj⟩ => by
  let ⟨l, li, lk, e⟩ := cospan ij kj
  refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩ <;> simp_rw [F.map_comp] <;> apply Set.range_comp_subset_range

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨i, ij⟩) ((fun f => Set.range (F.map f.snd)) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨k, kj⟩) ((fun f => Set.range (F.map f.snd)) z)

Tactic:
refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩ <;> simp_rw [F.map_comp] <;> apply Set.range_comp_subset_range

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
⊢ ∃ z,
    (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨i, ij⟩) ((fun f => Set.range (F.map f.snd)) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨k, kj⟩) ((fun f => Set.range (F.map f.snd)) z)

Tactic:
let ⟨l, li, lk, e⟩ := cospan ij kj

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
F : C ⥤ Type u_1
j : C
x✝¹ x✝ : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ ∃ z,
    (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨i, ij⟩) ((fun f => Set.range (F.map f.snd)) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun f => Set.range (F.map f.snd)) ⟨k, kj⟩) ((fun f => Set.range (F.map f.snd)) z)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem head?_drop (l : List α) (n : Nat) :
    (l.drop n).head? = l[n]?

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (drop n l).head? = l[n]?

Tactic:
rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.closure_eq_biUnion_inseparable {K : Set X} (hK : IsCompact K) :
    closure K = ⋃ x ∈ K, {y | Inseparable x y}

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
simp [hK.mem_closure_iff_exists_inseparable]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure K = ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
ext

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_addU {K : Type v} [Field K] (f : F →+* K) (P Q : Fin 3 → F) :
    addU (f ∘ P) (f ∘ Q) = f (addU P Q)

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -((⇑f ∘ P) y * (⇑f ∘ Q) z - (⇑f ∘ Q) y * (⇑f ∘ P) z) ^ 3 / ((⇑f ∘ P) z * (⇑f ∘ Q) z) =
    f (-(P y * Q z - Q y * P z) ^ 3 / (P z * Q z))

Tactic:
map_simp

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
simp only [addU]

Result:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -((⇑f ∘ P) y * (⇑f ∘ Q) z - (⇑f ∘ Q) y * (⇑f ∘ P) z) ^ 3 / ((⇑f ∘ P) z * (⇑f ∘ Q) z) =
    f (-(P y * Q z - Q y * P z) ^ 3 / (P z * Q z))
-- Mathlib/Topology/Constructions.lean
theorem isOpen_iff' {s : Set (CofiniteTopology X)} : IsOpen s ↔ s = ∅ ∨ sᶜ.Finite

Proof state:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsOpen s ↔ s = ∅ ∨ sᶜ.Finite

Tactic:
simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem minpolyGen_eq (pb : PowerBasis A S) : pb.minpolyGen = minpoly A pb.gen

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ pb.minpolyGen = minpoly A pb.gen

Tactic:
refine minpoly.unique' A _ pb.minpolyGen_monic pb.aeval_minpolyGen fun q hq =>
  or_iff_not_imp_left.2 fun hn0 h0 => ?_

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
q : A[X]
hq : q.degree < pb.minpolyGen.degree
hn0 : ¬q = 0
h0 : (aeval pb.gen) q = 0
⊢ False

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
q : A[X]
hq : q.degree < pb.minpolyGen.degree
hn0 : ¬q = 0
h0 : (aeval pb.gen) q = 0
⊢ False

Tactic:
exact (pb.dim_le_degree_of_root hn0 h0).not_lt (pb.degree_minpolyGen ▸ hq)

Result:
no goals

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.minpolyGen = minpoly A pb.gen

Tactic:
nontriviality A

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
a✝ : Nontrivial A
⊢ pb.minpolyGen = minpoly A pb.gen
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_add_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

Result:
no goals