harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FiniteType.lean
theorem mem_closure_of_mem_span_closure [Nontrivial R] {m : M} {S : Set M}
    (h : of R M m ∈ span R (Submonoid.closure (of R M '' S) : Set (MonoidAlgebra R M))) :
    m ∈ closure S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : (of R M) m ∈ span R ↑(Submonoid.map (of R M) (closure S))
⊢ m ∈ closure S

Tactic:
simpa using of_mem_span_of_iff.1 h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : (of R M) m ∈ span R ↑(closure (⇑(of R M) '' S))
⊢ m ∈ closure S

Tactic:
rw [← MonoidHom.map_mclosure] at h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : (of R M) m ∈ span R ↑(Submonoid.map (of R M) (closure S))
⊢ m ∈ closure S
-- Mathlib/Data/Finset/Dedup.lean
theorem _root_.List.toFinset_toList [DecidableEq α] {s : List α} (hs : s.Nodup) :
    s.toFinset.toList.Perm s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.Perm s

Tactic:
apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs

Result:
α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset

Tactic:
rw [toList_toFinset]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem sorted_cons_cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α} :
    Sorted r (b :: a :: l) ↔ r b a ∧ Sorted r (a :: l)

Proof state:
case mpr
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
⊢ r b a ∧ Sorted r (a :: l) → Sorted r (b :: a :: l)

Tactic:
rintro ⟨h, ha⟩

Result:
case mpr.intro
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
h : r b a
ha : Sorted r (a :: l)
⊢ Sorted r (b :: a :: l)

Proof state:
case mp
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
h : Sorted r (b :: a :: l)
⊢ r b a ∧ Sorted r (a :: l)

Tactic:
exact ⟨rel_of_sorted_cons h _ (mem_cons_self a _), h.of_cons⟩

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
⊢ Sorted r (b :: a :: l) ↔ r b a ∧ Sorted r (a :: l)

Tactic:
constructor

Result:
case mp
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
⊢ Sorted r (b :: a :: l) → r b a ∧ Sorted r (a :: l)

case mpr
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
⊢ r b a ∧ Sorted r (a :: l) → Sorted r (b :: a :: l)

Proof state:
case mpr.intro
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
h : r b a
ha : Sorted r (a :: l)
⊢ Sorted r (b :: a :: l)

Tactic:
exact ha.cons h

Result:
no goals

Proof state:
case mp
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
⊢ Sorted r (b :: a :: l) → r b a ∧ Sorted r (a :: l)

Tactic:
intro h

Result:
case mp
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
l : List α
a b : α
h : Sorted r (b :: a :: l)
⊢ r b a ∧ Sorted r (a :: l)
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem SurjectiveOnWith.exists_pos {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ}
    (h : f.SurjectiveOnWith K C) : ∃ C' > 0, f.SurjectiveOnWith K C'

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'

Tactic:
refine ⟨|C| + 1, ?_, ?_⟩

Result:
case refine_1
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ |C| + 1 > 0

case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)

Proof state:
case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)

Tactic:
apply h.mono

Result:
case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ C ≤ |C| + 1

Proof state:
case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ C ≤ |C| + 1

Tactic:
linarith [le_abs_self C]

Result:
no goals

Proof state:
case refine_1
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ |C| + 1 > 0

Tactic:
linarith [abs_nonneg C]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem algebraMap_apply' (r : R) :
    algebraMap R (A ⊗[R] B) r = 1 ⊗ₜ algebraMap R B r

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (algebraMap R (A ⊗[R] B)) r = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists {a : A} {z : ℂ} :
    z ∈ spectrum ℂ a ↔ ∃ f : characterSpace ℂ A, f a = z

Proof state:
case refine_1.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ A)
hf : (algebraMap ℂ ℂ) z = f a
⊢ ∃ f, f a = z

Tactic:
exact ⟨_, hf.symm⟩

Result:
no goals

Proof state:
case refine_1.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ A)
hf : f ((algebraMap ℂ A) z - a) = 0
⊢ ∃ f, f a = z

Tactic:
simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf

Result:
case refine_1.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ A)
hf : (algebraMap ℂ ℂ) z = f a
⊢ ∃ f, f a = z

Proof state:
case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ (∃ f, f a = z) → z ∈ spectrum ℂ a

Tactic:
rintro ⟨f, rfl⟩

Result:
case refine_2.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
f : ↑(characterSpace ℂ A)
⊢ f a ∈ spectrum ℂ a

Proof state:
case refine_1
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ f, f a = z

Tactic:
obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz

Result:
case refine_1.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ A)
hf : f ((algebraMap ℂ A) z - a) = 0
⊢ ∃ f, f a = z

Proof state:
case refine_2.intro
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
f : ↑(characterSpace ℂ A)
⊢ f a ∈ spectrum ℂ a

Tactic:
exact AlgHom.apply_mem_spectrum f a

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ spectrum ℂ a ↔ ∃ f, f a = z

Tactic:
refine ⟨fun hz => ?_, ?_⟩

Result:
case refine_1
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ f, f a = z

case refine_2
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ (∃ f, f a = z) → z ∈ spectrum ℂ a
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lintegral_eq_of_lmarginal_eq [Fintype δ] (s : Finset δ) {f g : (∀ i, π i) → ℝ≥0∞}
    (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ) :
    ∫⁻ x, f x ∂Measure.pi μ = ∫⁻ x, g x ∂Measure.pi μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
rcases isEmpty_or_nonempty (∀ i, π i) with h|⟨⟨x⟩⟩

Result:
case inl
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → π i)
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

case inr.intro
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → π i
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Proof state:
case inl
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → π i)
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
simp_rw [lintegral_of_isEmpty]

Result:
no goals

Proof state:
case inr.intro
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → π i
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ

Tactic:
simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_one : fract (1 : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ fract 1 = 0

Tactic:
simp [fract]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem rangeKerLift_injective : Injective (rangeKerLift φ) := fun a b =>
  Quotient.inductionOn₂' a b fun a b (h : φ.rangeRestrict a = φ.rangeRestrict b) =>
    Quotient.sound' <| by
      rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]

Proof state:
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ (leftRel φ.ker) a b

Tactic:
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
  φ.rangeRestrict.map_inv, inv_mul_cancel]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem zero_left {b : ℕ} (hb : 1 < b) : J(0 | b) = 0 :=
  (@eq_zero_iff_not_coprime 0 b ⟨ne_zero_of_lt hb⟩).mpr <| by
    rw [Int.gcd_zero_left, Int.natAbs_ofNat]; exact hb.ne'

Proof state:
b : ℕ
hb : 1 < b
⊢ Int.gcd 0 ↑b ≠ 1

Tactic:
rw [Int.gcd_zero_left, Int.natAbs_ofNat]

Result:
b : ℕ
hb : 1 < b
⊢ b ≠ 1

Proof state:
b : ℕ
hb : 1 < b
⊢ b ≠ 1

Tactic:
exact hb.ne'

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma lift_le_ofENat {x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x ≤ m ↔ x ≤ m

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m

Tactic:
rw [← lift_ofENat.{u, v}, lift_le]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_one_of_forall_eq_one {f : α → M} (h : ∀ x, f x = 1) : ∏ᶠ i, f i = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
h : ∀ (x : α), f x = 1
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
simp +contextual [h]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma contractible_distinguished (X : Cᵒᵖ) :
    contractibleTriangle X ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop),
  ⟨contractibleTriangleIso X⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ contractibleTriangle X ∈ distinguishedTriangles C

Tactic:
rw [mem_distinguishedTriangles_iff']

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ ∃ T',
    ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
      Nonempty (contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
theorem blastConst.go_decl_eq {aig : AIG α} (i : Nat) (s : AIG.RefVec aig i) (val : BitVec w)
    (hi : i ≤ w) :
    ∀ (curr : Nat) (h1) (h2),
        (go aig val i s hi).aig.decls[curr]'h2 = aig.decls[curr]'h1

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefVec i
val : BitVec w
hi : i ≤ w
res : AIG.RefVecEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref)
            ⋯).aig.decls.size
⊢ (aig.mkConstCached (val.getLsbD i)).aig.decls[curr] = aig.decls[curr]

case isTrue.h1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefVec i
val : BitVec w
hi : i ≤ w
res : AIG.RefVecEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref)
            ⋯).aig.decls.size
⊢ curr < (aig.mkConstCached (val.getLsbD i)).aig.decls.size

Tactic:
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]

Result:
case isTrue.h2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
i : Nat
s : aig.RefVec i
val : BitVec w
hi : i ≤ w
res : AIG.RefVecEntry α w
h✝ : i < w
hgo :
  go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkConstCached (val.getLsbD i)).aig val (i + 1) ((s.cast ⋯).push (aig.mkConstCached (val.getLsbD i)).ref)
            ⋯).aig.decls.size
⊢ curr < (aig.mkConstCached (val.getLsbD i)).aig.decls.size
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_pi_of_isCoseparator {β : Type w} (f : β → C) [HasProduct f] (b : β)
    (hb : IsCoseparator (f b)) : IsCoseparator (∏ᶜ f) :=
  (isCoseparator_pi _).2 <| IsCoseparating.mono hb <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
b : β
hb : IsCoseparator (f b)
⊢ {f b} ⊆ Set.range f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Pi/Basic.lean
lemma isIso_pi_iff {X Y : ∀ i, C i} (f : X ⟶ Y) :
    IsIso f ↔ ∀ i, IsIso (f i)

Proof state:
case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ IsIso f

Tactic:
exact ⟨fun i => inv (f i), by aesop_cat, by aesop_cat⟩

Result:
no goals

Proof state:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

Tactic:
intro _ i

Result:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : IsIso f
i : I
⊢ IsIso (f i)

Proof state:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)

Tactic:
constructor

Result:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f

Proof state:
case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ (∀ (i : I), IsIso (f i)) → IsIso f

Tactic:
intro

Result:
case mpr
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ IsIso f

Proof state:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (f ≫ fun i => inv (f i)) = 𝟙 X

Tactic:
aesop_cat

Result:
no goals

Proof state:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (fun i => inv (f i)) ≫ f = 𝟙 Y

Tactic:
aesop_cat

Result:
no goals

Proof state:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : IsIso f
i : I
⊢ IsIso (f i)

Tactic:
exact (Pi.isoApp (asIso f) i).isIso_hom

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem leftInverse_rangeSplitting (f : α → β) :
    LeftInverse (rangeFactorization f) (rangeSplitting f) := fun x => by
  ext
  simp only [rangeFactorization_coe]
  apply apply_rangeSplitting

Proof state:
case a
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x

Tactic:
simp only [rangeFactorization_coe]

Result:
case a
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ f (rangeSplitting f x) = ↑x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
ext

Result:
case a
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x

Proof state:
case a
α : Type u_1
β : Type u_2
f : α → β
x : ↑(range f)
⊢ f (rangeSplitting f x) = ↑x

Tactic:
apply apply_rangeSplitting

Result:
no goals
-- Mathlib/RingTheory/DualNumber.lean
lemma isMaximal_span_singleton_eps [DivisionRing K] :
    (Ideal.span {ε} : Ideal K[ε]).IsMaximal

Proof state:
case refine_2.inr.inr
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < ⊤
⊢ ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Ideal.span {ε} ≠ ⊤

Tactic:
simp [ne_eq, Ideal.eq_top_iff_one, Ideal.mem_span_singleton', TrivSqZeroExt.ext_iff]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : DivisionRing K
⊢ (Ideal.span {ε}).IsMaximal

Tactic:
refine ⟨?_, fun I hI ↦ ?_⟩

Result:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Ideal.span {ε} ≠ ⊤

case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
⊢ I = ⊤

Proof state:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
⊢ I = ⊤

Tactic:
rcases ideal_trichotomy I with rfl|rfl|rfl <;>
first | simp at hI | simp

Result:
no goals

Proof state:
case refine_2.inr.inl
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < Ideal.span {ε}
⊢ Ideal.span {ε} = ⊤

Tactic:
simp at hI

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_iff_isRelPrime {m n : ℕ} : m.Coprime n ↔ IsRelPrime m n

Proof state:
m n : ℕ
⊢ m.Coprime n ↔ IsRelPrime m n

Tactic:
simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]

Result:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m.gcd n → d ∣ 1
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup_inf_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α}
    (hf : Monotone f) (hg : Monotone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Proof state:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ i, f i.1 ⊓ g i.2 ≤ ⨆ i, f i ⊓ g i

Tactic:
refine iSup_mono' fun i => ?_

Result:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
⊢ ∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Proof state:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Tactic:
refine (le_iSup_inf_iSup f g).antisymm ?_

Result:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ i, f i) ⊓ ⨆ i, g i ≤ ⨆ i, f i ⊓ g i

Proof state:
case intro.intro
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.1 ≤ j
h₂ : i.2 ≤ j
⊢ ∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Tactic:
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩

Result:
no goals

Proof state:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ (⨆ i, f i) ⊓ ⨆ i, g i ≤ ⨆ i, f i ⊓ g i

Tactic:
rw [iSup_inf_iSup]

Result:
α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ i, f i.1 ⊓ g i.2 ≤ ⨆ i, f i ⊓ g i
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem pow_sub_dvd_iterate_derivative_of_pow_dvd {p q : R[X]} {n : ℕ} (m : ℕ)
    (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ derivative^[m] p

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n m : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - m) ∣ (⇑derivative)^[m] p

Tactic:
induction m generalizing p with
| zero => simpa
| succ m ih =>
  rw [Nat.sub_succ, Function.iterate_succ']
  exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - 0) ∣ (⇑derivative)^[0] p

Tactic:
simpa

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative)^[m + 1] p

Tactic:
rw [Nat.sub_succ, Function.iterate_succ']

Result:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p

Tactic:
exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

Result:
no goals