harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructions.lean
lemma isClosed_preimage_val {s t : Set X} : IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t

Tactic:
rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image,
  ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe,
  Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff,
  and_iff_right]

Result:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure (s ∩ t) ⊆ s

X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure (s ∩ t)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ closure (s ∩ t) ⊆ s

X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∩ t ⊆ s ∩ closure (s ∩ t)

Tactic:
exacts [Set.inter_subset_left, Set.subset_inter Set.inter_subset_left subset_closure]

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_insert {a : ∀ i, α i} :
    s.sigma (fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
a : (i : ι) → α i
⊢ (s.sigma fun i => insert (a i) (t i)) = (fun i => ⟨i, a i⟩) '' s ∪ s.sigma t

Tactic:
simp_rw [insert_eq, sigma_union, sigma_singleton]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem smul_orthogonalProjection_singleton {v : E} (w : E) :
    ((‖v‖ ^ 2 : ℝ) : 𝕜) • (orthogonalProjection (𝕜 ∙ v) w : E) = ⟪v, w⟫ • v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
this : ↑((orthogonalProjection (Submodule.span 𝕜 {v})) (↑‖v‖ ^ 2 • w)) = ⟪v, w⟫_𝕜 • v
⊢ ↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v

Tactic:
simpa using this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) (↑‖v‖ ^ 2 • w)) = ⟪v, w⟫_𝕜 • v

Tactic:
apply eq_orthogonalProjection_of_mem_of_inner_eq_zero

Result:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫_𝕜 • v ∈ Submodule.span 𝕜 {v}

case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ Submodule.span 𝕜 {v}, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫_𝕜 • v, w_1⟫_𝕜 = 0

Proof state:
case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ w_1 ∈ Submodule.span 𝕜 {v}, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫_𝕜 • v, w_1⟫_𝕜 = 0

Tactic:
rw [← Submodule.mem_orthogonal', Submodule.mem_orthogonal_singleton_iff_inner_left]

Result:
case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫_𝕜 • v, v⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v

Tactic:
suffices ((orthogonalProjection (𝕜 ∙ v) (((‖v‖ : 𝕜) ^ 2) • w)) : E) = ⟪v, w⟫ • v by
  simpa using this

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ↑((orthogonalProjection (Submodule.span 𝕜 {v})) (↑‖v‖ ^ 2 • w)) = ⟪v, w⟫_𝕜 • v

Proof state:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫_𝕜 • v ∈ Submodule.span 𝕜 {v}

Tactic:
rw [Submodule.mem_span_singleton]

Result:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∃ a, a • v = ⟪v, w⟫_𝕜 • v

Proof state:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ∃ a, a • v = ⟪v, w⟫_𝕜 • v

Tactic:
use ⟪v, w⟫

Result:
no goals

Proof state:
case hvo
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫_𝕜 • v, v⟫_𝕜 = 0

Tactic:
simp [inner_sub_left, inner_smul_left, inner_self_eq_norm_sq_to_K, mul_comm]

Result:
no goals
-- Mathlib/Probability/Integration.lean
theorem IndepFun.integrable_right_of_integrable_mul {β : Type*} [MeasurableSpace β] {X Y : Ω → β}
    [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (h'XY : Integrable (X * Y) μ)
    (hX : AEStronglyMeasurable X μ) (hY : AEStronglyMeasurable Y μ) (h'X : ¬X =ᵐ[μ] 0) :
    Integrable Y μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
⊢ HasFiniteIntegral Y μ

Tactic:
refine lt_top_iff_ne_top.2 fun H => ?_

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_2
inst✝² : MeasurableSpace β
X Y : Ω → β
inst✝¹ : NormedDivisionRing β
inst✝ : BorelSpace β
hXY : IndepFun X Y μ
h'XY : Integrable (X * Y) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
I : ∫⁻ (ω : Ω), ‖X ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖Y a‖ₑ ∂μ = ⊤
⊢ False
-- Mathlib/Algebra/Order/Floor.lean
theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
  sub_lt_iff_lt_add.2 <| by
    rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
    exact lt_floor_add_one _

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a < b + ↑⌊a / b⌋ * b

Tactic:
rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]

Result:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b a : k
hb : 0 < b
⊢ a / b < ↑⌊a / b⌋ + 1

Tactic:
exact lt_floor_add_one _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_prod_X_sub_C (s : Finset R) : (s.prod fun a => X - C a).roots = s.val

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ ∏ a ∈ s, (X - C a) ≠ 0

Tactic:
refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (∏ a ∈ s, (X - C a)).roots = s.val

Tactic:
apply (roots_prod (fun a => X - C a) s ?_).trans

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i => (X - C i).roots) = s.val

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ ∏ a ∈ s, (X - C a) ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i => (X - C i).roots) = s.val

Tactic:
simp_rw [roots_X_sub_C]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i => {i}) = s.val

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i => {i}) = s.val

Tactic:
rw [Multiset.bind_singleton, Multiset.map_id']

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem tail_update_zero : tail (update q 0 z) = tail q

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
⊢ tail (update q 0 z) = tail q

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
j : Fin n
⊢ tail (update q 0 z) j = tail q j

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
j : Fin n
⊢ tail (update q 0 z) j = tail q j

Tactic:
simp [tail, Fin.succ_ne_zero]

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_ediv_neg {a b q q' : ℤ} (h : IsInt (a / -b) q) (hq : -q = q') : IsInt (a / b) q' :=
  ⟨by rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]⟩

Proof state:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = ↑q'

Tactic:
rw [Int.cast_id, ← hq, ← @Int.cast_id q, ← h.out, ← Int.ediv_neg, Int.neg_neg]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma exists_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The transformation on ℂ that is used for `scale` maps the closed strip ``re ⁻¹' [l, u]``
  to the closed strip ``re ⁻¹' [0, 1]``. -/
lemma scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip {l u : ℝ} (hul : l < u) {z : ℂ}
    (hz : z ∈ verticalClosedStrip 0 1) : l + z * (u - l) ∈ verticalClosedStrip l u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ z.re * (u - l) ≤ u - l

Tactic:
nth_rewrite 2 [← one_mul (u - l)]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ z.re * (u - l) ≤ 1 * (u - l)

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
this : 0 ≤ u - l
⊢ z.re * (u - l) ≤ 1 * (u - l)

Tactic:
gcongr

Result:
no goals

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalClosedStrip l u

Tactic:
simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
  ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc, le_add_iff_nonneg_right]

Result:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Tactic:
simp only [verticalClosedStrip, mem_preimage, mem_Icc] at hz

Result:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ l + z.re * (u - l) ≤ u

Tactic:
rw [add_comm, ← sub_le_sub_iff_right l, add_sub_assoc, sub_self, add_zero]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ z.re * (u - l) ≤ u - l

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Tactic:
simp only [sub_pos, hul, mul_nonneg_iff_of_pos_right, hz₁, true_and]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ l + z.re * (u - l) ≤ u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ z.re * (u - l) ≤ 1 * (u - l)

Tactic:
have := sub_nonneg.2 hul.le

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
this : 0 ≤ u - l
⊢ z.re * (u - l) ≤ 1 * (u - l)

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Tactic:
obtain ⟨hz₁, hz₂⟩ := hz

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 ≤ z.re
hz₂ : z.re ≤ 1
⊢ 0 ≤ z.re * (u - l) ∧ l + z.re * (u - l) ≤ u
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem beq_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' == rhs') = (lhs == rhs)

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' == rhs') = (lhs == rhs)

Tactic:
simp[*]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem induction_on {P : RatFunc K → Prop} (x : RatFunc K)
    (f : ∀ (p q : K[X]) (_ : q ≠ 0), P (algebraMap _ (RatFunc K) p / algebraMap _ _ q)) : P x :=
  x.induction_on' fun p q hq => by simpa using f p q hq

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : RatFunc K → Prop
x : RatFunc K
f : ∀ (p q : K[X]), q ≠ 0 → P ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q)
p q : K[X]
hq : q ≠ 0
⊢ P (RatFunc.mk p q)

Tactic:
simpa using f p q hq

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem repr_fract_apply (m : E) (i : ι) : b.repr (fract b m) i = Int.fract (b.repr m i)

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr (fract b m)) i = Int.fract ((b.repr m) i)

Tactic:
rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_ofNat (n : ℕ) : W.Φ (n + 1) =
    X * W.preΨ' (n + 1) ^ 2 * (if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * (if Even n then W.Ψ₂Sq else 1)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.Φ (↑n + 1) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Tactic:
rw [Φ, ← Nat.cast_one, ← Nat.cast_add, ΨSq_ofNat, ← mul_assoc, ← Nat.cast_add, preΨ_ofNat,
  Nat.cast_add, add_sub_cancel_right, preΨ_ofNat, ← Nat.cast_add]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ((X * W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1) -
      W.preΨ' (n + 1 + 1) * W.preΨ' n * if Even ↑(n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ((X * W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1) -
      W.preΨ' (n + 1 + 1) * W.preΨ' n * if Even ↑(n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Tactic:
simp only [Nat.even_add_one, Int.even_add_one, Int.even_coe_nat, ite_not]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_coe_eq_empty {s t : Set α} : ((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅

Proof state:
α : Type u_1
s t : Set α
⊢ val ⁻¹' t = ∅ ↔ s ∩ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_iff_isLimit_pretopology [HasPullbacks C] (K : Pretopology C) :
    IsSheaf (K.toGrothendieck C) P ↔
      ∀ ⦃X : C⦄ (R : Presieve X),
        R ∈ K X → Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf (Pretopology.toGrothendieck C K) P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
dsimp [IsSheaf]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf (Pretopology.toGrothendieck C K) (P ⋙ coyoneda.obj (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ coyoneda.obj (op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
exact
  ⟨fun h X R hR => (isLimit_iff_isSheafFor_presieve P R).2 fun E => h E.unop R hR,
    fun h E X R hR => (isLimit_iff_isSheafFor_presieve P R).1 (h R hR) (op E)⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A), Presieve.IsSheaf (Pretopology.toGrothendieck C K) (P ⋙ coyoneda.obj (op E))) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))

Tactic:
simp_rw [isSheaf_pretopology]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ (E : A) {X : C}, ∀ R ∈ K.coverings X, IsSheafFor (P ⋙ coyoneda.obj (op E)) R) ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (generate R).arrows.cocone.op))
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions antivary iff the rearrangement inequality holds. -/
lemma antivary_iff_smul_rearrangement :
    Antivary f g ↔ ∀ i j, f i • g i + f j • g j ≤ f i • g j + f j • g i :=
  monovary_toDual_right.symm.trans <| by rw [monovary_iff_smul_rearrangement]; rfl

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι),
      f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤
        f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovary_iff_smul_rearrangement]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι),
      f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤
        f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Mathlib/Order/RelSeries.lean
@[simp] lemma last_tail (p : RelSeries r) (len_pos : p.length ≠ 0) :
    (p.tail len_pos).last = p.last

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.toFun (Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = p.toFun (Fin.last p.length)

Tactic:
congr

Result:
case e_a
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = Fin.last p.length

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 0 < p.length.sub 0

Tactic:
simpa [Nat.pos_iff_ne_zero] using len_pos

Result:
no goals

Proof state:
case e_a
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = Fin.last p.length

Tactic:
ext

Result:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ↑(Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = ↑(Fin.last p.length)

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (p.tail len_pos).last = p.last

Tactic:
show p _ = p _

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.toFun (Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = p.toFun (Fin.last p.length)

Proof state:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ↑(Fin.cast ⋯ (Fin.last (p.tail len_pos).length)).succ = ↑(Fin.last p.length)

Tactic:
simp only [tail_length, Fin.val_succ, Fin.coe_cast, Fin.val_last]

Result:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length

Proof state:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.length - 1 + 1 = p.length

Tactic:
exact Nat.succ_pred_eq_of_pos (by simpa [Nat.pos_iff_ne_zero] using len_pos)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.shiftLeft_zero' (n : BitVec w) : n <<< 0#w' = n

Proof state:
w w' : Nat
n : BitVec w
⊢ n <<< 0#w' = n

Tactic:
ext i

Result:
case pred
w w' : Nat
n : BitVec w
i : Nat
a✝ : i < w
⊢ (n <<< 0#w').getLsbD i = n.getLsbD i

Proof state:
case pred
w w' : Nat
n : BitVec w
i : Nat
a✝ : i < w
⊢ (n.shiftLeft (0#w').toNat).getLsbD i = n.getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem get?_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α} :
    l.get? a = getValue? a l.toList

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : AssocList α fun x => β
a : α
⊢ get? a l = getValue? a l.toList

Tactic:
induction l <;> simp_all [get?, List.getValue?]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem lipschitzWith_sup_right (z : α) : LipschitzWith 1 fun x => x ⊔ z :=
  LipschitzWith.of_dist_le_mul fun x y => by
    rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]
    exact norm_sup_sub_sup_le_norm x y z

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ dist (x ⊔ z) (y ⊔ z) ≤ ↑1 * dist x y

Tactic:
rw [NNReal.coe_one, one_mul, dist_eq_norm, dist_eq_norm]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
z x y : α
⊢ ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖

Tactic:
exact norm_sup_sub_sup_le_norm x y z

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem comp_sub {X Y Z : C} (f : X ⟶ Y) (g h : Y ⟶ Z) : f ≫ (g - h) = f ≫ g - f ≫ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g - h) = f ≫ g - f ≫ h

Tactic:
rw [sub_def, ← Category.assoc, prod.comp_lift, sub_def]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_inv_cancel {f : CauSeq β abv} (hf) : f * inv f hf ≈ 1 := fun ε ε0 =>
  let ⟨K, K0, i, H⟩ := abv_pos_of_not_limZero hf
  ⟨i, fun j ij => by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * f.inv hf - 1) j) < ε

Tactic:
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.finitary {M : Matroid α} [Finitary M] (h : N ≤r M) : N.Finitary

Proof state:
α : Type u_1
N M : Matroid α
inst✝ : M.Finitary
h : N ≤r M
⊢ N.Finitary

Tactic:
obtain ⟨R, -, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
inst✝ : M.Finitary
R : Set α
⊢ (M ↾ R).Finitary

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem map_one [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
    (1 : Matrix n n α).map f = (1 : Matrix n n β)

Proof state:
case a
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ f (if i✝ = j✝ then 1 else 0) = if i✝ = j✝ then 1 else 0

Tactic:
split_ifs <;> simp [h₀, h₁]

Result:
no goals

Proof state:
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
⊢ map 1 f = 1

Tactic:
ext

Result:
case a
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ map 1 f i✝ j✝ = 1 i✝ j✝

Proof state:
case a
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ map 1 f i✝ j✝ = 1 i✝ j✝

Tactic:
simp only [one_apply, map_apply]

Result:
case a
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ f (if i✝ = j✝ then 1 else 0) = if i✝ = j✝ then 1 else 0