harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/ScottTopology.lean
lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t)

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupClosed (sᶜ ∩ tᶜ)

Tactic:
exact hs.compl.inter ht.compl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∪ t)

Tactic:
rw [← dirSupClosed_compl, compl_union]

Result:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupClosed (sᶜ ∩ tᶜ)
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_init_self : snoc (init q) (q (last n)) = q

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (init q) (q (last n)) j = q j

Tactic:
simp only [init, snoc, h, cast_eq, dite_true, castSucc_castLT]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (init q) (q (last n)) = q

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j

Tactic:
by_cases h : j.val < n

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ↑j < n
⊢ snoc (init q) (q (last n)) j = q j

case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) j = q j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) j = q j

Tactic:
rw [eq_last_of_not_lt h]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) (last n) = q (last n)

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
h : ¬↑j < n
⊢ snoc (init q) (q (last n)) (last n) = q (last n)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
          =
        (expr.eval assign).getLsbD idx

Proof state:
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (go aig lhs).1.aig,
        ref := { gate := (((go aig lhs).1.vec.cast ⋯).get idx✝ hidx✝).gate, hgate := ?bin.add.hleft.hstart } }⟧ =
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx✝ ?bin.add.hleft.hidx }⟧

Tactic:
simp

Result:
no goals

Proof state:
case shiftLeft.hright
w : Nat
assign : Assignment
m✝ n✝ : Nat
lhs : BVExpr m✝
rhs : BVExpr n✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < m✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < n✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < m✝
⊢ ∀ (idx : Nat)
    (hidx : idx < { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.n),
    ⟦assign.toAIGAssignment,
        { aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.distance.get
              idx hidx }⟧ =
      (eval assign rhs).getLsbD idx

Tactic:
intros

Result:
case shiftLeft.hright
w : Nat
assign : Assignment
m✝ n✝ : Nat
lhs : BVExpr m✝
rhs : BVExpr n✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < m✝),
    ⟦assign.toAIGAssignment, { aig := (go aig lhs).val.aig, ref := (go aig lhs).val.vec.get idx hidx }⟧ =
      (eval assign lhs).getLsbD idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < n✝),
    ⟦assign.toAIGAssignment, { aig := (go aig rhs).val.aig, ref := (go aig rhs).val.vec.get idx hidx }⟧ =
      (eval assign rhs).getLsbD idx
aig : AIG BVBit
idx : Nat
hidx : idx < m✝
idx✝ : Nat
hidx✝ : idx✝ < { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.n
⊢ ⟦assign.toAIGAssignment,
      { aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref :=
          { n := n✝, target := (go aig lhs).1.vec.cast ⋯, distance := (go (go aig lhs).1.aig rhs).1.vec }.distance.get
            idx✝ hidx✝ }⟧ =
    (eval assign rhs).getLsbD idx✝
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma mul_X_mem_coeffsIn : p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
s : σ
⊢ p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simpa [-mul_monomial_mem_coeffsIn] using mul_monomial_mem_coeffsIn (i := .single s 1)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma preimage_subset {s t} (hs : s ⊆ f '' t) (hf : Set.InjOn f (f ⁻¹' s)) : f ⁻¹' s ⊆ t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ b ∈ f ⁻¹' s

Tactic:
simpa [hba]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
⊢ a ∈ t

Tactic:
obtain ⟨b, hb, hba⟩ := hs ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ a ∈ t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ a ∈ t

Tactic:
rwa [hf ha _ hba.symm]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ b ∈ f ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
⊢ f ⁻¹' s ⊆ t

Tactic:
rintro a ha

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
⊢ a ∈ t
-- Mathlib/Data/Num/Lemmas.lean
theorem lt_to_nat {m n : PosNum} : (m : ℕ) < n ↔ m < n :=
  show (m : ℕ) < n ↔ cmp m n = Ordering.lt from
    match cmp m n, cmp_to_nat m n with
    | Ordering.lt, h => by simp only at h; simp [h]
    | Ordering.eq, h => by simp only at h; simp [h, lt_irrefl]
    | Ordering.gt, h => by simp [not_lt_of_gt h]

Proof state:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Result:
no goals

Proof state:
m n : PosNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h, lt_irrefl]

Result:
no goals

Proof state:
m n : PosNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp only at h

Result:
m n : PosNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Proof state:
m n : PosNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp only at h

Result:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Proof state:
m n : PosNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
simp [not_lt_of_gt h]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem lookupAll_eq_nil {a : α} :
    ∀ {l : List (Sigma β)}, lookupAll a l = [] ↔ ∀ b : β a, Sigma.mk a b ∉ l
  | [] => by simp
  | ⟨a', b⟩ :: l => by
    by_cases h : a = a'
    · subst a'
      simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
        false_iff, not_forall, not_and, not_not, reduceCtorEq]
      use b
      simp
    · simp [h, lookupAll_eq_nil]

Proof state:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ¬b = b → ⟨a, b⟩ ∈ l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a', b⟩ :: l

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a', b⟩ :: l

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a', b⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ∃ x, ¬x = b → ⟨a, x⟩ ∈ l

Tactic:
use b

Result:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ¬b = b → ⟨a, b⟩ ∈ l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ lookupAll a [] = [] ↔ ∀ (b : β a), ⟨a, b⟩ ∉ []

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a', b⟩ :: l

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ lookupAll a (⟨a, b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a, b⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ lookupAll a (⟨a, b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a, b⟩ :: l

Tactic:
simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
  false_iff, not_forall, not_and, not_not, reduceCtorEq]

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ∃ x, ¬x = b → ⟨a, x⟩ ∈ l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ⟨a, b_1⟩ ∉ ⟨a', b⟩ :: l

Tactic:
simp [h, lookupAll_eq_nil]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem iSupIndep_sUnion_of_directed {s : Set (Set α)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, sSupIndep a) : sSupIndep (⋃₀ s)

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃ i, ↑i)

Tactic:
exact sSupIndep_iUnion_of_directed hs.directed_val (by simpa using h)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ ∀ (i : ↑s), sSupIndep ↑i

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃₀ s)

Tactic:
rw [Set.sUnion_eq_iUnion]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set (Set α)
hs : DirectedOn (fun x1 x2 => x1 ⊆ x2) s
h : ∀ a ∈ s, sSupIndep a
⊢ sSupIndep (⋃ i, ↑i)
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem mem_find_iff {p : Fin n → Prop} [DecidablePred p] {i : Fin n} :
    i ∈ Fin.find p ↔ p i ∧ ∀ j, p j → i ≤ j :=
  ⟨fun hi ↦ ⟨find_spec _ hi, fun _ ↦ find_min' hi⟩, by
    rintro ⟨hpi, hj⟩
    cases hfp : Fin.find p
    · rw [find_eq_none_iff] at hfp
      exact (hfp _ hpi).elim
    · exact Option.some_inj.2 (Fin.le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))⟩

Proof state:
case intro.some
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
val✝ : Fin n
hfp : find p = some val✝
⊢ i ∈ some val✝

Tactic:
exact Option.some_inj.2 (Fin.le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))

Result:
no goals

Proof state:
case intro.none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : find p = none
⊢ i ∈ none

Tactic:
rw [find_eq_none_iff] at hfp

Result:
case intro.none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : ∀ (i : Fin n), ¬p i
⊢ i ∈ none

Proof state:
case intro
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
⊢ i ∈ find p

Tactic:
cases hfp : Fin.find p

Result:
case intro.none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : find p = none
⊢ i ∈ none

case intro.some
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
val✝ : Fin n
hfp : find p = some val✝
⊢ i ∈ some val✝

Proof state:
case intro.none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : ∀ (i : Fin n), ¬p i
⊢ i ∈ none

Tactic:
exact (hfp _ hpi).elim

Result:
no goals

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
⊢ (p i ∧ ∀ (j : Fin n), p j → i ≤ j) → i ∈ find p

Tactic:
rintro ⟨hpi, hj⟩

Result:
case intro
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
⊢ i ∈ find p
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRight_cons_of_of
    {f g h i : a ⟶ b} {j : b ⟶ c}
    {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {ηs₁ : h ≫ j ⟶ i ≫ j}
    {η₁ : g ≫ j ⟶ h ≫ j} {η₂ : g ≫ j ⟶ i ≫ j} {η₃ : f ≫ j ⟶ i ≫ j}
    (e_ηs₁ : ηs ▷ j = ηs₁) (e_η₁ : η ▷ j = η₁)
    (e_η₂ : η₁ ≫ ηs₁ = η₂) (e_η₃ : (whiskerRightIso α j).hom ≫ η₂ = η₃) :
    (α.hom ≫ η ≫ ηs) ▷ j = η₃

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g h i : a ⟶ b
j : b ⟶ c
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ≫ j ⟶ i ≫ j
η₁ : g ≫ j ⟶ h ≫ j
η₂ : g ≫ j ⟶ i ≫ j
η₃ : f ≫ j ⟶ i ≫ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (whiskerRightIso α j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_iff_of_iUnion_eq_univ [Countable ι] {s : ι → Set α} (hs : ⋃ i, s i = univ) :
    μ = ν ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable ι
s : ι → Set α
hs : ⋃ i, s i = univ
⊢ μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

Tactic:
rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma holdsForLocalizationAway :
    HoldsForLocalizationAway FormallyUnramified

Proof state:
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => FormallyUnramified

Tactic:
intros R S _ _ _ r _

Result:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FormallyUnramified

Proof state:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FormallyUnramified R S

Tactic:
exact .of_isLocalization (.powers r)

Result:
no goals

Proof state:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap R S).FormallyUnramified

Tactic:
rw [formallyUnramified_algebraMap]

Result:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Algebra.FormallyUnramified R S
-- Mathlib/RingTheory/LocalRing/Module.lean
/-- If `M` is of finite presentation over a local ring `(R, 𝔪, k)` such that
`𝔪 ⊗ M → M` is injective, then every family of elements that is a `k`-basis of
`k ⊗ M` is an `R`-basis of `M`. -/
lemma exists_basis_of_basis_baseChange [Module.FinitePresentation R M]
    {ι : Type u} (v : ι → M) (hli : LinearIndependent k (TensorProduct.mk R k M 1 ∘ v))
    (hsp : Submodule.span k (Set.range (TensorProduct.mk R k M 1 ∘ v)) = ⊤)
    (H : Function.Injective ((𝔪).subtype.rTensor M)) :
    ∃ (b : Basis ι R M), ∀ i, b i = v i

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
this : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Surjective ⇑i

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
this : IsNoetherian k (k ⊗[R] (ι →₀ R)) := isNoetherian_of_isNoetherianRing_of_finite k (k ⊗[R] (ι →₀ R))
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
⊢ Submodule.span R (Set.range v) = ⊤
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma stalkClosedPointIso_inv :
    (stalkClosedPointIso R).inv = StructureSheaf.toStalk R _

Proof state:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (stalkClosedPointIso R).inv = StructureSheaf.toStalk (↑R) (closedPoint ↑R)

Tactic:
ext x

Result:
case hf.a
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↑R
⊢ (CommRingCat.Hom.hom (stalkClosedPointIso R).inv) x =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R) (closedPoint ↑R))) x

Proof state:
case hf.a
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↑R
⊢ (CommRingCat.Hom.hom (stalkClosedPointIso R).inv) x =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R) (closedPoint ↑R))) x

Tactic:
exact StructureSheaf.localizationToStalk_of _ _ _

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
lemma algebraMap_C_mem_adicCompletionIntegers (x : K) :
    ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈
      adicCompletionIntegers (RatFunc K) (idealX K)

Proof state:
K : Type u_2
inst✝ : Field K
x : K
⊢ ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Tactic:
have : HahnSeries.C x = ofPowerSeries ℤ K (PowerSeries.C K x) := by
  simp [C_apply, ofPowerSeries_C]

Result:
K : Type u_2
inst✝ : Field K
x : K
this : HahnSeries.C x = (ofPowerSeries ℤ K) ((PowerSeries.C K) x)
⊢ ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Proof state:
K : Type u_2
inst✝ : Field K
x : K
this : HahnSeries.C x = (ofPowerSeries ℤ K) ((PowerSeries.C K) x)
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) ((PowerSeries.C K) x)) ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Tactic:
apply LaurentSeriesRingEquiv_mem_valuationSubring

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
x : K
this : HahnSeries.C x = (ofPowerSeries ℤ K) ((PowerSeries.C K) x)
⊢ ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Tactic:
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, this]

Result:
K : Type u_2
inst✝ : Field K
x : K
this : HahnSeries.C x = (ofPowerSeries ℤ K) ((PowerSeries.C K) x)
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) ((PowerSeries.C K) x)) ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Proof state:
K : Type u_2
inst✝ : Field K
x : K
⊢ HahnSeries.C x = (ofPowerSeries ℤ K) ((PowerSeries.C K) x)

Tactic:
simp [C_apply, ofPowerSeries_C]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c

Proof state:
case intro.intro
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd✝ : d < a + b
a' : EReal
ha' : a' < a
hd : d < a' + b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd

Result:
case intro.intro.intro.intro
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd✝¹ : d < a + b
a' : EReal
ha' : a' < a
hd✝ : d < a' + b
b' : EReal
hb' : b' < b
hd : d < a' + b'
⊢ d ≤ c

Proof state:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
⊢ a + b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Result:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd : d < a + b
⊢ d ≤ c

Proof state:
case intro.intro.intro.intro
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd✝¹ : d < a + b
a' : EReal
ha' : a' < a
hd✝ : d < a' + b
b' : EReal
hb' : b' < b
hd : d < a' + b'
⊢ d ≤ c

Tactic:
exact hd.le.trans (h _ ha' _ hb')

Result:
no goals

Proof state:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd : d < a + b
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd

Result:
case intro.intro
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd✝ : d < a + b
a' : EReal
ha' : a' < a
hd : d < a' + b
⊢ d ≤ c
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.param_zpow_mul (hk : Tendsto k l atTop)
    (hf : SuperpolynomialDecay l k f) (z : ℤ) :
    SuperpolynomialDecay l k fun a => k a ^ z * f a

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z z' : ℤ
x : α
hx : k x ≠ 0
⊢ k x ^ (z' + z) * f x = (fun a => k a ^ z' * (k a ^ z * f a)) x

Tactic:
simp [zpow_add₀ hx, mul_assoc, Pi.mul_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a => k a ^ z * f a

Tactic:
rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a => k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a => k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)

Tactic:
refine fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => ?_)

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z z' : ℤ
x : α
hx : k x ≠ 0
⊢ k x ^ (z' + z) * f x = (fun a => k a ^ z' * (k a ^ z * f a)) x