harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Digraph/Basic.lean
theorem iSup_adj {f : ι → Digraph V} : (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Proof state:
ι : Sort u_1
V : Type u_2
a b : V
f : ι → Digraph V
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma ne_top_iff_ne_one : p ≠ ∞ ↔ q ≠ 1

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p ≠ ⊤ ↔ q ≠ 1

Tactic:
rw [not_iff_not, eq_top_iff_eq_one p q]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
    map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
n : Nat
l : List α
⊢ map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l)

Tactic:
induction l generalizing n <;> simp_all

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem supp_eq {α : TypeVec n} {i} (x : F α) :
    supp x i = { u | ∀ a f, abs ⟨a, f⟩ = x → u ∈ f i '' univ }

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
⊢ supp x i = {u | ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ}

Tactic:
ext

Result:
case h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ}

Proof state:
case h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔ x✝ ∈ {u | ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ}

Tactic:
apply mem_supp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_iff_left_iff_imp  : ∀ {a b : Bool}, ((a || b) = a) ↔ (b → a)

Proof state:
⊢ ∀ {a b : Bool}, (a || b) = a ↔ b = true → a = true

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Finmap.lean
@[simp] lemma keysLookupEquiv_symm_apply_lookup :
    ∀ (f : {f : Finset α × (∀ a, Option (β a)) // ∀ i, (f.2 i).isSome ↔ i ∈ f.1}) a,
      (keysLookupEquiv.symm f).lookup a = f.1.2 a :=
  keysLookupEquiv.surjective.forall.2 fun _ _ => by
    simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : Finmap β
x✝ : α
⊢ lookup x✝ (keysLookupEquiv.symm (keysLookupEquiv x✝¹)) = (↑(keysLookupEquiv x✝¹)).2 x✝

Tactic:
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem encode_lt_comp (cf cg) :
    encode cf < encode (comp cf cg) ∧ encode cg < encode (comp cf cg)

Proof state:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.comp cg)
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Tactic:
exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Result:
no goals

Proof state:
cf cg : Code
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Tactic:
have : encode (pair cf cg) < encode (comp cf cg) := by simp [encodeCode_eq, encodeCode]

Result:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.comp cg)
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Proof state:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.comp cg)

Tactic:
simp [encodeCode_eq, encodeCode]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem is_cartan_of_zeroRootSubalgebra_eq (h : zeroRootSubalgebra R L H = H) :
    H.IsCartanSubalgebra :=
  { nilpotent := inferInstance
    self_normalizing

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
h : zeroRootSubalgebra R L H = H
⊢ H.normalizer = H

Tactic:
rw [← h]

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
h : zeroRootSubalgebra R L H = H
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
h : zeroRootSubalgebra R L H = H
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Tactic:
exact zeroRootSubalgebra_normalizer_eq_self R L H

Result:
no goals
-- Mathlib/Data/Analysis/Topology.lean
theorem isOpen [TopologicalSpace α] (F : Realizer α) (s : F.σ) : IsOpen (F.F s) :=
  isOpen_iff_nhds.2 fun a m ↦ by simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ F.F.f s
⊢ 𝓝 a ≤ 𝓟 (F.F.f s)

Tactic:
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma moduleCat_exact_iff_ker_sub_range :
    S.Exact ↔ LinearMap.ker S.g.hom ≤ LinearMap.range S.f.hom

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f)

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f)

Tactic:
rw [moduleCat_exact_iff]

Result:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) ↔
    LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f)
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_mul_le' (a b : E) : ‖a * b‖ ≤ ‖a‖ + ‖b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a * b‖ ≤ ‖a‖ + ‖b‖

Tactic:
simpa [dist_eq_norm_div] using dist_triangle a 1 b⁻¹

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.lt_left_of_right_lt (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment 𝕜 x y) (hyz : f y < f z) : f z < f x

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y < f (a • x + b • y)
⊢ f (a • x + b • y) < f x

Tactic:
exact hf.lt_left_of_right_lt' hx hy ha hb hab hyz

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y < f z
⊢ f z < f x

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y < f (a • x + b • y)
⊢ f (a • x + b • y) < f x
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma jacobian_eq_jacobiMatrix_det : P.jacobian = algebraMap P.Ring S P.jacobiMatrix.det

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
⊢ P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
simp [jacobiMatrix, jacobian]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma negMulLog_eq_neg : negMulLog = fun x ↦ - (x * log x)

Proof state:
⊢ negMulLog = fun x => -(x * log x)

Tactic:
simp [negMulLog_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
    (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
simp_rw [product_self_eq_disjiUnion_perm hσ, sum_disjiUnion, sum_map, Embedding.coeFn_mk]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
rw [sum_smul_sum, ← sum_product']

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)
-- Mathlib/Data/TypeVec.lean
theorem id_eq_nilFun {α : TypeVec 0} : @id _ α = nilFun

Proof state:
case a.h
α : TypeVec.{u_1} 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x x✝

Tactic:
cases x

Result:
no goals

Proof state:
α : TypeVec.{u_1} 0
⊢ id = nilFun

Tactic:
ext x

Result:
case a.h
α : TypeVec.{u_1} 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x x✝
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma transfiniteCompositionsOfShape_ιObj :
    (coproducts.{w} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType
      (ιObj I κ f) :=
  ⟨((relativeCellComplexιObj I κ f).transfiniteCompositionOfShape).ofLE
    (by simp)⟩

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts ≤ (coproducts.{w, v, u} I).pushouts

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.right₀_nth {Γ} [Inhabited Γ] (T : Tape Γ) (n : ℕ) : T.right₀.nth n = T.nth n

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ T.right₀.nth n = T.nth ↑n

Tactic:
cases n <;> simp only [Tape.nth, Tape.right₀, Int.ofNat_zero, ListBlank.nth_zero,
  ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_zero (a : Ordinal) : a - 0 = a

Proof state:
a : Ordinal.{u_4}
⊢ a - 0 = a

Tactic:
simpa only [zero_add] using add_sub_cancel 0 a

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
    cochainsMap (MonoidHom.id G) (φ ≫ ψ) =
      cochainsMap (MonoidHom.id G) φ ≫ cochainsMap (MonoidHom.id G) ψ

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ cochainsMap (MonoidHom.id G) (φ ≫ ψ) = cochainsMap (MonoidHom.id G) φ ≫ cochainsMap (MonoidHom.id G) ψ

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem sInf_toSubmodule_eq_iInf (S : Set (LieSubmodule R L M)) :
    (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (N : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⨅ N ∈ S, ↑N

Tactic:
rw [sInf_toSubmodule, ← Set.image, sInf_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
    as.all p start stop ↔ ∀ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop → p as[i]

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
this : ¬as.any (fun x => !p x) start stop = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true
⊢ (!as.any (fun x => !p x) start stop) = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ as.all p start stop = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true

Tactic:
rw [all_eq_not_any_not]

Result:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ (!as.any (fun x => !p x) start stop) = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
start stop : Nat
⊢ ¬as.any (fun x => !p x) start stop = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true

Tactic:
simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
  Bool.not_eq_false, and_imp]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma neg_pred (a : ℤ) : -pred a = succ (-a)

Proof state:
a : ℤ
⊢ -a.pred = (-a).succ

Tactic:
rw [← Int.neg_eq_comm.mp (neg_succ (-a)), Int.neg_neg]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem int_sub (h : Irrational x) (m : ℤ) : Irrational (m - x)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m - x)

Tactic:
simpa only [Rat.cast_intCast] using h.rat_sub m

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem map_permutations' (f : α → β) (ts : List α) :
    map (map f) (permutations' ts) = permutations' (map f ts)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations' = (map f ts).permutations'

Tactic:
induction' ts with t ts ih <;>
  [rfl; simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem isIso_iff_mk_eq_top {X Y : C} (f : X ⟶ Y) [Mono f] : IsIso f ↔ mk f = ⊤ :=
  ⟨fun _ => mk_eq_mk_of_comm _ _ (asIso f) (Category.comp_id _), fun h => by
    rw [← ofMkLEMk_comp h.le, Category.comp_id]
    exact (isoOfMkEqMk _ _ h).isIso_hom⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso f

Tactic:
rw [← ofMkLEMk_comp h.le, Category.comp_id]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) ⋯)

Tactic:
exact (isoOfMkEqMk _ _ h).isIso_hom

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_cancel' {r₁ : R} {r₂ : X} {s t : S} :
    ((r₁ * s) /ₒ t) • (r₂ /ₒ s) = (r₁ • r₂) /ₒ t

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s t : ↥S
⊢ (r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t

Tactic:
simp [oreDiv_smul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Scheme.zeroLocus_iInf_of_nonempty
    {X : Scheme.{u}} {U : X.Opens} {ι : Type*}
    (I : ι → Ideal Γ(X, U)) [Finite ι] [Nonempty ι] :
    X.zeroLocus (U := U) ↑(⨅ i, I i) = ⋃ i, X.zeroLocus (U := U) (I i)

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
inst✝¹ : Finite ι
inst✝ : Nonempty ι
⊢ X.zeroLocus ↑(⨅ i, I i) = ⋃ i, X.zeroLocus ↑(I i)

Tactic:
simpa using zeroLocus_biInf_of_nonempty I Set.finite_univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Bitwise.lean
theorem Bool.toBitVec_toUInt64 {b : Bool} :
    b.toUInt64.toBitVec = (BitVec.ofBool b).setWidth 64

Proof state:
b : Bool
⊢ b.toUInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)

Tactic:
cases b <;> simp [toUInt64]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_one_sub (s : ℝ) : Gamma s * Gamma (1 - s) = π / sin (π * s)

Proof state:
s : ℝ
⊢ Gamma s * Gamma (1 - s) = π / sin (π * s)

Tactic:
simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ←
  Complex.Gamma_ofReal, Complex.ofReal_sub, Complex.ofReal_one]

Result:
s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma (1 - ↑s) = ↑π / Complex.sin (↑π * ↑s)

Proof state:
s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma (1 - ↑s) = ↑π / Complex.sin (↑π * ↑s)

Tactic:
exact Complex.Gamma_mul_Gamma_one_sub s

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_left {g : β →*₀o γ} {f₁ f₂ : α →*₀o β} (hg : Function.Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
lemma sum_card_fiberwise_eq_card_filter {κ : Type*} [DecidableEq κ] (s : Finset ι) (t : Finset κ)
    (g : ι → κ) : ∑ j ∈ t, #{i ∈ s | g i = j} = #{i ∈ s | g i ∈ t}

Proof state:
ι : Type u_1
κ : Type u_6
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ j ∈ t, #(filter (fun i => g i = j) s) = #(filter (fun i => g i ∈ t) s)

Tactic:
simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_eq {s : SignedMeasure α} {j : JordanDecomposition α}
    (h : s = j.toSignedMeasure) : s.toJordanDecomposition = j

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ s.toJordanDecomposition = j

Tactic:
rw [h, toJordanDecomposition_toSignedMeasure]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem one_mem_div {I J : Submodule R A} : 1 ∈ I / J ↔ J ≤ I

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I J : Submodule R A
⊢ 1 ∈ I / J ↔ J ≤ I

Tactic:
rw [← one_le, le_div_iff_mul_le, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
nonrec lemma Subgroup.orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G) {x} (hx : x ∈ s) :
  orderOf x ∣ Nat.card s

Proof state:
G : Type u_6
inst✝ : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card ↥s

Tactic:
simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m

Proof state:
m n : Nat
⊢ m.gcd (n.gcd m) = n.gcd m

Tactic:
rw [gcd_comm n m, gcd_gcd_self_right_left]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_finrank_top (h : A ≤ B) : relfinrank A B * finrank B E = finrank A E

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relfinrank B * finrank (↥B) E = finrank (↥A) E

Tactic:
simpa using congr(toNat $(relrank_mul_rank_top h))

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negY_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.negY P = -P y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.negY P = -P y

Tactic:
rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * 0 ^ 3 = 0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P P = 0

Tactic:
rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * 0 ^ 3 = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_cons_cons : (a :: b :: l).getLast? = (b :: l).getLast?

Proof state:
α✝ : Type u_1
a b : α✝
l : List α✝
⊢ (a :: b :: l).getLast? = (b :: l).getLast?

Tactic:
simp [getLast?_cons]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ inner x x = 0 ↔ x = 0

Tactic:
rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, ofReal_eq_zero, norm_eq_zero]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b ↔ a ⩿ b :=
  Set.OrdConnected.apply_wcovBy_apply_iff OrderEmbedding.withTopCoe <| by
    simp [WithTop.range_coe, ordConnected_Iio]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (range ⇑OrderEmbedding.withTopCoe).OrdConnected

Tactic:
simp [WithTop.range_coe, ordConnected_Iio]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.diam s

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
⊢ diam ((convexHull ℝ) s) = diam s

Tactic:
simp only [Metric.diam, convexHull_ediam]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem inf_relindex_left : (H ⊓ K).relindex H = K.relindex H

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relindex H = K.relindex H

Tactic:
rw [inf_comm, inf_relindex_right]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma Indep_iff_IndepSets (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    Indep m₁ m₂ μ ↔ IndepSets {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ

Proof state:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ μ ↔ IndepSets {s | MeasurableSet s} {s | MeasurableSet s} μ

Tactic:
simp only [Indep, IndepSets, Kernel.Indep]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_X_pow_char_pow_sub_C {y : R} :
    (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
have H := roots_expand_pow (p := p) (n := n) (f := X - C y)

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) (X - C y).roots
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) (X - C y).roots
⊢ (X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
rwa [roots_X_sub_C, Multiset.map_singleton, map_sub, expand_X, expand_C] at H

Result:
no goals