harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem bound_of_shell [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε C : ℝ} (ε_pos : 0 < ε) {c : 𝕜}
    (hc : 1 < ‖c‖) (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) :
    ‖f x‖ ≤ C * ‖x‖

Proof state:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
exact SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
by_cases hx : x = 0

Result:
case pos
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
/-- The image of an element `p` of `FreeAddMonoid (R × Π i, s i)` in the `PiTensorProduct` is
equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries `(a, m)` of `p`.
-/
lemma _root_.FreeAddMonoid.toPiTensorProduct (p : FreeAddMonoid (R × Π i, s i)) :
    AddCon.toQuotient (c := addConGen (PiTensorProduct.Eqv R s)) p =
    List.sum (List.map (fun x ↦ x.1 • ⨂ₜ[R] i, x.2 i) p)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑p = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum

Tactic:
match p with
| [] => rw [List.map_nil, List.sum_nil]; rfl
| x :: ps => rw [List.map_cons, List.sum_cons, ← List.singleton_append, ← toPiTensorProduct ps,
               ← tprodCoeff_eq_smul_tprod]; rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑[] = 0

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑[] = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) []).sum

Tactic:
rw [List.map_nil, List.sum_nil]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
⊢ ↑[] = 0

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
x : R × ((i : ι) → s i)
ps : List (R × ((i : ι) → s i))
⊢ ↑([x] ++ ps) = (tprodCoeff R x.1 fun i => x.2 i) + ↑ps

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
x : R × ((i : ι) → s i)
ps : List (R × ((i : ι) → s i))
⊢ ↑(x :: ps) = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (x :: ps)).sum

Tactic:
rw [List.map_cons, List.sum_cons, ← List.singleton_append, ← toPiTensorProduct ps,
  ← tprodCoeff_eq_smul_tprod]

Result:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
p : FreeAddMonoid (R × ((i : ι) → s i))
x : R × ((i : ι) → s i)
ps : List (R × ((i : ι) → s i))
⊢ ↑([x] ++ ps) = (tprodCoeff R x.1 fun i => x.2 i) + ↑ps
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.indep {m1 m2 m : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    [IsZeroOrMarkovKernel κ] {p1 p2 : Set (Set Ω)} (h1 : m1 ≤ m) (h2 : m2 ≤ m) (hp1 : IsPiSystem p1)
    (hp2 : IsPiSystem p2) (hpm1 : m1 = generateFrom p1) (hpm2 : m2 = generateFrom p2)
    (hyp : IndepSets p1 p2 κ μ) :
    Indep m1 m2 κ μ

Proof state:
case h.hn
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
a : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
i j : ℕ
hij : i ≠ j
⊢ Disjoint (f i ∩ t2) (f j ∩ t2)

Tactic:
exact Disjoint.inter_left _ (Disjoint.inter_right _ (hf_disj hij))

Result:
no goals

Proof state:
case inr.empty
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (∅ ∩ t2) = (κ a) ∅ * (κ a) t2

Tactic:
simp only [Set.empty_inter, measure_empty, zero_mul, eq_self_iff_true, Filter.eventually_true]

Result:
no goals

Proof state:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
⊢ Indep m1 m2 κ μ

Tactic:
intros t1 t2 ht1 ht2

Result:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h : IsMarkovKernel κ
t1 t2 : Set Ω
ht1 : t1 ∈ {s | MeasurableSet s}
ht2 : t2 ∈ {s | MeasurableSet s}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem _root_.List.attachWith_mem_toArray {l : List α} :
    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
case h
α : Type u_1
l : List α
⊢ ∀ (a : α), a ∈ l → ∀ (h₁ : a ∈ l.toArray) (h₂ : a ∈ l), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ List.pmap Subtype.mk l ⋯ = List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯

Tactic:
apply List.pmap_congr_left

Result:
case h
α : Type u_1
l : List α
⊢ ∀ (a : α), a ∈ l → ∀ (h₁ : a ∈ l.toArray) (h₂ : a ∈ l), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Proof state:
α : Type ?u.6607
l : List α
x : α
h : x ∈ l
⊢ (fun x => x ∈ l.toArray) x

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.attachWith (fun x => x ∈ l.toArray) ⋯ =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      l.attach

Tactic:
simp only [List.attachWith, List.attach, List.map_pmap]

Result:
α : Type u_1
l : List α
⊢ List.pmap Subtype.mk l ⋯ = List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯

Proof state:
α : Type ?u.6607
l : List α
x✝ : { x // x ∈ l }
x : α
h : x ∈ l
⊢ x ∈ l.toArray

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_biUnion {s : Set ι} {f : ι → Set α} (hs : s.Finite) :
    IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem exists_ne_none {p : Option α → Prop} : (∃ x ≠ none, p x) ↔ (∃ x : α, p x)

Proof state:
α : Type u_1
p : Option α → Prop
⊢ (∃ x, x ≠ none ∧ p x) ↔ ∃ x, p (some x)

Tactic:
simp only [← exists_prop, bex_ne_none]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys)

Proof state:
case nil
ys : IntList
⊢ [] - ys = [] + -ys

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), xs - ys = xs + -ys
y : Int
ys : List Int
⊢ x :: xs - y :: ys = x :: xs + -(y :: ys)

Tactic:
simp_all [Int.sub_eq_add_neg]

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), xs - ys = xs + -ys
ys : IntList
⊢ x :: xs - ys = x :: xs + -ys

Tactic:
cases ys with
| nil => simp
| cons y ys => simp_all [Int.sub_eq_add_neg]

Result:
no goals

Proof state:
xs ys : IntList
⊢ xs - ys = xs + -ys

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys => simp_all [Int.sub_eq_add_neg]

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ (ys : IntList), xs - ys = xs + -ys
⊢ x :: xs - [] = x :: xs + -[]

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem length_rowLens {μ : YoungDiagram} : μ.rowLens.length = μ.colLen 0

Proof state:
μ : YoungDiagram
⊢ μ.rowLens.length = μ.colLen 0

Tactic:
simp only [rowLens, List.length_map, List.length_range]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma exists_mul_self (x : ℕ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x :=
  ⟨fun ⟨n, hn⟩ ↦ by rw [← hn, sqrt_eq], fun h ↦ ⟨sqrt x, h⟩⟩

Proof state:
x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ x.sqrt * x.sqrt = x

Tactic:
rw [← hn, sqrt_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.compIso_hom_comp_image_ι [HasImage f] [IsIso g] :
    (image.compIso f g).hom ≫ image.ι (f ≫ g) = image.ι f ≫ g

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g

Tactic:
simp [image.compIso]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).hom ≫ ι (f ≫ g) = ι f ≫ g

Tactic:
ext

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast_range' (n : Nat) (h) : (range' s n).getLast h = s + n - 1

Proof state:
case zero
s : Nat
h : range' s 0 ≠ []
⊢ (range' s 0).getLast h = s + 0 - 1

Tactic:
simp at h

Result:
no goals

Proof state:
case succ
s n : Nat
h : range' s (n + 1) ≠ []
⊢ (range' s (n + 1)).getLast h = s + (n + 1) - 1

Tactic:
simp [getLast?_range', getLast_eq_iff_getLast_eq_some]

Result:
no goals

Proof state:
s n : Nat
h : range' s n ≠ []
⊢ (range' s n).getLast h = s + n - 1

Tactic:
cases n with
| zero => simp at h
| succ n => simp [getLast?_range', getLast_eq_iff_getLast_eq_some]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_eq_bot_iff {f : R[T;T⁻¹]} : f.degree = ⊥ ↔ f = 0

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f n = 0 n

Tactic:
simp only [coe_zero, Pi.zero_apply]

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f n = 0

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f n = 0

Tactic:
simp_rw [degree, Finset.max_eq_sup_withBot, Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne,
  WithBot.coe_ne_bot, imp_false, not_not] at h

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), f s = 0
⊢ f n = 0

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), f s = 0
⊢ f n = 0

Tactic:
exact h n

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ f.degree = ⊥ ↔ f = 0

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, degree_zero]⟩

Result:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
⊢ f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ f.degree = ⊥

Tactic:
rw [h, degree_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
⊢ f = 0

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ f n = 0 n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
    (ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx]'hbounds = aig.decls[idx]

Proof state:
case gate
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig rhs atomHandler).val.aig.decls.size),
    (go aig rhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.gate g lhs rhs) atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go aig lhs atomHandler).val.aig.decls.size
this :
  (go aig lhs atomHandler).val.aig.decls.size ≤ (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
lih : (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
⊢ (go aig (BoolExpr.gate g lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Tactic:
specialize rih (go aig lhs atomHandler).val.aig (by omega) (by omega)

Result:
case gate
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
g : Gate
lhs rhs : BoolExpr α
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (BoolExpr.gate g lhs rhs) atomHandler).val.aig.decls.size
this✝ : aig.decls.size ≤ (go aig lhs atomHandler).val.aig.decls.size
this :
  (go aig lhs atomHandler).val.aig.decls.size ≤ (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
lih : (go aig lhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
rih :
  (go (go aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls[idx] = (go aig lhs atomHandler).val.aig.decls[idx]
⊢ (go aig (BoolExpr.gate g lhs rhs) atomHandler).val.aig.decls[idx] = aig.decls[idx]

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
idx : Nat
discr lhs rhs : BoolExpr α
rih :
  ∀ (aig : AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig rhs atomHandler).val.aig.decls.size),
    (go aig rhs atomHandler).val.aig.decls[idx] = aig.decls[idx]
aig : AIG β
h : idx < aig.decls.size
hbounds : idx < (go aig (discr.ite lhs rhs) atomHandler).val.aig.decls.size
this✝¹ : aig.decls.size ≤ (go aig discr atomHandler).val.aig.decls.size
this✝ :
  (go aig discr atomHandler).val.aig.decls.size ≤
    (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls.size
this :
  (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls.size ≤
    (go (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig rhs atomHandler).val.aig.decls.size
dih : (go aig discr atomHandler).val.aig.decls[idx] = aig.decls[idx]
lih :
  (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls[idx] =
    (go aig discr atomHandler).val.aig.decls[idx]
⊢ idx < (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig.decls.size

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_eq_iff {a : Vector α n} {i : Nat} {h : i < n} : a[i] = x ↔ a[i]? = some x

Proof state:
α : Type u_1
n : Nat
x : α
a : Vector α n
i : Nat
h : i < n
⊢ a[i] = x ↔ ∃ h, a[i] = x

Tactic:
exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
a : Vector α n
i : Nat
h : i < n
⊢ a[i] = x ↔ a[i]? = some x

Tactic:
simp only [getElem?_eq_some_iff]

Result:
α : Type u_1
n : Nat
x : α
a : Vector α n
i : Nat
h : i < n
⊢ a[i] = x ↔ ∃ h, a[i] = x
-- Mathlib/SetTheory/Game/Basic.lean
theorem mul_moveLeft_inl {x y : PGame} {i j} :
    (x * y).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
      x.moveLeft i * y + x * y.moveLeft j - x.moveLeft i * y.moveLeft j

Proof state:
case mk
y : PGame
j : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveLeft i * y + mk α✝ β✝ a✝¹ a✝ * y.moveLeft j - (mk α✝ β✝ a✝¹ a✝).moveLeft i * y.moveLeft j

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveLeft j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * (mk α✝ β✝ a✝¹ a✝).moveLeft j

Proof state:
x y : PGame
i : x.LeftMoves
j : y.LeftMoves
⊢ (x * y).moveLeft (toLeftMovesMul (Sum.inl (i, j))) = x.moveLeft i * y + x * y.moveLeft j - x.moveLeft i * y.moveLeft j

Tactic:
cases x

Result:
case mk
y : PGame
j : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveLeft i * y + mk α✝ β✝ a✝¹ a✝ * y.moveLeft j - (mk α✝ β✝ a✝¹ a✝).moveLeft i * y.moveLeft j

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesMul (Sum.inl (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveLeft j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * (mk α✝ β✝ a✝¹ a✝).moveLeft j

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_insertIdx {α} (x : α) (l : List α) {n} (h : n ≤ l.length) :
    insertIdx n x l ~ x :: l

Proof state:
case cons.succ
α : Type u_1
x head✝ : α
tail✝ : List α
ih : ∀ {n : Nat}, n ≤ tail✝.length → insertIdx n x tail✝ ~ x :: tail✝
n✝ : Nat
h : n✝ + 1 ≤ (head✝ :: tail✝).length
⊢ insertIdx (n✝ + 1) x (head✝ :: tail✝) ~ x :: head✝ :: tail✝

Tactic:
simp only [insertIdx, modifyTailIdx]

Result:
case cons.succ
α : Type u_1
x head✝ : α
tail✝ : List α
ih : ∀ {n : Nat}, n ≤ tail✝.length → insertIdx n x tail✝ ~ x :: tail✝
n✝ : Nat
h : n✝ + 1 ≤ (head✝ :: tail✝).length
⊢ head✝ :: modifyTailIdx (cons x) n✝ tail✝ ~ x :: head✝ :: tail✝

Proof state:
case cons
α : Type u_1
x head✝ : α
tail✝ : List α
ih : ∀ {n : Nat}, n ≤ tail✝.length → insertIdx n x tail✝ ~ x :: tail✝
n : Nat
h : n ≤ (head✝ :: tail✝).length
⊢ insertIdx n x (head✝ :: tail✝) ~ x :: head✝ :: tail✝

Tactic:
cases n with
| zero => simp [insertIdx]
| succ =>
  simp only [insertIdx, modifyTailIdx]
  refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
x head✝ : α
tail✝ : List α
ih : ∀ {n : Nat}, n ≤ tail✝.length → insertIdx n x tail✝ ~ x :: tail✝
h : 0 ≤ (head✝ :: tail✝).length
⊢ insertIdx 0 x (head✝ :: tail✝) ~ x :: head✝ :: tail✝

Tactic:
simp [insertIdx]

Result:
no goals

Proof state:
α : Type u_1
x : α
l : List α
n : Nat
h : n ≤ l.length
⊢ insertIdx n x l ~ x :: l

Tactic:
induction l generalizing n with
| nil =>
  cases n with
  | zero => rfl
  | succ => cases h
| cons _ _ ih =>
  cases n with
  | zero => simp [insertIdx]
  | succ =>
    simp only [insertIdx, modifyTailIdx]
    refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)

Result:
no goals

Proof state:
case nil
α : Type u_1
x : α
n : Nat
h : n ≤ [].length
⊢ insertIdx n x [] ~ [x]

Tactic:
cases n with
| zero => rfl
| succ => cases h

Result:
no goals

Proof state:
case nil.zero
α : Type u_1
x : α
h : 0 ≤ [].length
⊢ insertIdx 0 x [] ~ [x]

Tactic:
rfl

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
x head✝ : α
tail✝ : List α
ih : ∀ {n : Nat}, n ≤ tail✝.length → insertIdx n x tail✝ ~ x :: tail✝
n✝ : Nat
h : n✝ + 1 ≤ (head✝ :: tail✝).length
⊢ head✝ :: modifyTailIdx (cons x) n✝ tail✝ ~ x :: head✝ :: tail✝

Tactic:
refine .trans (.cons _ (ih (Nat.le_of_succ_le_succ h))) (.swap ..)

Result:
no goals

Proof state:
case nil.succ
α : Type u_1
x : α
n✝ : Nat
h : n✝ + 1 ≤ [].length
⊢ insertIdx (n✝ + 1) x [] ~ [x]

Tactic:
cases h

Result:
no goals
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma orthogonal_isCompl_toSubmodule (I : LieIdeal K L) (hI : IsAtom I) :
    IsCompl I.toSubmodule (orthogonal Φ hΦ_inv I).toSubmodule

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)

Tactic:
exact orthogonal_disjoint Φ hΦ_nondeg hΦ_inv hL I hI

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)

Tactic:
rw [orthogonal_toSubmodule, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint hΦ_refl,
    ← orthogonal_toSubmodule _ hΦ_inv, ← LieSubmodule.disjoint_iff_toSubmodule]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : IsAtom I
⊢ Disjoint I (orthogonal Φ hΦ_inv I)