harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_eq_neg_one_pow (hζ : IsPrimitiveRoot ζ 2) [IsDomain L] :
    norm K ζ = (-1 : K) ^ finrank K L

Proof state:
K : Type u
L : Type v
inst✝³ : CommRing L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsDomain L
⊢ (Algebra.norm K) ζ = (-1) ^ Module.finrank K L

Tactic:
rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]

Result:
no goals

Proof state:
K : Type u
L : Type v
inst✝³ : CommRing L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst✝ : IsDomain L
⊢ -1 = (algebraMap K L) (-1)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
lemma inv_hom_apply {M N : ModuleCat.{v} R} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x

Proof state:
R : Type u
inst✝ : Ring R
M N : ModuleCat R
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
@[ext]
lemma ext {F G : OplaxFunctor B C} {α β : F ⟶ G} {m n : α ⟶ β} (w : ∀ b, m.app b = n.app b) :
    m = n

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
⊢ m = n

Tactic:
apply Modification.ext

Result:
case app
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
⊢ m.app = n.app

Proof state:
case app
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
⊢ m.app = n.app

Tactic:
ext

Result:
case app.h
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
x✝ : B
⊢ m.app x✝ = n.app x✝

Proof state:
case app.h
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
x✝ : B
⊢ m.app x✝ = n.app x✝

Tactic:
apply w

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem rotateRight_zero (l : List α) : rotateRight l 0 = l

Proof state:
α : Type u_1
l : List α
⊢ l.rotateRight 0 = l

Tactic:
simp [rotateRight]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_div_some [Div α] (a b : α) : some a / some b = some (a / b)

Proof state:
α : Type u_1
inst✝ : Div α
a b : α
⊢ some a / some b = some (a / b)

Tactic:
simp [div_def]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_eq_iInf' (s : Set α) : m.trim s = ⨅ t : { t // s ⊆ t ∧ MeasurableSet t }, m t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, m ↑t

Tactic:
simp [iInf_subtype, iInf_and, trim_eq_iInf]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_comm [DecidableEq n] (M N : Matrix n n A) : det (M * N) = det (N * M)

Proof state:
A : Type u_5
inst✝² : CommRing A
n : Type u_7
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M N : Matrix n n A
⊢ (M * N).det = (N * M).det

Tactic:
rw [det_mul, det_mul, mul_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hc' : #ι < cof c)
    (hf : ∀ (i), ∀ b < c, f i b < c) {a} : a < c → nfpFamily.{u, u} f a < c :=
  nfpFamily_lt_ord_lift hc (by rwa [(#ι).lift_id]) hf

Proof state:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
⊢ Cardinal.lift.{?u.33310, u} #ι < c.cof

Tactic:
rwa [(#ι).lift_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_append_left' (l₂ : Array α) {l₁ : Array α} {i : Nat} (hi : i < l₁.size) :
    l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.size hi)

Proof state:
α : Type u_1
l₂ l₁ : Array α
i : Nat
hi : i < l₁.size
⊢ l₁[i] = (l₁ ++ l₂)[i]

Tactic:
rw [getElem_append_left] <;> simp

Result:
no goals

Proof state:
α : Type ?u.236287
l₂ l₁ : Array α
i : Nat
hi : i < l₁.size
⊢ i < (l₁ ++ l₂).size

Tactic:
simpa using Nat.lt_add_right l₂.size hi

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem pairwise_sublists {R} {l : List α} (H : Pairwise R l) :
    Pairwise (Lex R on reverse) (sublists l)

Proof state:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
have := (pairwise_reverse.2 H).sublists'

Result:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (Lex (swap fun b a => R a b)) l.reverse.sublists'
⊢ Pairwise (Lex R on reverse) l.sublists

Proof state:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (Lex (swap fun b a => R a b)) l.reverse.sublists'
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
rwa [sublists'_reverse, pairwise_map] at this

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
theorem hasBasis_nhds_zero_of_basis {ι' : Type*} {p : ι' → Prop} {b : ι' → Set F}
    (h : (𝓝 (0 : F)).HasBasis p b) :
    (𝓝 (0 : E [⋀^ι]→L[𝕜] F)).HasBasis
      (fun Si : Set (ι → E) × ι' => IsVonNBounded 𝕜 Si.1 ∧ p Si.2)
      fun Si => { f | MapsTo f Si.1 (b Si.2) }

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι' : Type u_5
p : ι' → Prop
b : ι' → Set F
h : (𝓝 0).HasBasis p b
⊢ (𝓝 0).HasBasis (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}

Tactic:
rw [nhds_induced]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι' : Type u_5
p : ι' → Prop
b : ι' → Set F
h : (𝓝 0).HasBasis p b
⊢ (Filter.comap toContinuousMultilinearMap (𝓝 (toContinuousMultilinearMap 0))).HasBasis
    (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι' : Type u_5
p : ι' → Prop
b : ι' → Set F
h : (𝓝 0).HasBasis p b
⊢ (Filter.comap toContinuousMultilinearMap (𝓝 (toContinuousMultilinearMap 0))).HasBasis
    (fun Si => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si => {f | MapsTo (⇑f) Si.1 (b Si.2)}

Tactic:
exact (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis h).comap _

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem not_principal_iff_of_monotone
    (h₁ : ∀ a, Monotone (op a)) (h₂ : ∀ a, Monotone (Function.swap op a)) :
    ¬ Principal op o ↔ ∃ a < o, o ≤ op a a

Proof state:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ ¬Principal op o ↔ ∃ a < o, o ≤ op a a

Tactic:
simp [principal_iff_of_monotone h₁ h₂]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_sInf (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) :
    (sInf s).toReal = sInf (ENNReal.toReal '' s)

Proof state:
s : Set ℝ≥0∞
hf : ∀ r ∈ s, r ≠ ⊤
⊢ (sInf s).toReal = sInf (ENNReal.toReal '' s)

Tactic:
simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem cast_rfl {l : Vector α n} : l.cast rfl = l

Proof state:
case mk
α : Type u_1
l : Array α
⊢ Vector.cast ⋯ { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ Vector.cast ⋯ l = l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
l : Array α
⊢ Vector.cast ⋯ { toArray := l, size_toArray := ⋯ } = { toArray := l, size_toArray := ⋯ }
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_of_isEmpty [IsEmpty ι] (μ : ι → Measure α) : sum μ = 0

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : IsEmpty ι
μ : ι → Measure α
⊢ sum μ = 0

Tactic:
rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem IsTransitive.inter (hx : x.IsTransitive) (hy : y.IsTransitive) :
    (x ∩ y).IsTransitive := fun z hz w hw => by
  rw [mem_inter] at hz ⊢
  exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

Proof state:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y

Tactic:
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

Result:
no goals

Proof state:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∩ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∩ y

Tactic:
rw [mem_inter] at hz ⊢

Result:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem OneHom.comp_one [One M] [One N] [One P] (f : OneHom N P) : f.comp (1 : OneHom M N) = 1

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ f.comp 1 = 1

Tactic:
ext

Result:
case h
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝

Proof state:
case h
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝

Tactic:
simp only [OneHom.map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
    Tendsto f atBot (𝓝 (⨆ i, f i))

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto f atBot (𝓝 (⨆ i, f i))

Tactic:
convert tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_filter_le (a b c : α) : {x ∈ Ico a b | c ≤ x} = Ico (max a c) b

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ a
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (a ⊔ c) b

Tactic:
rw [Ico_filter_le_of_le_left h, max_eq_left h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (a ⊔ c) b

Tactic:
cases le_total a c with
| inl h => rw [Ico_filter_le_of_left_le h, max_eq_right h]
| inr h => rw [Ico_filter_le_of_le_left h, max_eq_left h]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (a ⊔ c) b

Tactic:
rw [Ico_filter_le_of_left_le h, max_eq_right h]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem eval_eq_sum_degreeLTEquiv {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) (x : R) :
    p.eval x = ∑ i, degreeLTEquiv _ _ ⟨p, hp⟩ i * x ^ (i : ℕ)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ (p.sum fun e a => a * x ^ e) = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Tactic:
exact (sum_fin _ (by simp_rw [zero_mul, forall_const]) (mem_degreeLT.mp hp)).symm

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ eval x p = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Tactic:
simp_rw [eval_eq_sum]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ (p.sum fun e a => a * x ^ e) = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), 0 * x ^ i = 0

Tactic:
simp_rw [zero_mul, forall_const]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccLimit_toDual_iff : IsSuccLimit (toDual a) ↔ IsPredLimit a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
⊢ IsSuccLimit (toDual a) ↔ IsPredLimit a

Tactic:
simp [IsSuccLimit, IsPredLimit]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Localization.lean
lemma W_eq_W_range_sheafToPresheaf_obj :
    J.W = LeftBousfield.W (· ∈ Set.range (sheafToPresheaf J A).obj)

Proof state:
case h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ P ∈ Set.range (sheafToPresheaf J A).obj → Presheaf.IsSheaf J P

Tactic:
rintro ⟨F, rfl⟩

Result:
case h.h.a.mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
F : Sheaf J A
⊢ Presheaf.IsSheaf J ((sheafToPresheaf J A).obj F)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
⊢ J.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
apply congr_arg

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
⊢ Presheaf.IsSheaf J = fun x => x ∈ Set.range (sheafToPresheaf J A).obj

Proof state:
case h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ P ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
exact ⟨⟨P, hP⟩, rfl⟩

Result:
no goals

Proof state:
case h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P → P ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
intro hP

Result:
case h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ P ∈ Set.range (sheafToPresheaf J A).obj

Proof state:
case h.h.a
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P ↔ P ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
constructor

Result:
case h.h.a.mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P → P ∈ Set.range (sheafToPresheaf J A).obj

case h.h.a.mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ P ∈ Set.range (sheafToPresheaf J A).obj → Presheaf.IsSheaf J P

Proof state:
case h.h.a.mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
F : Sheaf J A
⊢ Presheaf.IsSheaf J ((sheafToPresheaf J A).obj F)

Tactic:
exact F.cond

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
⊢ Presheaf.IsSheaf J = fun x => x ∈ Set.range (sheafToPresheaf J A).obj

Tactic:
ext P

Result:
case h.h.a
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_4, u_2} A
P : Cᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf J P ↔ P ∈ Set.range (sheafToPresheaf J A).obj
-- Mathlib/Order/Filter/Tendsto.lean
theorem comap_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : ψ ∘ φ = id)
    (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : comap φ g = f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ g = f

Tactic:
refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f

Tactic:
rw [comap_comap, eq, comap_id]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map {v' : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (inf : Injective f)
    (h : v.IsEquiv v') : (v.map f hf).IsEquiv (v'.map f hf) :=
  let H : StrictMono f := hf.strictMono_of_injective inf
  fun r s =>
  calc
    f (v r) ≤ f (v s) ↔ v r ≤ v s

Proof state:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ f (v r) ≤ f (v s) ↔ v r ≤ v s

Tactic:
rw [H.le_iff_le]

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone ⇑f
inf : Injective ⇑f
h : v.IsEquiv v'
H : StrictMono ⇑f := Monotone.strictMono_of_injective hf inf
r s : R
⊢ v' r ≤ v' s ↔ f (v' r) ≤ f (v' s)

Tactic:
rw [H.le_iff_le]

Result:
no goals
-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem ax_grothendieck_univ (p : ι → MvPolynomial ι K) :
    (fun v i => eval v (p i)).Injective →
    (fun v i => eval v (p i)).Surjective

Proof state:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
⊢ (Function.Injective fun v i => (eval v) (p i)) → Function.Surjective fun v i => (eval v) (p i)

Tactic:
simpa [Set.injective_iff_injOn_univ, Set.surjective_iff_surjOn_univ] using
    ax_grothendieck_zeroLocus 0 p

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[reassoc (attr := simp)]
lemma tensorCongr_SpecTensorTo {T T' : Triplet f g} (h : T = T') :
    Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo

Tactic:
simp only [Triplet.tensorCongr_refl, Iso.refl_hom, Spec.map_id, Category.id_comp]

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
subst h

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map (Triplet.tensorCongr ⋯).hom ≫ T.SpecTensorTo = T.SpecTensorTo
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem OrthonormalBasis.volume_parallelepiped (b : OrthonormalBasis ι ℝ F) :
    volume (parallelepiped b) = 1

Proof state:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
⊢ volume (parallelepiped ⇑b) = 1

Tactic:
let o := (stdOrthonormalBasis ℝ F).toBasis.orientation

Result:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation
⊢ volume (parallelepiped ⇑b) = 1

Proof state:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ volume (parallelepiped ⇑b) = 1

Tactic:
haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩

Result:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
⊢ volume (parallelepiped ⇑b) = 1

Proof state:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation
⊢ volume (parallelepiped ⇑b) = 1

Tactic:
rw [← o.measure_eq_volume]

Result:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation
⊢ o.volumeForm.measure (parallelepiped ⇑b) = 1

Proof state:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := (stdOrthonormalBasis ℝ F).toBasis.orientation
⊢ o.volumeForm.measure (parallelepiped ⇑b) = 1

Tactic:
exact o.measure_orthonormalBasis b

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_iff_segment_subset : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s

Tactic:
rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
exact h hy ⟨a, b, ha, hb, hab, rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s) → StarConvex 𝕜 x s

Proof state:
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
exact h hy ha hb hab

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s) → StarConvex 𝕜 x s

Tactic:
rintro h y hy a b ha hb hab

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → [x-[𝕜]y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s