harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_eq_default [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α}
    (h : containsKey a l = false) : getValue! a l = default

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
h : getValue? a l = none
⊢ getValue! a l = default

Tactic:
rw [getValue!_eq_getValue?, h, Option.get!_none]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
h : containsKey a l = false
⊢ getValue! a l = default

Tactic:
rw [containsKey_eq_isSome_getValue?, Bool.eq_false_iff, ne_eq, Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
h : getValue? a l = none
⊢ getValue! a l = default
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_sSup {s : Set Cardinal} (hs : BddAbove s) :
    lift.{u} (sSup s) = sSup (lift.{u} '' s)

Proof state:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c

Tactic:
intro c hc

Result:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
⊢ lift.{u, u_1} (sSup s) ≤ c

Proof state:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
⊢ lift.{u, u_1} (sSup s) ≤ c

Tactic:
by_contra h

Result:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ c
⊢ False

Proof state:
case intro.intro
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)

Tactic:
exact lift_le.2 (le_csSup hs hj)

Result:
no goals

Proof state:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ False

Tactic:
simp_rw [lift_le] at h hc

Result:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False

Proof state:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False

Tactic:
rw [csSup_le_iff' hs] at h

Result:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False

Proof state:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)

Tactic:
rintro i ⟨j, hj, rfl⟩

Result:
case intro.intro
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)

Proof state:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False

Tactic:
exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)

Result:
no goals

Proof state:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
hc : c ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ c
⊢ False

Tactic:
obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le

Result:
case intro
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ False

Proof state:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

Tactic:
apply ((le_csSup_iff' (bddAbove_image.{_,u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)

Result:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c

s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_right_Ioc (a b c : α) :
    (Ioc a b).map (addRightEmbedding c) = Ioc (a + c) (b + c)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ioc _ _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ioc, coe_Ioc]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem norm_inner_symm (x y : F) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖⟪x, y⟫_𝕜‖ = ‖⟪y, x⟫_𝕜‖

Tactic:
rw [← inner_conj_symm, norm_conj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_zip_eq_zipWith (f : α × β → γ) (l : Vector α n) (l' : Vector β n) :
    map f (l.zip l') = zipWith (Function.curry f) l l'

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : Array α
l' : Vector β l.size
⊢ map f ({ toArray := l, size_toArray := ⋯ }.zip l') = zipWith (Function.curry f) { toArray := l, size_toArray := ⋯ } l'

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : Array α
l' : Array β
h : l'.size = l.size
⊢ map f ({ toArray := l, size_toArray := ⋯ }.zip { toArray := l', size_toArray := h }) =
    zipWith (Function.curry f) { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : Array α
l' : Array β
h : l'.size = l.size
⊢ map f ({ toArray := l, size_toArray := ⋯ }.zip { toArray := l', size_toArray := h }) =
    zipWith (Function.curry f) { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }

Tactic:
simp [Array.map_zip_eq_zipWith]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α × β → γ
l : Vector α n
l' : Vector β n
⊢ map f (l.zip l') = zipWith (Function.curry f) l l'

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : Array α
l' : Vector β l.size
⊢ map f ({ toArray := l, size_toArray := ⋯ }.zip l') = zipWith (Function.curry f) { toArray := l, size_toArray := ⋯ } l'
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma zero_lt_pairingIn_iff :
    0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i

Tactic:
rw [← B.zero_lt_apply_root_root_iff, ← B.isSymm_posForm.eq, RingHom.id_apply,
  B.zero_lt_apply_root_root_iff]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_eq_of_sub_lt (h : v (y - x) < v x) : v y = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v (y - x) ⊔ v x
⊢ v y = v x

Tactic:
rw [max_eq_right (le_of_lt h)] at this

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v x
⊢ v y = v x

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
⊢ v y = v x

Tactic:
have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v (y - x) < v x
this : v (y - x + x) = v (y - x) ⊔ v x
⊢ v y = v x
-- Mathlib/Order/Hom/Lattice.lean
theorem withTopWithBot_comp (f : LatticeHom β γ) (g : LatticeHom α β) :
    (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
ext

Result:
case h
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝

Proof state:
case h
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem zmod_congr_of_sub_mem_max_ideal (x : ℤ_[p]) (m n : ℕ) (hm : x - m ∈ maximalIdeal ℤ_[p])
    (hn : x - n ∈ maximalIdeal ℤ_[p]) : (m : ZMod p) = n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : (ZMod.castHom ⋯ (ZMod p)) ↑↑m = (ZMod.castHom ⋯ (ZMod p)) ↑↑n
⊢ ↑m = ↑n

Tactic:
simp only [map_intCast] at this

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
simpa only [Int.cast_natCast] using this

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p) at this

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : (ZMod.castHom ⋯ (ZMod p)) ↑↑m = (ZMod.castHom ⋯ (ZMod p)) ↑↑n
⊢ ↑m = ↑n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
⊢ ↑m = ↑n

Tactic:
have := zmod_congr_of_sub_mem_span_aux 1 x m n

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p ^ 1} → x - ↑↑n ∈ Ideal.span {↑p ^ 1} → ↑↑m = ↑↑n
⊢ ↑m = ↑n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p} → x - ↑↑n ∈ Ideal.span {↑p} → ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
specialize this hm hn

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ p ∣ p ^ 1

Tactic:
rw [pow_one]

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p ^ 1} → x - ↑↑n ∈ Ideal.span {↑p ^ 1} → ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
simp only [pow_one] at this

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : x - ↑↑m ∈ Ideal.span {↑p} → x - ↑↑n ∈ Ideal.span {↑p} → ↑↑m = ↑↑n
⊢ ↑m = ↑n

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n

Tactic:
rw [maximalIdeal_eq_span_p] at hm hn

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
⊢ ↑m = ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_emod_unique {a b r q : Int} (h : 0 < b) :
  a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b

Proof state:
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q

Tactic:
rw [Int.add_mul_ediv_left r q (Int.ne_of_gt h), ediv_eq_zero_of_lt hz hb]

Result:
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ 0 + q = q

Proof state:
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b

Tactic:
constructor

Result:
case mp
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < b

case mpr
a b r q : Int
h : 0 < b
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < b → a / b = q ∧ a % b = r

Proof state:
case mpr
a b r q : Int
h : 0 < b
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < b → a / b = q ∧ a % b = r

Tactic:
intro ⟨rfl, hz, hb⟩

Result:
case mpr
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Proof state:
case mp
a b r q : Int
h : 0 < b
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < b

Tactic:
intro ⟨rfl, rfl⟩

Result:
case mp
a b r q : Int
h : 0 < b
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < b

Proof state:
case mp
a b r q : Int
h : 0 < b
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < b

Tactic:
exact ⟨emod_add_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩

Result:
no goals

Proof state:
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ 0 + q = q

Tactic:
simp [Int.zero_add]

Result:
no goals

Proof state:
case mpr.right
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) % b = r

Tactic:
rw [add_mul_emod_self_left, emod_eq_of_lt hz hb]

Result:
no goals

Proof state:
case mpr
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Tactic:
constructor

Result:
case mpr.left
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) / b = q

case mpr.right
a b r q : Int
h : 0 < b
hz : 0 ≤ r
hb : r < b
⊢ (r + b * q) % b = r
-- Mathlib/Computability/TuringMachine.lean
theorem step_run {k : K} (q : TM2.Stmt Γ Λ σ) (v : σ) (S : ∀ k, List (Γ k)) : ∀ s : StAct K Γ σ k,
    TM2.stepAux (stRun s q) v S = TM2.stepAux q (stVar v (S k) s) (update S k (stWrite v (S k) s))
  | StAct.push _ => rfl
  | StAct.peek f => by unfold stWrite; rw [Function.update_eq_self]; rfl
  | StAct.pop _ => rfl

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f)) (update S k (stWrite v (S k) (StAct.peek f)))

Tactic:
unfold stWrite

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f))
      (update S k
        (match StAct.peek f with
        | StAct.push f => f v :: S k
        | StAct.peek a => S k
        | StAct.pop a => (S k).tail))

Tactic:
rw [Function.update_eq_self]

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S = TM2.stepAux q (stVar v (S k) (StAct.peek f)) S

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem norm_sq_eq_add_norm_sq_projection (x : E) (S : Submodule 𝕜 E) [HasOrthogonalProjection S] :
    ‖x‖ ^ 2 = ‖orthogonalProjection S x‖ ^ 2 + ‖orthogonalProjection Sᗮ x‖ ^ 2 :=
  calc
    ‖x‖ ^ 2 = ‖(orthogonalProjection S x : E) + orthogonalProjection Sᗮ x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection S
⊢ ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ *
      ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ =
    ‖(orthogonalProjection S) x‖ * ‖(orthogonalProjection S) x‖ +
      ‖(orthogonalProjection Sᗮ) x‖ * ‖(orthogonalProjection Sᗮ) x‖

Tactic:
exact norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
  (S.mem_orthogonal _).1 (orthogonalProjection Sᗮ x).2 _ (orthogonalProjection S x).2

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection S
⊢ ‖x‖ ^ 2 = ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ ^ 2

Tactic:
rw [orthogonalProjection_add_orthogonalProjection_orthogonal]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection S
⊢ ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ ^ 2 =
    ‖(orthogonalProjection S) x‖ ^ 2 + ‖(orthogonalProjection Sᗮ) x‖ ^ 2

Tactic:
simp only [sq]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection S
⊢ ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ *
      ‖↑((orthogonalProjection S) x) + ↑((orthogonalProjection Sᗮ) x)‖ =
    ‖(orthogonalProjection S) x‖ * ‖(orthogonalProjection S) x‖ +
      ‖(orthogonalProjection Sᗮ) x‖ * ‖(orthogonalProjection Sᗮ) x‖
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_mul_inv_iff₀'` for a version with multiplication on the other side. -/
lemma le_mul_inv_iff₀ (hc : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
h : a ≤ b * c⁻¹
⊢ a * c ≤ b

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_right h hc.le

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
h : a * c ≤ b
⊢ a ≤ b * c⁻¹

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 hc.le)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem dite_none_left_eq_some {p : Prop} [Decidable p] {b : ¬p → Option β} :
    (if h : p then none else b h) = some a ↔ ∃ h, b h = some a

Proof state:
β : Type u_1
a : β
p : Prop
inst✝ : Decidable p
b : ¬p → Option β
⊢ (if h : p then none else b h) = some a ↔ ∃ h, b h = some a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem traverse_eq_map_id {α β} (f : α → β) (x : List α) :
    List.traverse ((pure : _ → Id _) ∘ f) x = (pure : _ → Id _) (f <$> x)

Proof state:
case cons
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ cons (f head✝) <*> map f tail✝ = f head✝ :: map f tail✝

Tactic:
rfl

Result:
no goals

Proof state:
α β : Type u_1
f : α → β
x : List α
⊢ List.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
induction x <;> simp! [*, functor_norm]

Result:
case cons
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ cons (f head✝) <*> map f tail✝ = f head✝ :: map f tail✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_empty {c} : (empty c : Raw α β).size = 0

Proof state:
α : Type u
β : α → Type v
c : Nat
⊢ (empty c).size = 0

Tactic:
simp_to_raw using Raw₀.size_empty

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma insert_indep_iff : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Proof state:
case neg
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
simp [hI, show ¬ M.Indep (insert e I) from fun h ↦ hI <| h.subset <| subset_insert _ _]

Result:
no goals

Proof state:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
rw [hI.insert_indep_iff, and_iff_right hI, or_iff_not_imp_right]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

Tactic:
by_cases hI : M.Indep I

Result:
case pos
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

case neg
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : ¬M.Indep I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
    (replicate n a).eraseP p = replicate (n - 1) a

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : p a = true
⊢ eraseP p (replicate n a) = replicate (n - 1) a

Tactic:
cases n <;> simp [replicate_succ, h]

Result:
no goals