harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (p : ℕ).Prime]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) (hirr : Irreducible (cyclotomic (↑(p ^ k) : ℕ) K)) :
    discr K (hζ.powerBasis K).basis =
      (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hcycl : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
hirr : Irreducible (cyclotomic (↑(p ^ k)) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
rcases k with - | k

Result:
case zero
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ 0)
hirr : Irreducible (cyclotomic (↑(p ^ 0)) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (↑p ^ 0) / 2) * ↑↑p ^ (↑p ^ (0 - 1) * ((↑p - 1) * 0 - 1))

case succ
p : ℕ+
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime ↑p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ (k + 1 - 1) * ((↑p - 1) * (k + 1) - 1))
-- Mathlib/LinearAlgebra/Reflection.lean
lemma preReflection_preReflection (g : Dual R M) (h : f x = 2) :
    preReflection (preReflection x f y) (preReflection f (Dual.eval R M x) g) =
    (preReflection x f) ∘ₗ (preReflection y g) ∘ₗ (preReflection x f)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
h : f x = 2
m : M
⊢ m - (g m • y - (f m * g x) • y - ((g m * f y) • x - (f m * (g x * f y)) • x)) =
    m - f m • x - (g m • y - (g m * f y) • x) -
      (f m • x - (f m • x + f m • x) - ((f m * g x) • y - (f m * (g x * f y)) • x))

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
h : f x = 2
⊢ preReflection ((preReflection x f) y) ((preReflection f ((Dual.eval R M) x)) g) =
    preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f

Tactic:
ext m

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
h : f x = 2
m : M
⊢ (preReflection ((preReflection x f) y) ((preReflection f ((Dual.eval R M) x)) g)) m =
    (preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f) m

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
h : f x = 2
m : M
⊢ (preReflection ((preReflection x f) y) ((preReflection f ((Dual.eval R M) x)) g)) m =
    (preReflection x f ∘ₗ preReflection y g ∘ₗ preReflection x f) m

Tactic:
simp only [h, preReflection_apply, mul_comm (g x) (f m), mul_two, mul_assoc, Dual.eval_apply,
  LinearMap.sub_apply, LinearMap.coe_comp, LinearMap.smul_apply, smul_eq_mul, smul_sub, sub_smul,
  smul_smul, sub_mul, comp_apply, map_sub, map_smul, add_smul]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
h : f x = 2
m : M
⊢ m - (g m • y - (f m * g x) • y - ((g m * f y) • x - (f m * (g x * f y)) • x)) =
    m - f m • x - (g m • y - (g m * f y) • x) -
      (f m • x - (f m • x + f m • x) - ((f m * g x) • y - (f m * (g x * f y)) • x))
-- Mathlib/CategoryTheory/Quotient.lean
lemma natTrans_ext {F G : Quotient r ⥤ D} (τ₁ τ₂ : F ⟶ G)
    (h : whiskerLeft (Quotient.functor r) τ₁ = whiskerLeft (Quotient.functor r) τ₂) : τ₁ = τ₂ :=
  NatTrans.ext (by ext1 ⟨X⟩; exact NatTrans.congr_app h X)

Proof state:
case h.mk
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} D
F G : Quotient r ⥤ D
τ₁ τ₂ : F ⟶ G
h : whiskerLeft (functor r) τ₁ = whiskerLeft (functor r) τ₂
X : C
⊢ τ₁.app { as := X } = τ₂.app { as := X }

Tactic:
exact NatTrans.congr_app h X

Result:
no goals

Proof state:
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} D
F G : Quotient r ⥤ D
τ₁ τ₂ : F ⟶ G
h : whiskerLeft (functor r) τ₁ = whiskerLeft (functor r) τ₂
⊢ τ₁.app = τ₂.app

Tactic:
ext1 ⟨X⟩

Result:
case h.mk
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} D
F G : Quotient r ⥤ D
τ₁ τ₂ : F ⟶ G
h : whiskerLeft (functor r) τ₁ = whiskerLeft (functor r) τ₂
X : C
⊢ τ₁.app { as := X } = τ₂.app { as := X }
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasFDerivAtFilter.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasFDerivAtFilter f f' x L) (hL : Tendsto f L L) (hx : f x = x) (n : ℕ) :
    HasFDerivAtFilter f^[n] (f' ^ n) x L

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
⊢ HasFDerivAtFilter f^[n] (f' ^ n) x L

Tactic:
induction n with
| zero => exact hasFDerivAtFilter_id x L
| succ n ihn =>
  rw [Function.iterate_succ, pow_succ]
  rw [← hx] at ihn
  exact ihn.comp x hf hL

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L

Tactic:
rw [← hx] at ihn

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) (f x) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) x L
⊢ HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) x L

Tactic:
rw [Function.iterate_succ, pow_succ]

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) x L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) (f x) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') x L

Tactic:
exact ihn.comp x hf hL

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
L : Filter E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
⊢ HasFDerivAtFilter f^[0] (f' ^ 0) x L

Tactic:
exact hasFDerivAtFilter_id x L

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_eq_nil_iff_eq_zero {b n : ℕ} : digits b n = [] ↔ n = 0

Proof state:
case mp
b n : ℕ
h : b.digits n = []
⊢ n = 0

Tactic:
have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]

Result:
case mp
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = 0

Proof state:
case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Tactic:
rintro rfl

Result:
case mpr
b : ℕ
⊢ b.digits 0 = []

Proof state:
case h.e'_2
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = ofDigits b (b.digits n)

Tactic:
rw [ofDigits_digits]

Result:
no goals

Proof state:
case mp
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = 0

Tactic:
convert this

Result:
case h.e'_2
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = ofDigits b (b.digits n)

Proof state:
b n : ℕ
⊢ b.digits n = [] ↔ n = 0

Tactic:
constructor

Result:
case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Proof state:
case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

Tactic:
intro h

Result:
case mp
b n : ℕ
h : b.digits n = []
⊢ n = 0

Proof state:
case mpr
b : ℕ
⊢ b.digits 0 = []

Tactic:
simp

Result:
no goals

Proof state:
b n : ℕ
h : b.digits n = []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_zero : ⌈(0 : α)⌉₊ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
⊢ ⌈0⌉₊ = 0

Tactic:
rw [← Nat.cast_zero, ceil_natCast]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.collectedBasis_repr_of_mem (h : IsInternal A) {α : ι → Type*}
    (v : ∀ i, Basis (α i) R (A i)) {x : M} {i : ι} {a : α i} (hx : x ∈ A i) :
    (h.collectedBasis v).repr x ⟨i, a⟩ = (v i).repr ⟨x, hx⟩ a

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i : ι
a : α i
hx : x ∈ A i
⊢ ((sigmaFinsuppLequivDFinsupp R).symm
        (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x)))
      ⟨i, a⟩ =
    ((v i).repr ⟨x, hx⟩) a

Tactic:
simp [h.ofBijective_coeLinearMap_of_mem hx]

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i : ι
a : α i
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a

Tactic:
change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _

Result:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i : ι
a : α i
hx : x ∈ A i
⊢ ((sigmaFinsuppLequivDFinsupp R).symm
        (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x)))
      ⟨i, a⟩ =
    ((v i).repr ⟨x, hx⟩) a
-- Mathlib/Order/RelSeries.lean
@[simp] lemma reverse_reverse {r : Rel α α} (p : RelSeries r) : p.reverse.reverse = p

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
⊢ p.reverse.reverse = p

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma cyclesIsoSc'_hom_iCycles :
    (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).iCycles = K.iCycles j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) ≫ (K.sc' i j k).iCycles = K.iCycles j

Tactic:
simp only [ShortComplex.cyclesMap_i, shortComplexFunctor_obj_X₂, shortComplexFunctor'_obj_X₂,
  natIsoSc'_hom_app_τ₂, comp_id]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc j).iCycles = K.iCycles j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc j).iCycles = K.iCycles j

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.cyclesIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).iCycles = K.iCycles j

Tactic:
dsimp [cyclesIsoSc']

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) ≫ (K.sc' i j k).iCycles = K.iCycles j
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The completed L-function of a non-trivial Dirichlet character is differentiable everywhere. -/
lemma differentiable_completedLFunction {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :
    Differentiable ℂ (completedLFunction χ)

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
⊢ Differentiable ℂ (completedLFunction χ)

Tactic:
refine fun s ↦ differentiableAt_completedLFunction _ _ (Or.inr ?_) (Or.inr hχ)

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
s : ℂ
⊢ N ≠ 1

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ≠ 1
s : ℂ
⊢ N ≠ 1

Tactic:
exact hχ ∘ level_one' _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_neg_add_le_right {a b c : Int} (h : -c + a ≤ b) : a ≤ b + c

Proof state:
a b c : Int
h : -c + a ≤ b
⊢ a ≤ b + c

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a + -c ≤ b
⊢ a ≤ b + c

Proof state:
a b c : Int
h : a + -c ≤ b
⊢ a ≤ b + c

Tactic:
exact Int.le_add_of_sub_right_le h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.Inv_gateToCNF {aig : AIG Nat} {h}
    (heq : aig.decls[upper]'h = .gate lhs rhs linv rinv) :
    State.Inv
      (aig := aig)
      (Decl.gateToCNF
        (.inr ⟨upper, h⟩)
        (.inr ⟨lhs, by have := aig.invariant h heq; omega⟩)
        (.inr ⟨rhs, by have := aig.invariant h heq; omega⟩)
        linv
        rinv)

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ rhs < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ rhs < aig.decls.size

Tactic:
have := aig.invariant h heq

Result:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ rhs < aig.decls.size

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ Inv (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv)

Tactic:
intro assign1

Result:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1)
    (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv)

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ lhs < aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ lhs < aig.decls.size

Tactic:
have := aig.invariant h heq

Result:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ lhs < aig.decls.size

Proof state:
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1)
    (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv)

Tactic:
simp [CNF.sat_def, denote_idx_gate heq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem sub_self [NeZero n] {x : Fin n} : x - x = 0

Proof state:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑(x - x) = ↑0

Tactic:
rw [Fin.sub_def]

Result:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑⟨(n - ↑x + ↑x) % n, ⋯⟩ = ↑0

Proof state:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑⟨(n - ↑x + ↑x) % n, ⋯⟩ = ↑0

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ x - x = 0

Tactic:
ext

Result:
case h
n : Nat
inst✝ : NeZero n
x : Fin n
⊢ ↑(x - x) = ↑0
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.comp (hh₂ : HasStrictDerivAt h₂ h₂' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x

Tactic:
exact hh₂.scomp x hh

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
rw [mul_comm]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Vector α n} :
    (x, i) ∈ l.zipIdx ↔ l[i]? = x

Proof state:
case mk
α : Type u_1
x : α
i : Nat
l : Array α
⊢ (x, i) ∈ { toArray := l, size_toArray := ⋯ }.zipIdx ↔ { toArray := l, size_toArray := ⋯ }[i]? = some x

Tactic:
simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
i : Nat
l : Vector α n
⊢ (x, i) ∈ l.zipIdx ↔ l[i]? = some x

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
x : α
i : Nat
l : Array α
⊢ (x, i) ∈ { toArray := l, size_toArray := ⋯ }.zipIdx ↔ { toArray := l, size_toArray := ⋯ }[i]? = some x
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_comp {N' : Type*} [AddCommGroup N'] [Module R N'] (f : N' →ₗ[R] M) :
    associatedHom S (Q.comp f) = (associatedHom S Q).compl₁₂ f f

Proof state:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : IsScalarTower S R N
inst✝² : Invertible 2
Q : QuadraticMap R M N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N' →ₗ[R] M
x✝¹ x✝ : N'
⊢ (((associatedHom S) (Q.comp f)) x✝¹) x✝ = ((LinearMap.compl₁₂ ((associatedHom S) Q) f f) x✝¹) x✝

Tactic:
simp only [associated_apply, comp_apply, map_add, LinearMap.compl₁₂_apply]

Result:
no goals

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : IsScalarTower S R N
inst✝² : Invertible 2
Q : QuadraticMap R M N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N' →ₗ[R] M
⊢ (associatedHom S) (Q.comp f) = LinearMap.compl₁₂ ((associatedHom S) Q) f f

Tactic:
ext

Result:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : IsScalarTower S R N
inst✝² : Invertible 2
Q : QuadraticMap R M N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N' →ₗ[R] M
x✝¹ x✝ : N'
⊢ (((associatedHom S) (Q.comp f)) x✝¹) x✝ = ((LinearMap.compl₁₂ ((associatedHom S) Q) f f) x✝¹) x✝
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[ext] lemma Hom.ext' {X Y : LocallyRingedSpace.{u}} {f g : X ⟶ Y} (h : f.toShHom = g.toShHom) :
    f = g

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
h : toShHom f = toShHom g
⊢ f = g

Tactic:
cases f

Result:
case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toShHom = toShHom g
⊢ { toHom := toHom✝, prop := prop✝ } = g

Proof state:
case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toShHom = { toHom := toHom✝, prop := prop✝ }.toShHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toShHom = toShHom g
⊢ { toHom := toHom✝, prop := prop✝ } = g

Tactic:
cases g

Result:
case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toShHom = { toHom := toHom✝, prop := prop✝ }.toShHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_mono_smul {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ ∞) (h0 : c ≠ 0)
    (hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂) : (mkMetric m₁ : Measure X) ≤ c • mkMetric m₂ := fun s ↦ by
  rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric]
  exact OuterMeasure.mkMetric_mono_smul hc h0 hle s

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ (OuterMeasure.mkMetric m₁) s ≤ (c • ⇑(OuterMeasure.mkMetric m₂)) s

Tactic:
exact OuterMeasure.mkMetric_mono_smul hc h0 hle s

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ (mkMetric m₁) s ≤ (c • mkMetric m₂) s

Tactic:
rw [← OuterMeasure.coe_mkMetric, coe_smul, ← OuterMeasure.coe_mkMetric]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
s : Set X
⊢ (OuterMeasure.mkMetric m₁) s ≤ (c • ⇑(OuterMeasure.mkMetric m₂)) s