harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α}
    {v : β k} :
    getKeyD (m.insertIfNew k v) a fallback =
      if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getKeyD a fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a fallback : α
v : β k
⊢ (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_insertIfNew

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem List.stream_drop_eq_drop (l : List α) : Stream.drop l n = l.drop n

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ Stream.drop l n = drop n l

Tactic:
induction n generalizing l with
| zero => rfl
| succ n ih =>
  match l with
  | [] => rfl
  | _::_ => simp [Stream.drop, List.drop_succ_cons, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
l : List α
⊢ Stream.drop l 0 = drop 0 l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.drop l n = drop n l
l : List α
⊢ Stream.drop [] (n + 1) = drop (n + 1) []

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.drop l n = drop n l
l : List α
⊢ Stream.drop l (n + 1) = drop (n + 1) l

Tactic:
match l with
| [] => rfl
| _::_ => simp [Stream.drop, List.drop_succ_cons, ih]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
ih : ∀ (l : List α), Stream.drop l n = drop n l
l : List α
head✝ : α
tail✝ : List α
⊢ Stream.drop (head✝ :: tail✝) (n + 1) = drop (n + 1) (head✝ :: tail✝)

Tactic:
simp [Stream.drop, List.drop_succ_cons, ih]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_symm (h : IsAdjoinRoot S f) (h' : IsAdjoinRoot T f) :
    (h.aequiv h').symm = h'.aequiv h

Proof state:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
a✝ : T
⊢ (h.aequiv h').symm a✝ = (h'.aequiv h) a✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
⊢ (h.aequiv h').symm = h'.aequiv h

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : IsAdjoinRoot S f
h' : IsAdjoinRoot T f
a✝ : T
⊢ (h.aequiv h').symm a✝ = (h'.aequiv h) a✝
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_map' {mβ : MeasurableSpace β} {f : β → ℝ≥0∞} {g : α → β}
    (hf : AEMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) :
    ∫⁻ a, f a ∂Measure.map g μ = ∫⁻ a, f (g a) ∂μ :=
  calc
    ∫⁻ a, f a ∂Measure.map g μ = ∫⁻ a, hf.mk f a ∂Measure.map g μ :=
      lintegral_congr_ae hf.ae_eq_mk
    _ = ∫⁻ a, hf.mk f a ∂Measure.map (hg.mk g) μ

Proof state:
case e_μ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ

Tactic:
exact Measure.map_congr hg.ae_eq_mk

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map g μ =
    ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map (AEMeasurable.mk g hg) μ

Tactic:
congr 1

Result:
case e_μ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem add_left [T2Space N] [ContinuousAdd M] (h₁ : v₁ ⟂ᵥ w) (h₂ : v₂ ⟂ᵥ w) : v₁ + v₂ ⟂ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₁ : v₁ ⟂ᵥ w
h₂ : v₂ ⟂ᵥ w
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁

Result:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w

Proof state:
case neg.inl
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

case neg.inr
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
hxv : x ∈ vᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem ConvexOn.secant_mono_aux1 (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s) (hz : z ∈ s)
    (hxy : x < y) (hyz : y < z) : (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)

Tactic:
calc
  f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z) := ?_
  _ ≤ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z := hf.2 hx hz ha hb ?_
  _ = ((z - y) * f x + (y - x) * f z) / (z - x) := ?_

Result:
case calc_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z)

case calc_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

case calc_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)

Proof state:
case calc_3
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)

Tactic:
field_simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f u • f ∘ P

Proof state:
case h
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n

Tactic:
fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
⊢ ⇑f ∘ (u • P) = f u • ⇑f ∘ P

Tactic:
ext n

Result:
case h
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
u : R
n : Fin 3
⊢ (⇑f ∘ (u • P)) n = (f u • ⇑f ∘ P) n
-- Mathlib/Analysis/Convex/Strong.lean
private lemma aux_add (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a * (f x + m / (2 : ℝ) * ‖x‖ ^ 2) + b * (f y + m / (2 : ℝ) * ‖y‖ ^ 2) -
      m / (2 : ℝ) * ‖a • x + b • y‖ ^ 2
      = a * f x + b * f y + m / (2 : ℝ) * a * b * ‖x - y‖ ^ 2

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x + m / 2 * ‖x‖ ^ 2) + b * (f y + m / 2 * ‖y‖ ^ 2) - m / 2 * ‖a • x + b • y‖ ^ 2 =
    a * f x + b * f y + m / 2 * a * b * ‖x - y‖ ^ 2

Tactic:
simpa [neg_div] using aux_sub (E := E) (m := -m) ha hb hab

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lt_univ' {c} : c < univ.{u, v} ↔ ∃ c', c = lift.{max (u + 1) v, u} c' :=
  ⟨fun h => by
    let ⟨a, h', e⟩ := lt_lift_iff.1 h
    rw [← univ_id] at h'
    rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
    exact ⟨c', by simp only [e.symm, lift_lift]⟩, fun ⟨_, e⟩ => e.symm ▸ lift_lt_univ' _⟩

Proof state:
case intro
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
exact ⟨c', by simp only [e.symm, lift_lift]⟩

Result:
no goals

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
rw [← univ_id] at h'

Result:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
let ⟨a, h', e⟩ := lt_lift_iff.1 h

Result:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ c = lift.{max (u + 1) v, u} c'

Tactic:
simp only [e.symm, lift_lift]

Result:
no goals

Proof state:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < univ.{u, u + 1}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'

Tactic:
rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩

Result:
case intro
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem iSupIndep.subtype_ne_bot_le_finrank_aux
    {p : ι → Submodule R M} (hp : iSupIndep p) :
    #{ i // p i ≠ ⊥ } ≤ (finrank R M : Cardinal.{w})

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} ↑(finrank R M) = lift.{v, w} ↑(finrank R M)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)

Tactic:
calc
  Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
    hp.subtype_ne_bot_le_rank
  _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
  _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp

Result:
no goals

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
rwa [Cardinal.lift_le] at this

Result:
no goals

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ #{ i // p i ≠ ⊥ } ≤ ↑(finrank R M)

Tactic:
suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
  rwa [Cardinal.lift_le] at this

Result:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{v, w} #{ i // p i ≠ ⊥ } ≤ lift.{v, w} ↑(finrank R M)

Proof state:
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : NoZeroSMulDivisors R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} ↑(finrank R M)

Tactic:
rw [finrank_eq_rank]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Fold.lean
theorem fold.go_decl_eq {aig : AIG α} (acc : Ref aig) (i : Nat) (s : RefVec aig len)
    (f : (aig : AIG α) → BinaryInput aig → Entrypoint α) [LawfulOperator α BinaryInput f] :
    ∀ (idx : Nat) (h1) (h2),
      (go aig acc i len s f).1.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
acc : aig.Ref
i : Nat
s : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
res : Entrypoint α
h✝ : ¬i < len
hgo : { aig := aig, ref := acc } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, ref := acc }.aig.decls.size),
    { aig := aig, ref := acc }.aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
acc : aig.Ref
i : Nat
s : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
res : Entrypoint α
h✝ : ¬i < len
hgo : { aig := aig, ref := acc } = res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < { aig := aig, ref := acc }.aig.decls.size
⊢ { aig := aig, ref := acc }.aig.decls[idx✝] = aig.decls[idx✝]

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
acc : aig.Ref
i : Nat
s : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
res : Entrypoint α
hgo :
  (if hidx : i < len then
      let res := f aig { lhs := acc, rhs := s.get i hidx };
      let aig_1 := res.aig;
      let newAcc := res.ref;
      let input := s.cast ⋯;
      go aig_1 newAcc (i + 1) len input f
    else { aig := aig, ref := acc }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
split at hgo

Result:
case isTrue
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
acc : aig.Ref
i : Nat
s : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
res : Entrypoint α
h✝ : i < len
hgo :
  (let res := f aig { lhs := acc, rhs := s.get i h✝ };
    let aig_1 := res.aig;
    let newAcc := res.ref;
    let input := s.cast ⋯;
    go aig_1 newAcc (i + 1) len input f) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
acc : aig.Ref
i : Nat
s : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
res : Entrypoint α
h✝ : ¬i < len
hgo : { aig := aig, ref := acc } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLE_refl {B : C} (X : Subobject B) : ofLE X X le_rfl = 𝟙 _

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X : Subobject B
⊢ X.ofLE X ⋯ ≫ X.arrow = 𝟙 (underlying.obj X) ≫ X.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X : Subobject B
⊢ X.ofLE X ⋯ = 𝟙 (underlying.obj X)

Tactic:
apply (cancel_mono X.arrow).mp

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X : Subobject B
⊢ X.ofLE X ⋯ ≫ X.arrow = 𝟙 (underlying.obj X) ≫ X.arrow
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLenAux_append :
    ∀ (n : ℕ) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ),
      sublistsLenAux n l (g ∘ f) (r.map g ++ s) = (sublistsLenAux n l f r).map g ++ s
  | 0, l, f, g, r, s => by unfold sublistsLenAux; simp
  | _ + 1, [], _, _, _, _ => rfl
  | n + 1, a :: l, f, g, r, s => by
    unfold sublistsLenAux
    simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append,
      sublistsLenAux_append]

Proof state:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s

Tactic:
unfold sublistsLenAux

Result:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s

Proof state:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) ∘ cons a = g ∘ f ∘ cons a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) l (g ∘ f) (sublistsLenAux n l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ cons a) r)) ++ s

Tactic:
simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append,
  sublistsLenAux_append]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s

Tactic:
unfold sublistsLenAux

Result:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) l (g ∘ f) (sublistsLenAux n l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ cons a) r)) ++ s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (m.insertMany (⟨k, v⟩ :: l)).1 = ((m.insert k v).insertMany l).1

Proof state:
case cons
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
hd : (a : α) × β a
tl : List ((a : α) × β a)
⊢ m.insertListₘ (⟨k, v⟩ :: hd :: tl) = (m.insert k v).insertListₘ (hd :: tl)

Tactic:
simp [insertListₘ]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ m.insertListₘ [⟨k, v⟩] = (m.insert k v).insertListₘ []

Tactic:
simp [insertListₘ]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (m.insertMany (⟨k, v⟩ :: l)).val = ((m.insert k v).insertMany l).val

Tactic:
simp only [insertMany_eq_insertListₘ]

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
⊢ m.insertListₘ (⟨k, v⟩ :: l) = (m.insert k v).insertListₘ l

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
k : α
v : β k
⊢ m.insertListₘ (⟨k, v⟩ :: l) = (m.insert k v).insertListₘ l

Tactic:
cases l with
| nil => simp [insertListₘ]
| cons hd tl => simp [insertListₘ]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem liftAux_apply (x : L) (n : ℕ) (y : K) (h : i y = x ^ p ^ n) :
    liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
replace h := congr($(h.symm) ^ p ^ n')

Result:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : (x ^ p ^ n) ^ p ^ n' = i y ^ p ^ n'
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
have h' := Classical.choose_spec (lift_aux i p x)

Result:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
h' : i (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p n).symm (j y)