harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/ComplexMGF.lean
theorem differentiableOn_complexMGF :
    DifferentiableOn ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)}

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ DifferentiableOn ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
intro z hz

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω => ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
rw [hasDerivAt_iff_hasFDerivAt] at h

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h :
  HasFDerivAt (complexMGF X μ) (ContinuousLinearMap.smulRight 1 (∫ (x : Ω), (fun ω => ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ))
    z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
have h := hasDerivAt_complexMGF hz

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω => ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h :
  HasFDerivAt (complexMGF X μ) (ContinuousLinearMap.smulRight 1 (∫ (x : Ω), (fun ω => ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ))
    z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
exact h.hasFDerivWithinAt.differentiableWithinAt

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
@[simp] lemma iSup_ulift {ι : Type*} [SupSet α] (f : ULift ι → α) :
    ⨆ i : ULift ι, f i = ⨆ i, f (.up i)

Proof state:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift.{u_9, u_8} ι → α
⊢ sSup (range fun i => f i) = sSup (range fun i => f { down := i })

Tactic:
congr with x

Result:
case e_a.h
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift.{u_9, u_8} ι → α
x : α
⊢ (x ∈ range fun i => f i) ↔ x ∈ range fun i => f { down := i }

Proof state:
case e_a.h
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift.{u_9, u_8} ι → α
x : α
⊢ (x ∈ range fun i => f i) ↔ x ∈ range fun i => f { down := i }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift.{u_9, u_8} ι → α
⊢ ⨆ i, f i = ⨆ i, f { down := i }

Tactic:
simp [iSup]

Result:
α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift.{u_9, u_8} ι → α
⊢ sSup (range fun i => f i) = sSup (range fun i => f { down := i })
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem uCompactlyGeneratedSpace_of_coinduced
    [UCompactlyGeneratedSpace.{u} X] {f : X → Y} (hf : Continuous f) (ht : tY = coinduced f tX) :
    UCompactlyGeneratedSpace.{u} Y

Proof state:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous f
ht : tY = coinduced f tX
⊢ UCompactlyGeneratedSpace Y

Tactic:
refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ ?_

Result:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed s

Proof state:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed s

Tactic:
rw [ht, isClosed_coinduced]

Result:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed (f ⁻¹' s)

Proof state:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed (f ⁻¹' s)

Tactic:
exact UCompactlyGeneratedSpace.isClosed fun _ ⟨g, hg⟩ ↦ h _ ⟨_, hf.comp hg⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem innerContent_bot : μ.innerContent ⊥ = 0

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ μ K ≤ μ ⊥

Tactic:
have : K = ⊥ := by
  ext1
  rw [subset_empty_iff.mp hK, Compacts.coe_bot]

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ μ K ≤ μ ⊥

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ K = ⊥

Tactic:
ext1

Result:
case h
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥

Proof state:
case h
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥

Tactic:
rw [subset_empty_iff.mp hK, Compacts.coe_bot]

Result:
no goals

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ 0

Tactic:
rw [← μ.empty]

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ μ ⊥

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ = 0

Tactic:
refine le_antisymm ?_ (zero_le _)

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ 0

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
this : K = ⊥
⊢ μ K ≤ μ ⊥

Tactic:
rw [this]

Result:
no goals

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ ≤ μ ⊥

Tactic:
refine iSup₂_le fun K hK => ?_

Result:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ μ K ≤ μ ⊥
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppScalarLeft_symm_apply_single (i : ι) (n : N) :
    (finsuppScalarLeft R N ι).symm (Finsupp.single i n) =
      (Finsupp.single i 1) ⊗ₜ[R] n

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
n : N
⊢ (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n

Tactic:
simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive]
lemma leOnePart_eq_inv_inf_one (a : α) : a⁻ᵐ = (a ⊓ 1)⁻¹

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹

Tactic:
rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem equiv_symm_eq_conj (b : B) :
    (of (φ.symm b : G) : HNNExtension G A B φ) = t⁻¹ * of (b : G) * t

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * of ↑b * t

Tactic:
rw [mul_assoc, of_mul_t]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ of ↑(φ.symm b) = t⁻¹ * (t * of ↑(φ.symm b))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vsub_vadd_comm (p₁ p₂ p₃ : P) : (p₁ -ᵥ p₂ : G) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ : P
⊢ (p₁ -ᵥ p₂) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁

Tactic:
rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]

Result:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₂ + (p₃ -ᵥ p₁ - (p₃ -ᵥ p₂)) = 0

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₂ + (p₃ -ᵥ p₁ - (p₃ -ᵥ p₂)) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_zero {n : ℕ} : (ascPochhammer S n).eval 0 = if n = 0 then 1 else 0

Proof state:
case zero
S : Type u
inst✝ : Semiring S
⊢ eval 0 (ascPochhammer S 0) = if 0 = 0 then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
S : Type u
inst✝ : Semiring S
n✝ : ℕ
⊢ eval 0 (ascPochhammer S (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0

Tactic:
simp [X_mul, Nat.succ_ne_zero, ascPochhammer_succ_left]

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0

Tactic:
cases n

Result:
case zero
S : Type u
inst✝ : Semiring S
⊢ eval 0 (ascPochhammer S 0) = if 0 = 0 then 1 else 0

case succ
S : Type u
inst✝ : Semiring S
n✝ : ℕ
⊢ eval 0 (ascPochhammer S (n✝ + 1)) = if n✝ + 1 = 0 then 1 else 0
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_of_cyclotomic_irreducible [IsDomain L] [IsCyclotomicExtension {n} K L]
    (hirr : Irreducible (cyclotomic n K)) : norm K ζ = ite (n = 2) (-1) 1

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
⊢ (Algebra.norm K) ζ = if n = 2 then -1 else 1

Tactic:
split_ifs with hn

Result:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
hn : n = 2
⊢ (Algebra.norm K) ζ = -1

case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
hn : ¬n = 2
⊢ (Algebra.norm K) ζ = 1

Proof state:
case pos
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : IsDomain L
hζ : IsPrimitiveRoot ζ ↑2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic (↑2) K)
⊢ (Algebra.norm K) ζ = -1

Tactic:
convert norm_eq_neg_one_pow (K := K) hζ

Result:
case h.e'_3
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : IsDomain L
hζ : IsPrimitiveRoot ζ ↑2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic (↑2) K)
⊢ -1 = (-1) ^ Module.finrank K L

Proof state:
case pos
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
hn : n = 2
⊢ (Algebra.norm K) ζ = -1

Tactic:
subst hn

Result:
case pos
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : IsDomain L
hζ : IsPrimitiveRoot ζ ↑2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic (↑2) K)
⊢ (Algebra.norm K) ζ = -1

Proof state:
case neg
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
hn : ¬n = 2
⊢ (Algebra.norm K) ζ = 1

Tactic:
exact hζ.norm_eq_one hn hirr

Result:
no goals

Proof state:
case h.e'_3
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : IsDomain L
hζ : IsPrimitiveRoot ζ ↑2
inst✝ : IsCyclotomicExtension {2} K L
hirr : Irreducible (cyclotomic (↑2) K)
⊢ -1 = (-1) ^ Module.finrank K L

Tactic:
erw [IsCyclotomicExtension.finrank _ hirr, totient_two, pow_one]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem IsCodetecting.isCoseparating [HasCoequalizers C] {𝒢 : Set C} :
    IsCodetecting 𝒢 → IsCoseparating 𝒢

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCoequalizers C
𝒢 : Set C
⊢ IsCodetecting 𝒢 → IsCoseparating 𝒢

Tactic:
simpa only [← isSeparating_op_iff, ← isDetecting_op_iff] using IsDetecting.isSeparating

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/ModEq.lean
theorem frequently_even : ∃ᶠ m : ℕ in atTop, Even m

Proof state:
⊢ ∃ᶠ (m : ℕ) in atTop, Even m

Tactic:
simpa only [even_iff] using frequently_mod_eq zero_lt_two

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem mem_span_repr_support (m : M) : m ∈ span R (b '' (b.repr m).support) :=
  (Finsupp.mem_span_image_iff_linearCombination _).2
    ⟨b.repr m, by simp [Finsupp.mem_supported_support]⟩

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
m : M
⊢ b.repr m ∈ supported R R ↑(b.repr m).support ∧ (linearCombination R ⇑b) (b.repr m) = m

Tactic:
simp [Finsupp.mem_supported_support]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem surjOn (f : r ≺i s) : Set.SurjOn f Set.univ { b | s b f.top }

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
⊢ Set.SurjOn (⇑f.toRelEmbedding) Set.univ {b | s b f.top}

Tactic:
intro b h

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ b ∈ ⇑f.toRelEmbedding '' Set.univ

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ b ∈ ⇑f.toRelEmbedding '' Set.univ

Tactic:
simpa using mem_range_of_rel_top _ h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.lean
theorem denote_blastNot (aig : AIG α) (target : RefVec aig w)
    (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastNot aig target).aig, (blastNot aig target).vec.get idx hidx, assign⟧
          =
        !⟦aig, target.get idx hidx, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.RefVec w
assign : α → Bool
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastNot aig target).aig, ref := (blastNot aig target).vec.get idx hidx }⟧ =
    !⟦assign, { aig := aig, ref := target.get idx hidx }⟧

Tactic:
unfold blastNot

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.RefVec w
assign : α → Bool
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (RefVec.map aig (RefVec.MapTarget.mk target mkNotCached)).aig,
        ref := (RefVec.map aig (RefVec.MapTarget.mk target mkNotCached)).vec.get idx hidx }⟧ =
    !⟦assign, { aig := aig, ref := target.get idx hidx }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.RefVec w
assign : α → Bool
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (RefVec.map aig (RefVec.MapTarget.mk target mkNotCached)).aig,
        ref := (RefVec.map aig (RefVec.MapTarget.mk target mkNotCached)).vec.get idx hidx }⟧ =
    !⟦assign, { aig := aig, ref := target.get idx hidx }⟧

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.RefVec w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastNot aig target).aig, ref := (blastNot aig target).vec.get idx hidx }⟧ =
      !⟦assign, { aig := aig, ref := target.get idx hidx }⟧

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.RefVec w
assign : α → Bool
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (blastNot aig target).aig, ref := (blastNot aig target).vec.get idx hidx }⟧ =
    !⟦assign, { aig := aig, ref := target.get idx hidx }⟧
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_pointReflection_of_ne {x y : P} (h : x ≠ y) : Sbtw R y x (pointReflection R x y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ x ≠ (pointReflection R x) y

Tactic:
nth_rw 1 [← pointReflection_self R x]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ (pointReflection R x) x ≠ (pointReflection R x) y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ (pointReflection R x) x ≠ (pointReflection R x) y

Tactic:
exact (pointReflection_involutive R x).injective.ne h

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R y x ((pointReflection R x) y)

Tactic:
refine ⟨wbtw_pointReflection _ _ _, h, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ x ≠ (pointReflection R x) y
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma scalarRTensor_apply_monomial_tmul (e : σ →₀ ℕ) (r : R) (n : N) (d : σ →₀ ℕ) :
    scalarRTensor (monomial e r ⊗ₜ[R] n) d = if e = d then r • n else 0

Proof state:
R : Type u
N : Type v
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : DecidableEq σ
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
⊢ (scalarRTensor ((monomial e) r ⊗ₜ[R] n)) d = if e = d then r • n else 0

Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem conjTranspose_col [Star α] (v : m → α) : (col ι v)ᴴ = row ι (star v)

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
⊢ (col ι v)ᴴ = row ι (star v)

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : ι
j✝ : m
⊢ (col ι v)ᴴ i✝ j✝ = row ι (star v) i✝ j✝

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : ι
j✝ : m
⊢ (col ι v)ᴴ i✝ j✝ = row ι (star v) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₂_comp {Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    YonedaCollection.map₂ F (f ≫ g) = YonedaCollection.map₂ F f ∘ YonedaCollection.map₂ F g

Proof state:
case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ F.map (eqToHom ⋯) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ map₂ F (f ≫ g) = map₂ F f ∘ map₂ F g

Tactic:
ext

Result:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : YonedaCollection F Z
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ F (f ≫ g) x✝¹).fst.app x✝ a✝ = ((map₂ F f ∘ map₂ F g) x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ F.map (eqToHom ⋯) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Proof state:
case h.h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : YonedaCollection F Z
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ F (f ≫ g) x✝¹).fst.app x✝ a✝ = ((map₂ F f ∘ map₂ F g) x✝¹).fst.app x✝ a✝

case h.h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ F.map (eqToHom ⋯) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Tactic:
all_goals simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Preconnected.ofBoxProdLeft [Nonempty β] (h : (G □ H).Preconnected) :
    G.Preconnected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
⊢ G.Preconnected

Tactic:
rintro a₁ a₂

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
⊢ G.Reachable a₁ a₂

Proof state:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ G.Reachable a₁ a₂

Tactic:
exact ⟨w.ofBoxProdLeft⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
⊢ G.Preconnected

Tactic:
classical
rintro a₁ a₂
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)
exact ⟨w.ofBoxProdLeft⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
⊢ G.Reachable a₁ a₂

Tactic:
obtain ⟨w⟩ := h (a₁, Classical.arbitrary _) (a₂, Classical.arbitrary _)

Result:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty β
h : (G □ H).Preconnected
a₁ a₂ : α
w : (G □ H).Walk (a₁, Classical.arbitrary β) (a₂, Classical.arbitrary β)
⊢ G.Reachable a₁ a₂
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem get : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.get ⟨utf8Len m₁⟩ = c
  | _, ⟨⟩ => by simpa using get_of_valid (l ++ m₁) (c :: m₂ ++ r)

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ { str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }.get
      { byteIdx := utf8Len m₁ } =
    c

Tactic:
simpa using get_of_valid (l ++ m₁) (c :: m₂ ++ r)

Result:
no goals