harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Map.lean
theorem Filter.filter_injOn_Iic_iff_injOn {s : Set α} {m : α → β} :
    InjOn (map m) (Iic <| 𝓟 s) ↔ InjOn m s

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

Tactic:
rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
  at hxy <;> rwa [mem_Iic, pure_le_principal]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
m : α → β
⊢ InjOn (map m) (Iic (𝓟 s)) ↔ InjOn m s

Tactic:
refine ⟨fun hm x hx y hy hxy ↦ ?_, fun hm F hF G hG ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Proof state:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Tactic:
simp [map_eq_map_iff_of_injOn (le_principal_iff.mp hF) (le_principal_iff.mp hG) hm]

Result:
no goals
-- Mathlib/Algebra/DualNumber.lean
theorem lift_apply_inl (fe : {fe : (A →ₐ[R] B) × B // _}) (a : A) :
    lift fe (inl a : A[ε]) = fe.val.1 a

Proof state:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
a : A
⊢ (lift fe) (inl a) = (↑fe).1 a

Tactic:
rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem AddMonoidHom.toNatLinearMap_injective [AddCommMonoid M] [AddCommMonoid M₂] :
    Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _)

Proof state:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
⊢ f = g

Tactic:
ext x

Result:
case h
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
x : M
⊢ f x = g x

Proof state:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
⊢ Injective toNatLinearMap

Tactic:
intro f g h

Result:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
⊢ f = g

Proof state:
case h
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_compl [DecidableEq α] [Fintype α] (hs : s.Finite) (h : sᶜ.Finite) :
    h.toFinset = hs.toFinsetᶜ

Proof state:
case h
α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinsetᶜ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
⊢ h.toFinset = hs.toFinsetᶜ

Tactic:
ext

Result:
case h
α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinsetᶜ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem erase_toArray [BEq α] {as : List α} {a : α} :
    as.toArray.erase a = (as.erase a).toArray

Proof state:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ as.toArray.erase a = (as.erase a).toArray

Tactic:
rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]

Result:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ (match finIdxOf? a as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match idxOf? a as with
      | none => as
      | some i => as.eraseIdx i).toArray

Proof state:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ (match finIdxOf? a as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match Option.map (fun x => ↑x) (finIdxOf? a as) with
      | none => as
      | some i => as.eraseIdx i).toArray

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ (match finIdxOf? a as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match idxOf? a as with
      | none => as
      | some i => as.eraseIdx i).toArray

Tactic:
rw [idxOf?_eq_map_finIdxOf?_val]

Result:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ (match finIdxOf? a as with
    | none => as.toArray
    | some i => as.toArray.eraseIdx ↑i ⋯) =
    (match Option.map (fun x => ↑x) (finIdxOf? a as) with
      | none => as
      | some i => as.eraseIdx i).toArray
-- Mathlib/Combinatorics/Quiver/ReflQuiver.lean
theorem ReflQuiver.homOfEq_id {V : Type*} [ReflQuiver V] {X X' : V} (hX : X = X') :
    Quiver.homOfEq (𝟙rq X) hX hX = 𝟙rq X'

Proof state:
V : Type u_1
inst✝ : ReflQuiver V
X X' : V
hX : X = X'
⊢ Quiver.homOfEq (𝟙rq X) hX hX = 𝟙rq X'

Tactic:
subst hX

Result:
V : Type u_1
inst✝ : ReflQuiver V
X : V
⊢ Quiver.homOfEq (𝟙rq X) ⋯ ⋯ = 𝟙rq X

Proof state:
V : Type u_1
inst✝ : ReflQuiver V
X : V
⊢ Quiver.homOfEq (𝟙rq X) ⋯ ⋯ = 𝟙rq X

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem toFunAux_eq {s : Set ℕ} [DecidablePred (· ∈ s)] (x : s) :
    toFunAux x = #{y ∈ Finset.range x | y ∈ s}

Proof state:
s : Set ℕ
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ Nat.Subtype.toFunAux x = #(filter (fun y => y ∈ s) (range ↑x))

Tactic:
rw [toFunAux, List.countP_eq_length_filter]

Result:
s : Set ℕ
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)).length = #(filter (fun y => y ∈ s) (range ↑x))

Proof state:
s : Set ℕ
inst✝ : DecidablePred fun x => x ∈ s
x : ↑s
⊢ (List.filter (fun x => decide (x ∈ s)) (List.range ↑x)).length = #(filter (fun y => y ∈ s) (range ↑x))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem mem_insertNone {s : Finset α} : ∀ {o : Option α}, o ∈ insertNone s ↔ ∀ a ∈ o, a ∈ s
  | none => iff_of_true (Multiset.mem_cons_self _ _) fun a h => by cases h
  | some a => Multiset.mem_cons.trans <| by simp

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ a_1 ∈ some a, a_1 ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s

Tactic:
cases h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem restrict_iff {s : Set X} : HolderWith C r (s.restrict f) ↔ HolderOnWith C r f s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
⊢ HolderWith C r (s.restrict f) ↔ HolderOnWith C r f s

Tactic:
simp [HolderWith, HolderOnWith]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
/-- If `map f μ = μ`, then the measure of the preimage of any null measurable set `s`
is equal to the measure of `s`.
Note that this lemma does not assume (a.e.) measurability of `f`. -/
lemma measure_preimage_of_map_eq_self {f : α → α} (hf : map f μ = μ)
    {s : Set α} (hs : NullMeasurableSet s μ) : μ (f ⁻¹' s) = μ s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
if hfm : AEMeasurable f μ then
  rw [← map_apply₀ hfm, hf]
  rwa [hf]
else
  rw [map_of_not_aemeasurable hfm] at hf
  simp [← hf]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : 0 = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
simp [← hf]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
rw [map_of_not_aemeasurable hfm] at hf

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : 0 = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
rw [← map_apply₀ hfm, hf]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : AEMeasurable f μ
⊢ NullMeasurableSet s (map f μ)

Tactic:
rwa [hf]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The L function of the trivial Dirichlet character mod `N` is obtained from the Riemann
zeta function by multiplying with `∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))`. -/
lemma LFunctionTrivChar_eq_mul_riemannZeta {s : ℂ} (hs : s ≠ 1) :
    LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))) * riemannZeta s

Proof state:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel ⋯) 1) s = LFunction 1 s * ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))

Tactic:
convert LFunction_changeLevel N.one_dvd 1 (.inr hs) using 4 with p

Result:
case h.e'_3.h.e'_6.a.h.e'_6
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
a✝ : p ∈ N.primeFactors
⊢ ↑p ^ (-s) = 1 ↑p * ↑p ^ (-s)

Proof state:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s

Tactic:
rw [← LFunction_modOne_eq (χ := 1), LFunctionTrivChar, ← changeLevel_one N.one_dvd, mul_comm]

Result:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunction ((changeLevel ⋯) 1) s = LFunction 1 s * ∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))

Proof state:
case h.e'_3.h.e'_6.a.h.e'_6
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
p : ℕ
a✝ : p ∈ N.primeFactors
⊢ ↑p ^ (-s) = 1 ↑p * ↑p ^ (-s)

Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem neg_one_geom_sum [Ring α] {n : ℕ} :
    ∑ i ∈ range n, (-1 : α) ^ i = if Even n then 0 else 1

Proof state:
case neg
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0

Tactic:
rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

Result:
no goals

Proof state:
case zero
α : Type u
inst✝ : Ring α
⊢ ∑ i ∈ range 0, (-1) ^ i = if Even 0 then 0 else 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i ∈ range (k + 1), (-1) ^ i = if Even (k + 1) then 0 else 1

Tactic:
simp only [geom_sum_succ', Nat.even_add_one, hk]

Result:
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1

Proof state:
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1

Tactic:
split_ifs with h

Result:
case pos
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

case neg
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0

Proof state:
case pos
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

Tactic:
rw [h.neg_one_pow, add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem blastDivSubtractShift_decl_eq (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastDivSubtractShiftOutput aig w
hres : blastDivSubtractShift aig falseRef trueRef n d wn wr q r = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
unfold blastDivSubtractShift at hres

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastDivSubtractShiftOutput aig w
hres :
  (let wn_1 := wn - 1;
    let wr := wr + 1;
    let res := blastShiftConcat aig { lhs := r, bit := n.getD wn_1 falseRef };
    let aig_1 := res.aig;
    let r' := res.vec;
    let_fun this := ⋯;
    let falseRef_1 := falseRef.cast this;
    let trueRef_1 := trueRef.cast this;
    let d_1 := d.cast this;
    let q_1 := q.cast this;
    let res_1 := blastShiftConcat aig_1 { lhs := q_1, bit := falseRef_1 };
    let aig_2 := res_1.aig;
    let posQ := res_1.vec;
    let_fun this_1 := ⋯;
    let trueRef_2 := trueRef_1.cast this_1;
    let d_2 := d_1.cast this_1;
    let q_2 := q_1.cast this_1;
    let r' := r'.cast this_1;
    let res := blastShiftConcat aig_2 { lhs := q_2, bit := trueRef_2 };
    let aig_3 := res.aig;
    let negQ := res.vec;
    let_fun this_2 := ⋯;
    let d_3 := d_2.cast this_2;
    let r' := r'.cast this_2;
    let posQ := posQ.cast this_2;
    let res_2 := blastSub aig_3 { lhs := r', rhs := d_3 };
    let aig_4 := res_2.aig;
    let negR := res_2.vec;
    let_fun this_3 := ⋯;
    let d_4 := d_3.cast this_3;
    let r'_1 := r'.cast this_3;
    let posQ := posQ.cast this_3;
    let negQ := negQ.cast this_3;
    let posR := r'_1;
    let res := BVPred.mkUlt aig_4 { lhs := r'_1, rhs := d_4 };
    let aig_5 := res.aig;
    let discr := res.ref;
    let_fun this_4 := ⋯;
    let posQ := posQ.cast this_4;
    let negQ := negQ.cast this_4;
    let posR := posR.cast this_4;
    let negR := negR.cast this_4;
    let res_3 := AIG.RefVec.ite aig_5 { discr := discr, lhs := posQ, rhs := negQ };
    let aig_6 := res_3.aig;
    let nextQ := res_3.vec;
    let_fun this_5 := ⋯;
    let posR := posR.cast this_5;
    let negR := negR.cast this_5;
    let discr := discr.cast this_5;
    let res := AIG.RefVec.ite aig_6 { discr := discr, lhs := posR, rhs := negR };
    ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem blastDivSubtractShift_decl_eq (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size),
    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx] = aig.decls[idx]

Tactic:
generalize hres : blastDivSubtractShift aig falseRef trueRef n d wn wr q r = res

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
res : BlastDivSubtractShiftOutput aig w
hres : blastDivSubtractShift aig falseRef trueRef n d wn wr q r = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Scheme.zeroLocus_biInf
    {X : Scheme.{u}} {U : X.Opens} {ι : Type*}
    (I : ι → Ideal Γ(X, U)) {t : Set ι} (ht : t.Finite) :
    X.zeroLocus (U := U) ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus (U := U) (I i)) ∪ (↑U)ᶜ

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus ↑(⨅ i ∈ ∅, I i) = (⋃ i ∈ ∅, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_

Result:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ X.zeroLocus ↑(⨅ i_1 ∈ insert i t, I i_1) = (⋃ i_1 ∈ insert i t, X.zeroLocus ↑(I i_1)) ∪ (↑U)ᶜ

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ X.zeroLocus ↑(⨅ i_1, ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) = X.zeroLocus (↑(I i) ∩ ↑(⨅ i ∈ t, I i))

Tactic:
congr!

Result:
case h.e'_3
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ ↑(⨅ i_1, ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) = ↑(I i) ∩ ↑(⨅ i ∈ t, I i)

Proof state:
case h.e'_3
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ ↑(⨅ i_1, ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) = ↑(I i) ∩ ↑(⨅ i ∈ t, I i)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ X.zeroLocus ↑(⨅ i_1 ∈ insert i t, I i_1) = (⋃ i_1 ∈ insert i t, X.zeroLocus ↑(I i_1)) ∪ (↑U)ᶜ

Tactic:
simp only [Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, ← IH, ← zeroLocus_inf,
  Submodule.inf_coe, Set.union_assoc]

Result:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t✝ : Set ι
ht✝ : t✝.Finite
i : ι
t : Set ι
hit : i ∉ t
ht : t.Finite
IH : X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
⊢ X.zeroLocus ↑(⨅ i_1, ⨅ (_ : i_1 = i ∨ i_1 ∈ t), I i_1) = X.zeroLocus (↑(I i) ∩ ↑(⨅ i ∈ t, I i))
-- Mathlib/Algebra/Module/Lattice.lean
/-- Any `R`-lattice in `ι → K` has `#ι` as `R`-rank. -/
lemma rank_of_pi {ι : Type*} [Fintype ι] [IsFractionRing R K] (M : Submodule R (ι → K))
    [IsLattice K M] : Module.rank R M = Fintype.card ι

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = ↑(Fintype.card ι)

Tactic:
rw [IsLattice.rank' K M]

Result:
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank K (ι → K) = ↑(Fintype.card ι)

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank K (ι → K) = ↑(Fintype.card ι)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedCoreAux_empty : balancedCoreAux 𝕜 (∅ : Set E) = ∅

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ balancedCoreAux 𝕜 ∅ = ∅

Tactic:
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ ∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ ∅

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ ∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ ∅

Tactic:
exact fun _ => ⟨1, norm_one.ge, not_mem_empty _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f i

Proof state:
case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j > i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f i (l.eraseIdx j)).length
h' : ¬i = k
h✝¹ : ¬k < j
h✝ : i = k + 1
⊢ f l[k + 1] = l[k + 1]

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j > i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f i (l.eraseIdx j)).length
⊢ ((modify f i l).eraseIdx j)[k] = (modify f i (l.eraseIdx j))[k]

Tactic:
simp only [getElem_eraseIdx, getElem_modify]

Result:
case h
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j > i
k : Nat
h₁ : k < ((modify f i l).eraseIdx j).length
h₂ : k < (modify f i (l.eraseIdx j)).length
⊢ (if h : k < j then if i = k then f l[k] else l[k] else if i = k + 1 then f l[k + 1] else l[k + 1]) =
    if i = k then f (if h' : k < j then l[k] else l[k + 1]) else if h' : k < j then l[k] else l[k + 1]
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
    partialGamma (s + 1) X = s * partialGamma s X - (-X).exp * X ^ s

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y => rexp (-y)) (-rexp (-x)) x
⊢ HasDerivAt (fun y => ↑y ^ s) (s * ↑x ^ (s - 1)) x

Tactic:
have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_

Result:
case refine_2
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y => rexp (-y)) (-rexp (-x)) x
t : HasDerivAt (fun x => id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ HasDerivAt (fun y => ↑y ^ s) (s * ↑x ^ (s - 1)) x

case refine_1
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
hx : x ∈ Ioo 0 X
d1 : HasDerivAt (fun y => rexp (-y)) (-rexp (-x)) x
⊢ id ↑x ∈ slitPlane
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_neg_iff {x y : PGame} : y ≤ -x ↔ x ≤ -y

Proof state:
x y : PGame
⊢ y ≤ -x ↔ x ≤ -y

Tactic:
rw [← neg_neg x, neg_le_neg_iff, neg_neg]

Result:
no goals