harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l

Proof state:
α : Type u_1
⊢ ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l

Tactic:
intro l a h

Result:
α : Type u_1
l : List α
a : α
h : a ∈ l.head?
⊢ a ∈ l

Proof state:
case cons
α : Type u_1
a b : α
l : List α
h : a ∈ (b :: l).head?
⊢ a ∈ b :: l

Tactic:
simp at h

Result:
case cons
α : Type u_1
a b : α
l : List α
h : b = a
⊢ a ∈ b :: l

Proof state:
case cons
α : Type u_1
a b : α
l : List α
h : b = a
⊢ a ∈ b :: l

Tactic:
cases h

Result:
case cons.refl
α : Type u_1
a : α
l : List α
⊢ a ∈ a :: l

Proof state:
case cons.refl
α : Type u_1
a : α
l : List α
⊢ a ∈ a :: l

Tactic:
exact mem_cons_self a l

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l.head?
⊢ a ∈ l

Tactic:
cases l with
| nil => simp at h
| cons b l =>
  simp at h
  cases h
  exact mem_cons_self a l

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
h : a ∈ [].head?
⊢ a ∈ []

Tactic:
simp at h

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem isUnitTrinomial_iff :
    p.IsUnitTrinomial ↔ #p.support = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
hy : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff m)
hz : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff n)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
simp_rw [coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow] at hx hy hz

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp :
  #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3 ∧
    ∀ k_1 ∈ (C x * X ^ k + C y * X ^ m + C z * X ^ n).support,
      IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
rw [support_trinomial hkm hmn hx hy hz] at hp

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
replace hx := hp.2 k (mem_insert_self k {m, n})

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hy : y ≠ 0
hz : z ≠ 0
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_subst {t : L.Term α} {tf : α → L.Term β} {v : β → M} :
    (t.subst tf).realize v = t.realize fun a => (tf a).realize v

Proof state:
case var
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
a✝ : α
⊢ realize v ((var a✝).subst tf) = realize (fun a => realize v (tf a)) (var a✝)

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
⊢ realize v (t.subst tf) = realize (fun a => realize v (tf a)) t

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp [ih]

Result:
no goals

Proof state:
case func
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), realize v ((_ts✝ a).subst tf) = realize (fun a => realize v (tf a)) (_ts✝ a)
⊢ realize v ((func _f✝ _ts✝).subst tf) = realize (fun a => realize v (tf a)) (func _f✝ _ts✝)

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Data/List/NodupEquivFin.lean
theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
    l.Duplicate x ↔
      ∃ (n m : Fin l.length) (_ : n < m),
        x = l.get n ∧ x = l.get m

Proof state:
α : Type u_1
l : List α
x : α
⊢ Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

Tactic:
rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist,
  sublist_iff_exists_fin_orderEmbedding_get_eq]

Result:
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m

Proof state:
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = l.get (f ⟨0, ⋯⟩) ∧ x = l.get (f ⟨1, ⋯⟩)

Tactic:
rw [← hf, ← hf]

Result:
case mp.intro
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = (replicate 2 x).get ⟨1, ⋯⟩

Proof state:
case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i => if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj

Result:
case mpr.intro.intro.intro.intro.refine_1.mk.succ.mk.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi✝ : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj✝ : n✝ + 1 < (replicate 2 x).length
hi : n✝¹ = 0
hj : n✝ = 0
⊢ ⟨n✝¹ + 1, hi✝⟩ < ⟨n✝ + 1, hj✝⟩ →
    (fun i => if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi✝⟩ < (fun i => if ↑i = 0 then n else m) ⟨n✝ + 1, hj✝⟩

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩

Result:
case mpr.intro.intro.intro.intro.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i => if ↑i = 0 then n else m

case mpr.intro.intro.intro.intro.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix =
      l.get ((OrderEmbedding.ofStrictMono (fun i => if ↑i = 0 then n else m) ?mpr.intro.intro.intro.intro.refine_1) ix)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem Measure.restrict_singleton' {a : α} : μ.restrict {a} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NoAtoms μ
a : α
⊢ μ.restrict {a} = 0

Tactic:
simp only [measure_singleton, Measure.restrict_eq_zero]

Result:
no goals
-- Mathlib/NumberTheory/FunctionField.lean
theorem InftyValuation.map_one' : inftyValuationDef Fq 1 = 1 :=
  (if_neg one_ne_zero).trans <| by rw [RatFunc.intDegree_one, ofAdd_zero, WithZero.coe_one]

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
⊢ ↑(Multiplicative.ofAdd (RatFunc.intDegree 1)) = 1

Tactic:
rw [RatFunc.intDegree_one, ofAdd_zero, WithZero.coe_one]

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem not_mem_sdiff_of_not_mem_left (h : a ∉ s) : a ∉ s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ a ∉ s \ t

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem apply_eq_of_dist_lt {x y : ∀ n, E n} {n : ℕ} (h : dist x y < (1 / 2) ^ n) {i : ℕ}
    (hi : i ≤ n) : x i = y i

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
this : n < firstDiff x y
⊢ x i = y i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_lt this)

Result:
no goals

Proof state:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n i : ℕ
hi : i ≤ n
h : dist x x < (1 / 2) ^ n
⊢ x i = x i

Tactic:
rfl

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
⊢ x i = y i

Tactic:
rcases eq_or_ne x y with (rfl | hne)

Result:
case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n i : ℕ
hi : i ≤ n
h : dist x x < (1 / 2) ^ n
⊢ x i = x i

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ x i = y i

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ x i = y i

Tactic:
have : n < firstDiff x y := by
  simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h

Result:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
this : n < firstDiff x y
⊢ x i = y i

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : dist x y < (1 / 2) ^ n
i : ℕ
hi : i ≤ n
hne : x ≠ y
⊢ n < firstDiff x y

Tactic:
simpa [dist_eq_of_ne hne, inv_lt_inv₀, pow_lt_pow_iff_right₀, one_lt_two] using h

Result:
no goals
-- Mathlib/Analysis/Analytic/Within.lean
/-- If `f` is `AnalyticOn` near each point in a set, it is `AnalyticOn` the set -/
lemma analyticOn_of_locally_analyticOn {f : E → F} {s : Set E}
    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) :
    AnalyticOn 𝕜 f s

Proof state:
case a.inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : Metric.ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
⊢ y = 0 ∨ x + y ∈ u

Tactic:
apply Or.inr (ru ?_)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)
x : E
m : x ∈ s
u : Set E
ou : IsOpen u
xu : x ∈ u
fu : AnalyticOn 𝕜 f (s ∩ u)
r : ℝ
r0 : r > 0
ru : Metric.ball x r ⊆ u
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p (s ∩ u) x t
y : E
yr : ‖y‖ < r ∧ edist y 0 < t
ys : x + y ∈ s
⊢ x + y ∈ Metric.ball x r
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsAlt.eq_of_add_add_eq_zero [IsCancelAdd M] {a b c : M₁} (hAdd : a + b + c = 0) :
    B a b = B b c

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) b = (B b) c

Tactic:
have : B a a + B a b + B a c = B a c + B b c + B c c := by
  simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) a + (B a) b + (B a) c = (B a) c + (B b) c + (B c) c
⊢ (B a) b = (B b) c

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) c + (B a) b = (B a) c + (B b) c
⊢ (B a) b = (B b) c

Tactic:
exact add_left_cancel this

Result:
no goals

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) a + (B a) b + (B a) c = (B a) c + (B b) c + (B c) c
⊢ (B a) b = (B b) c

Tactic:
rw [H, H, zero_add, add_zero, add_comm] at this

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this : (B a) c + (B a) b = (B a) c + (B b) c
⊢ (B a) b = (B b) c

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring R₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst✝ : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ (B a) a + (B a) b + (B a) c = (B a) c + (B b) c + (B c) c

Tactic:
simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem lt_size_of_lt_aig_size (aig : AIG α) (input : β aig) (h : x < aig.decls.size) :
    x < (f aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < (f aig input).aig.decls.size

Tactic:
apply Nat.lt_of_lt_of_le

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ Nat

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m

Tactic:
exact h

Result:
no goals

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
exact le_size aig input

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subset_one_on_sdiff [DecidableEq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 1)
    (hfg : ∀ x ∈ s₁, f x = g x) : ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i

Tactic:
rw [← prod_sdiff h, prod_eq_one hg, one_mul]

Result:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ x ∈ s₁, g x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = ∏ x ∈ s₁, g x

Tactic:
exact prod_congr rfl hfg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_eq_map (l : Array (α × β)) : unzip l = (l.map Prod.fst, l.map Prod.snd)

Proof state:
case mk
α : Type u_1
β : Type u_2
toList✝ : List (α × β)
⊢ { toList := toList✝ }.unzip = (map Prod.fst { toList := toList✝ }, map Prod.snd { toList := toList✝ })

Tactic:
simp [List.unzip_eq_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array (α × β)
⊢ l.unzip = (map Prod.fst l, map Prod.snd l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
toList✝ : List (α × β)
⊢ { toList := toList✝ }.unzip = (map Prod.fst { toList := toList✝ }, map Prod.snd { toList := toList✝ })
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_neg_eq_arg_add_pi_of_im_neg {x : ℂ} (hi : x.im < 0) : arg (-x) = arg x + π

Proof state:
x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π

Tactic:
simp [neg_div, Real.arccos_neg, add_comm, ← sub_eq_add_neg]

Result:
no goals

Proof state:
x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg + π

Tactic:
rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]

Result:
x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem dvd_mul_of_dvd_right (h : a ∣ b) (c : α) : a ∣ c * b

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ c * b

Tactic:
rw [mul_comm]

Result:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Tactic:
exact h.mul_right _

Result:
no goals
-- Mathlib/Topology/Order/T5.lean
theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE (hd : Disjoint s (closure t))
    (ha : a ∈ s) : (ordConnectedSection (ordSeparatingSet s t))ᶜ ∈ 𝓝[≥] a

Proof state:
case h.refine_2.intro.intro
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c < y

Tactic:
refine lt_of_not_le fun hyc => ?_

Result:
case h.refine_2.intro.intro
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
⊢ False
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_eq_zero_of_angle_eq_pi_right {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) :
    ∠ p₂ p₃ p₁ = 0

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₁ = π
⊢ ∠ p₂ p₃ p₁ = 0

Tactic:
exact angle_eq_zero_of_angle_eq_pi_left h

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 : ∠ p₁ p₂ p₃ = π
⊢ ∠ p₂ p₃ p₁ = 0

Tactic:
rw [angle_comm] 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 : ∠ p₃ p₂ p₁ = π
⊢ ∠ p₂ p₃ p₁ = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem rotateLeft_replicate (n) (a : α) : rotateLeft (replicate m a) n = replicate m a

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (n + 1) % m + (n + 1) % m = m

Tactic:
have : (n + 1) % m < m := Nat.mod_lt _ (by omega)

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (n + 1) % m + (n + 1) % m = m

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ (replicate m a).rotateLeft (n + 1) = replicate m a

Tactic:
suffices 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m by
  simpa [rotateLeft]

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m

Proof state:
α : Type u_1
m : Nat
a : α
n : Nat
this : 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m
⊢ (replicate m a).rotateLeft (n + 1) = replicate m a

Tactic:
simpa [rotateLeft]

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (n + 1) % m + (n + 1) % m = m

Tactic:
omega

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m

Tactic:
intro h

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (n + 1) % m + min ((n + 1) % m) m = m

Proof state:
case zero
α : Type u_1
m : Nat
a : α
⊢ (replicate m a).rotateLeft 0 = replicate m a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m > 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (n + 1) % m + min ((n + 1) % m) m = m

Tactic:
rw [Nat.min_eq_left (Nat.le_of_lt (Nat.mod_lt _ (by omega)))]

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (n + 1) % m + (n + 1) % m = m

Proof state:
α : Type u_1
m n : Nat
a : α
⊢ (replicate m a).rotateLeft n = replicate m a

Tactic:
cases n with
| zero => simp
| succ n =>
  suffices 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m by
    simpa [rotateLeft]
  intro h
  rw [Nat.min_eq_left (Nat.le_of_lt (Nat.mod_lt _ (by omega)))]
  have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
  omega

Result:
no goals