harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p

Proof state:
case mpr
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (i : Nat) (x : i < as.size), p as[i] = true) → ∀ (x : α), (∃ i h, as[i] = x) → p x = true

Tactic:
rintro w x ⟨i, h, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
p : α → Bool
as : Array α
w : ∀ (i : Nat) (x : i < as.size), p as[i] = true
i : Nat
h : i < as.toList.length
⊢ p as[i] = true

Proof state:
case mp
α : Type u_1
p : α → Bool
as : Array α
w : ∀ (x : α), (∃ i h, as[i] = x) → p x = true
i : Nat
h : i < as.size
⊢ p as[i] = true

Tactic:
exact w as[i] ⟨i, h, getElem_toList h⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), x ∈ as.toList → p x = true) ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

Tactic:
simp only [List.mem_iff_getElem, getElem_toList]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), (∃ i h, as[i] = x) → p x = true) ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

Proof state:
case mpr.intro.intro
α : Type u_1
p : α → Bool
as : Array α
w : ∀ (i : Nat) (x : i < as.size), p as[i] = true
i : Nat
h : i < as.toList.length
⊢ p as[i] = true

Tactic:
exact w i h

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.toList.all p = as.all p

Tactic:
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), x ∈ as.toList → p x = true) ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), (∃ i h, as[i] = x) → p x = true) ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

Tactic:
constructor

Result:
case mp
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), (∃ i h, as[i] = x) → p x = true) → ∀ (i : Nat) (x : i < as.size), p as[i] = true

case mpr
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (i : Nat) (x : i < as.size), p as[i] = true) → ∀ (x : α), (∃ i h, as[i] = x) → p x = true

Proof state:
case mp
α : Type u_1
p : α → Bool
as : Array α
⊢ (∀ (x : α), (∃ i h, as[i] = x) → p x = true) → ∀ (i : Nat) (x : i < as.size), p as[i] = true

Tactic:
intro w i h

Result:
case mp
α : Type u_1
p : α → Bool
as : Array α
w : ∀ (x : α), (∃ i h, as[i] = x) → p x = true
i : Nat
h : i < as.size
⊢ p as[i] = true
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem pNilradical_le_nilradical {R : Type*} [CommSemiring R] {p : ℕ} :
    pNilradical R p ≤ nilradical R

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : 1 < p
⊢ pNilradical R p ≤ nilradical R

Tactic:
rw [pNilradical, if_pos hp]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
⊢ pNilradical R p ≤ nilradical R

Tactic:
by_cases hp : 1 < p

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : 1 < p
⊢ pNilradical R p ≤ nilradical R

case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ pNilradical R p ≤ nilradical R

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : ¬1 < p
⊢ pNilradical R p ≤ nilradical R

Tactic:
simp_rw [pNilradical, if_neg hp, bot_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
    (l.attachWith p H).count a = l.count ↑a

Proof state:
α : Type u_1
n : Nat
inst✝ : DecidableEq α
p : α → Prop
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
a : { x // p x }
⊢ count a (l.attachWith p H) = count a.val l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
p : α → Prop
a : { x // p x }
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ count a ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    count a.val { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
p : α → Prop
a : { x // p x }
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ count a ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    count a.val { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mapRange.linearEquiv_trans (f : ∀ i, β i ≃ₗ[R] β₁ i) (f₂ : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
    (mapRange.linearEquiv fun i => (f i).trans (f₂ i)) =
      (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) :=
  LinearEquiv.ext <| mapRange_comp (fun i x => f₂ i x) (fun i x => f i x)
    (fun i => (f₂ i).map_zero) (fun i => (f i).map_zero) (by simp)

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_6
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β i ≃ₗ[R] β₁ i
f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i
⊢ ∀ (i : ι), ((fun i x => (f₂ i) x) i ∘ (fun i x => (f i) x) i) 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean
@[ext]
lemma hom_ext {M : ModuleCat.{v} R} {N : ModuleCat.{max u v} R} {n : ℕ}
    {f g : M.exteriorPower n ⟶ N}
    (h : mk.postcomp f = mk.postcomp g) : f = g

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ f = g

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ Hom.hom f = Hom.hom g

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ Hom.hom f = Hom.hom g

Tactic:
exact exteriorPower.linearMap_ext h

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.congr {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s)
    (hff' : ∀ᶠ n in p, Set.EqOn (F n) (F' n) s) : TendstoUniformlyOn F' f p s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOn F f p s
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOn F' f p s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at hf ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOnFilter F' f p (𝓟 s)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | EqOn (F x) (F' x) s} ∈ p
⊢ {x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s

Tactic:
simp only [Set.EqOn] at hff'

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | ∀ ⦃x_1 : α⦄, x_1 ∈ s → F x x_1 = F' x x_1} ∈ p
⊢ {x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | ∀ ⦃x_1 : α⦄, x_1 ∈ s → F x x_1 = F' x x_1} ∈ p
⊢ {x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s

Tactic:
simp only [mem_prod_principal, hff', mem_setOf_eq]

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ TendstoUniformlyOnFilter F' f p (𝓟 s)

Tactic:
refine hf.congr ?_

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, F n.1 n.2 = F' n.1 n.2

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : ∀ᶠ (n : ι) in p, EqOn (F n) (F' n) s
⊢ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, F n.1 n.2 = F' n.1 n.2

Tactic:
rw [eventually_iff] at hff' ⊢

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
F' : ι → α → β
hf : TendstoUniformlyOnFilter F f p (𝓟 s)
hff' : {x | EqOn (F x) (F' x) s} ∈ p
⊢ {x | F x.1 x.2 = F' x.1 x.2} ∈ p ×ˢ 𝓟 s
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice
    [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} {s : Set γ} (hsm : MeasurableSet s)
    (hs : s ⊆ (mutuallySingularSetSlice κ η a)ᶜ) :
    withDensity η (rnDeriv κ η) a s = κ a s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0

Tactic:
rw [ne_eq, sub_eq_zero]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ (κ.mutuallySingularSetSlice η a)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ ¬1 = κ.rnDerivAux (κ + η) a x
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
/-- A continuous function on a compact space has automatically compact support. This is not an
instance to avoid type class loops. -/
lemma of_compactSpace (G : Type*) [FunLike G α β]
    [ContinuousMapClass G α β] [CompactSpace α] : CompactlySupportedContinuousMapClass G α β where
  map_continuous := map_continuous
  hasCompactSupport

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
f : G
⊢ HasCompactSupport ⇑f

Tactic:
exact HasCompactSupport.of_compactSpace f

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), HasCompactSupport ⇑f

Tactic:
intro f

Result:
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
f : G
⊢ HasCompactSupport ⇑f
-- Mathlib/Data/List/Sigma.lean
theorem perm_lookupAll (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys)
    (p : l₁ ~ l₂) : lookupAll a l₁ = lookupAll a l₂

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
nd₂ : l₂.NodupKeys
p : l₁ ~ l₂
⊢ lookupAll a l₁ = lookupAll a l₂

Tactic:
simp [lookupAll_eq_dlookup, nd₁, nd₂, perm_dlookup a nd₁ nd₂ p]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_dvd_prod_of_dvd [CommMonoid β] {S : Multiset α} (g1 g2 : α → β)
    (h : ∀ a ∈ S, g1 a ∣ g2 a) : (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod

Proof state:
case h₂
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
a : α
T : Multiset α
haS : a ∈ S
a✝ : T ⊆ S
IH : (map g1 T).prod ∣ (map g2 T).prod
⊢ (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Tactic:
simp [mul_dvd_mul (h a haS) IH]

Result:
no goals

Proof state:
case h₁
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ (map g1 0).prod ∣ (map g2 0).prod

Tactic:
simp

Result:
no goals

Proof state:
case h₂
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ ∀ {a : α} {s : Multiset α},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod

Tactic:
intro a T haS _ IH

Result:
case h₂
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
a : α
T : Multiset α
haS : a ∈ S
a✝ : T ⊆ S
IH : (map g1 T).prod ∣ (map g2 T).prod
⊢ (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ (map g1 S).prod ∣ (map g2 S).prod

Tactic:
apply Multiset.induction_on' S

Result:
case h₁
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ (map g1 0).prod ∣ (map g2 0).prod

case h₂
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
S : Multiset α
g1 g2 : α → β
h : ∀ a ∈ S, g1 a ∣ g2 a
⊢ ∀ {a : α} {s : Multiset α},
    a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (m * n) = p.coeff n ^ m

Proof state:
case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)

Tactic:
rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn]

Result:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n

Proof state:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ m * p.natDegree ≤ m * n

Tactic:
exact mul_le_mul_of_nonneg_left pn m.zero_le

Result:
no goals

Proof state:
case zero
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ 0).coeff (0 * n) = p.coeff n ^ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))

Result:
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ m * p.natDegree ≤ m * n

Proof state:
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
induction' m with m hm

Result:
case zero
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ 0).coeff (0 * n) = p.coeff n ^ 0

case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ℕ) :
    (↑(MvPolynomial.finSuccEquiv R n).symm : Polynomial (MvPolynomial (Fin n) R) →+* _).comp
        (Polynomial.C.comp MvPolynomial.C) =
      (MvPolynomial.C : R →+* MvPolynomial (Fin n.succ) R)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ (Polynomial.C.comp C) x = (finSuccEquiv R n) (C x)

Tactic:
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x

Tactic:
refine
  (MvPolynomial.finSuccEquiv R n).injective
    (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ (Polynomial.C.comp C) x = (finSuccEquiv R n) (C x)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ((↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C)) x = C x

Tactic:
rw [RingHom.comp_apply]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C) = C

Tactic:
refine RingHom.ext fun x => ?_

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ((↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C)) x = C x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
    (pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (f' : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot_in_c : pivot ∈ Clause.toList c)
    (ratAddSuccess : performRatAdd f c pivot rupHints ratHints = (f', true)) :
    Equisat (PosFin n) f f'

Proof state:
case isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ Equisat (PosFin n) f f'

Tactic:
next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
rw [f'_def]
exact safe_insert_of_performRatCheck_fold_success f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
  ratHintsExhaustive_eq_true performRatCheck_fold_success

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
    (pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (f' : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot_in_c : pivot ∈ Clause.toList c)
    (ratAddSuccess : performRatAdd f c pivot rupHints ratHints = (f', true)) :
    Equisat (PosFin n) f f'

Proof state:
case isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    false
ratAddSuccess :
  ((Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
      false) =
    (f', true)
⊢ Equisat (PosFin n) f f'

Tactic:
simp at ratAddSuccess

Result:
no goals