harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousWithinAt_iff_range {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((↑) : range F → X → α) S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt Subtype.val S x₀

Tactic:
simp only [EquicontinuousWithinAt, forall_subtype_range_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma inter_ground_subset_closure (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ X ∩ M.E ⊆ M.closure X

Tactic:
simp_rw [closure_def, subset_sInter_iff]

Result:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ t' ∈ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}, X ∩ M.E ⊆ t'

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem lt_max_of_sq_lt_mul {a b c : M} (h : a ^ 2 < b * c) : a < max b c

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b c : M
h : a ^ 2 < b * c
⊢ a < b ⊔ c

Tactic:
simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_reverse {l : Vector α n} {i} (h : i < n) :
    l.reverse[i]? = l[n - 1 - i]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ l.reverse[i]? = l[n - 1 - i]?

Tactic:
cases l

Result:
case mk
α : Type u_1
n i : Nat
h : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[n - 1 - i]?

Proof state:
case mk
α : Type u_1
n i : Nat
h : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[n - 1 - i]?

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pbind_isSome {o : Option α} {f : (a : α) → a ∈ o → Option β} :
    (o.pbind f).isSome = ∃ a h, (f a h).isSome

Proof state:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : (f a ⋯).isSome = true
⊢ ∃ a_1 h, (f a_1 ⋯).isSome = true

Tactic:
exact ⟨a, rfl, h⟩

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (f a ⋯).isSome = true ↔ ∃ a_1 h, (f a_1 ⋯).isSome = true

Tactic:
constructor

Result:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (f a ⋯).isSome = true → ∃ a_2 h, (f a_2 ⋯).isSome = true

case some.mpr
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, (f a_1 ⋯).isSome = true) → (f a ⋯).isSome = true

Proof state:
case some.mpr
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (∃ a_1 h, (f a_1 ⋯).isSome = true) → (f a ⋯).isSome = true

Tactic:
rintro ⟨a, rfl, h⟩

Result:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : (f a ⋯).isSome = true
⊢ (f a ⋯).isSome = true

Proof state:
case none
α : Type u_1
β : Type u_2
f : (a : α) → a ∈ none → Option β
⊢ ((none.pbind f).isSome = true) = ∃ a h, (f a h).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
case some.mpr.intro.intro
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : (f a ⋯).isSome = true
⊢ (f a ⋯).isSome = true

Tactic:
exact h

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (((some a).pbind f).isSome = true) = ∃ a_1 h, (f a_1 h).isSome = true

Tactic:
simp only [pbind_some, mem_def, some.injEq, eq_iff_iff]

Result:
case some
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (f a ⋯).isSome = true ↔ ∃ a_1 h, (f a_1 ⋯).isSome = true

Proof state:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
⊢ (f a ⋯).isSome = true → ∃ a_2 h, (f a_2 ⋯).isSome = true

Tactic:
intro h

Result:
case some.mp
α : Type u_1
β : Type u_2
a : α
f : (a_1 : α) → a_1 ∈ some a → Option β
h : (f a ⋯).isSome = true
⊢ ∃ a_1 h, (f a_1 ⋯).isSome = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_false_iff_not_lex [DecidableEq α] (lt : α → α → Bool) :
    lex l₁ l₂ lt = false ↔ ¬ Lex (fun x y => lt x y) l₁ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
lt : α → α → Bool
⊢ l₁.lex l₂ lt = false ↔ ¬Lex (fun x y => lt x y = true) l₁ l₂

Tactic:
simp [Bool.eq_false_iff, lex_eq_true_iff_lex]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma rev_add (a b : Fin n) : rev (a + b) = rev a - b

Proof state:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b

Tactic:
rw [← last_sub, ← last_sub, sub_add_eq_sub_sub]

Result:
no goals

Proof state:
case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b

Tactic:
exact a.elim0

Result:
no goals

Proof state:
n : ℕ
a b : Fin n
⊢ (a + b).rev = a.rev - b

Tactic:
cases n

Result:
case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b

case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3

Proof state:
case mk
toBitVec✝ : BitVec 8
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Tactic:
simp_arith [UInt8.toNat, BitVec.toNat]

Result:
no goals

Proof state:
a : UInt8
⊢ sizeOf a = a.toNat + 3

Tactic:
cases a

Result:
case mk
toBitVec✝ : BitVec 8
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.mulMon_denote (ctx : Context) (p : Poly) (k : Nat) (m : Mon) : (p.mulMon k m).denote ctx = p.denote ctx * k * m.denote ctx

Proof state:
ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx (p.mulMon k m) = denote ctx p * k * Mon.denote ctx m

Tactic:
simp [mulMon, go]

Result:
ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx [] + denote ctx p * k * Mon.denote ctx m = denote ctx p * k * Mon.denote ctx m

Proof state:
ctx : Context
p : Poly
k : Nat
m : Mon
⊢ denote ctx [] + denote ctx p * k * Mon.denote ctx m = denote ctx p * k * Mon.denote ctx m

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
p✝¹ : Poly
k : Nat
m : Mon
p✝ acc : Poly
k' : Nat
m' : Mon
p : List (Nat × Mon)
⊢ denote ctx (mulMon.go k m ((k', m') :: p) acc) = denote ctx acc + denote ctx ((k', m') :: p) * k * Mon.denote ctx m

Tactic:
simp! [go p, Nat.left_distrib, denote_insertSorted, Mon.mul_denote, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc]

Result:
no goals

Proof state:
ctx : Context
p✝ : Poly
k : Nat
m : Mon
p acc : Poly
⊢ denote ctx (mulMon.go k m [] acc) = denote ctx acc + denote ctx [] * k * Mon.denote ctx m

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
p✝ : Poly
k : Nat
m : Mon
p acc : Poly
⊢ denote ctx (mulMon.go k m p acc) = denote ctx acc + denote ctx p * k * Mon.denote ctx m

Tactic:
match p with
| [] => simp!
| (k', m') :: p =>
  simp! [go p, Nat.left_distrib, denote_insertSorted, Mon.mul_denote, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findFinIdx?_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp))

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findFinIdx? f { toList := toList✝ } =
    Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g { toList := toList✝ }.unattach)

Tactic:
simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g toList✝.unattach) =
    Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g { toList := toList✝ }.unattach)

Proof state:
α : Type ?u.59478
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
i : Fin l.unattach.size
⊢ l.unattach.size = l.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g l.unattach)

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ findFinIdx? f { toList := toList✝ } =
    Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g { toList := toList✝ }.unattach)

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g toList✝.unattach) =
    Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g { toList := toList✝ }.unattach)

Tactic:
rw [findFinIdx?_congr List.unattach_toArray]

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g toList✝.unattach) =
    Option.map (fun i => Fin.cast ⋯ i) (Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g toList✝.unattach.toArray))

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g toList✝.unattach) =
    Option.map (fun i => Fin.cast ⋯ i) (Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g toList✝.unattach.toArray))

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
  | 0 => rfl
  | n + 1 => by
    rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
      succ_eq_add_one]
    ring

Proof state:
n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!

Tactic:
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
  succ_eq_add_one]

Result:
n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem Isometry.preimage_perpBisector {f : P → P'} (h : Isometry f) (p₁ p₂ : P) :
    f ⁻¹' (perpBisector (f p₁) (f p₂)) = perpBisector p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V' : Type u_3
P' : Type u_4
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ : P
⊢ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) = ↑(perpBisector p₁ p₂)

Tactic:
ext x

Result:
case h
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V' : Type u_3
P' : Type u_4
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ x : P
⊢ x ∈ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) ↔ x ∈ ↑(perpBisector p₁ p₂)

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V' : Type u_3
P' : Type u_4
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ x : P
⊢ x ∈ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) ↔ x ∈ ↑(perpBisector p₁ p₂)

Tactic:
simp [mem_perpBisector_iff_dist_eq, h.dist_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem le_inv_self_iff : a ≤ a⁻¹ ↔ a ≤ 1

Proof state:
α : Type u
inst✝ : LinearOrderedCommGroup α
a : α
⊢ a ≤ a⁻¹ ↔ a ≤ 1

Tactic:
simp [← not_iff_not]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem compl_top : (⊤ : α)ᶜ = ⊥ :=
  eq_of_forall_le_iff fun a => by rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ ⊤ᶜ ↔ a ≤ ⊥

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecCol_mul_mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0)
    (i : Fin r) :
    ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr unit) = 0

Proof state:
case hM
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0

Tactic:
simpa [mul_listTransvecRow_last_col] using hM

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0

Tactic:
have : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod) := by
  simp [listTransvecCol, mul_listTransvecRow_last_col]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0

Tactic:
rw [this, Matrix.mul_assoc]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0

Tactic:
apply listTransvecCol_mul_last_col

Result:
case hM
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)

Tactic:
simp [listTransvecCol, mul_listTransvecRow_last_col]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/SInteger.lean
theorem integer_eq :
    (S.integer K).toSubring =
      ⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.toSubring :=
  SetLike.ext' <| by ext; simp

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ↑(S.integer K).toSubring = ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

Tactic:
ext

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ↑(S.integer K).toSubring ↔
    x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝ : K
⊢ x✝ ∈ ↑(S.integer K).toSubring ↔
    x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), (HeightOneSpectrum.valuation K v).valuationSubring.toSubring)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_append_right {s t : Array α} {i : Nat} {x : α} (h : s.size ≤ i) :
    (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - s.size) x

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h : s.size ≤ i
⊢ (s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - s.size) x

Tactic:
rw [setIfInBounds_append, if_neg (by omega)]

Result:
no goals

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h : s.size ≤ i
⊢ ¬i < s.size

Tactic:
omega

Result:
no goals
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem natPow_zero_natMod_one : Nat.mod (Nat.pow a (nat_lit 0)) (nat_lit 1) = nat_lit 0

Proof state:
a : ℕ
⊢ (a.pow 0).mod 1 = 0

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
a : ℕ
⊢ (a.pow 0).mod 1 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive] lemma one_mem_pow (hs : 1 ∈ s) : 1 ∈ s ^ n

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using pow_mem_pow hs

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.add_eq_lift_id_desc [HasBinaryBiproduct X X] :
    f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f g : X ⟶ Y
inst✝ : HasBinaryBiproduct X X
⊢ f + g = lift (𝟙 X) (𝟙 X) ≫ desc f g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_restrict (h : R ⊆ E) : (freeOn E) ↾ R = freeOn R

Proof state:
α : Type u_1
E R : Set α
h : R ⊆ E
⊢ freeOn E ↾ R = freeOn R

Tactic:
simp [h, eq_freeOn_iff, Subset.rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_empty_iff_forall_not_mem {l : Array α} : l = #[] ↔ ∀ a, a ∉ l

Proof state:
α : Type u_1
l : Array α
⊢ l = #[] ↔ ∀ (a : α), ¬a ∈ l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ } = #[] ↔ ∀ (a : α), ¬a ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ } = #[] ↔ ∀ (a : α), ¬a ∈ { toList := toList✝ }

Tactic:
simp [List.eq_nil_iff_forall_not_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem exists_mem_of_size_pos (l : Vector α n) (h : 0 < n) : ∃ x, x ∈ l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
h : 0 < n
⊢ ∃ x, x ∈ l

Tactic:
simpa using List.exists_mem_of_ne_nil l.toList (by simpa using (Nat.ne_of_gt h))

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
h : 0 < n
⊢ l.toList ≠ []

Tactic:
simpa using (Nat.ne_of_gt h)

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_val (x : Icc a b) : projIcc a b h x = x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : ↑(Icc a b)
⊢ projIcc a b h ↑x = x

Tactic:
cases x

Result:
case mk
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
apply projIcc_of_mem

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_eq_arctan_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₃ ≠ p₂) : ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, angle_add_eq_arctan_of_inner_eq_zero h h0]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
rw [ne_comm, ← @vsub_ne_zero V] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} (hl : DistinctKeys l) : containsKey a (eraseKey k l) → containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ containsKey a (eraseKey k l) = true → containsKey a l = true

Tactic:
simp [containsKey_eraseKey hl]

Result:
no goals