harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem include_range (A : Type v) [Semiring A] (B : Type w) [Semiring B]
    [Algebra R A] [Algebra R B] :
    (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B).range.LinearDisjoint
      (Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).range

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((toSubmodule Algebra.TensorProduct.includeLeft.range).mulMap
        (toSubmodule Algebra.TensorProduct.includeRight.range))

Tactic:
change Function.Injective <|
  Submodule.mulMap (LinearMap.range Algebra.TensorProduct.includeLeft)
    (LinearMap.range Algebra.TensorProduct.includeRight)

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((LinearMap.range Algebra.TensorProduct.includeLeft).mulMap (LinearMap.range Algebra.TensorProduct.includeRight))

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Algebra.TensorProduct.includeLeft.range.LinearDisjoint Algebra.TensorProduct.includeRight.range

Tactic:
rw [Subalgebra.LinearDisjoint, Submodule.linearDisjoint_iff]

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((toSubmodule Algebra.TensorProduct.includeLeft.range).mulMap
        (toSubmodule Algebra.TensorProduct.includeRight.range))

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective
    ⇑((LinearMap.range Algebra.TensorProduct.includeLeft).mulMap (LinearMap.range Algebra.TensorProduct.includeRight))

Tactic:
rw [← Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap]

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective ⇑↑(Algebra.TensorProduct.linearEquivIncludeRange R A B).symm

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
B : Type w
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective ⇑↑(Algebra.TensorProduct.linearEquivIncludeRange R A B).symm

Tactic:
exact LinearEquiv.injective _

Result:
no goals
-- Mathlib/Topology/JacobsonSpace.lean
lemma Topology.IsOpenEmbedding.preimage_closedPoints (hf : IsOpenEmbedding f) [JacobsonSpace Y] :
    f ⁻¹' closedPoints Y = closedPoints X

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ x ∈ f ⁻¹' closedPoints Y

Tactic:
apply isClosed_singleton_of_isLocallyClosed_singleton

Result:
case hx
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed {f x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ closedPoints X ⊆ f ⁻¹' closedPoints Y

Proof state:
case hx
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed (f '' {x})

Tactic:
exact (hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Result:
no goals

Proof state:
case hx
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed {f x}

Tactic:
rw [← Set.image_singleton]

Result:
case hx
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed (f '' {x})

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
⊢ closedPoints X ⊆ f ⁻¹' closedPoints Y

Tactic:
intros x hx

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ x ∈ f ⁻¹' closedPoints Y
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Basis.card_le_card_of_linearIndependent_aux {R : Type*} [Ring R] [StrongRankCondition R]
    (n : ℕ) {m : ℕ} (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n := fun h => by
  simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StrongRankCondition R
n m : ℕ
v : Fin m → Fin n → R
h : LinearIndependent R v
⊢ m ≤ n

Tactic:
simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
theorem toReal_smul (r : ℝ≥0) (s : ℝ≥0∞) : (r • s).toReal = r • s.toReal

Proof state:
r : ℝ≥0
s : ℝ≥0∞
⊢ (r • s).toReal = r • s.toReal

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]

Result:
r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * s.toReal = r • s.toReal

Proof state:
r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * s.toReal = r • s.toReal

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem disjoint_span_commMap_ker [NumberField K] :
    Disjoint (Submodule.span ℝ (Set.range (canonicalEmbedding.latticeBasis K)))
      (LinearMap.ker (commMap K))

Proof state:
case neg.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ x φ = 0

Tactic:
apply RingHom.injective (starRingEnd ℂ)

Result:
case neg.inr.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (starRingEnd ℂ) (x φ) = (starRingEnd ℂ) 0

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ x φ = 0

Tactic:
apply Complex.ext

Result:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).re = Complex.re 0

case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).im = Complex.im 0

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0

Tactic:
by_cases hφ : ComplexEmbedding.IsReal φ

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ x φ = 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ x φ = 0
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_le_right (a b : α) : min a b ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b ≤ b

Tactic:
simpa [min_def, if_pos h] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b ≤ b

Tactic:
simp [min_def, if_neg h, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b

Tactic:
if h : a ≤ b
then simpa [min_def, if_pos h] using h
else simp [min_def, if_neg h, le_refl]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[reassoc]
lemma shiftFunctorAdd'_assoc_hom_app (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
    (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
    (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃])).hom.app X ≫
      ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X)⟦a₃⟧' =
    (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃])).hom.app X ≫
      (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app (X⟦a₁⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X ≫
      (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X) =
    (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X ≫
      (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom
  (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
rw [← h₁₂, h₁₂₃]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem integrableOn_peak_smul_of_integrableOn_of_tendsto
    (hs : MeasurableSet s) (h'st : t ∈ 𝓝[s] x₀)
    (hlφ : ∀ u : Set α, IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u))
    (hiφ : Tendsto (fun i ↦ ∫ x in t, φ i x ∂μ) l (𝓝 1))
    (h'iφ : ∀ᶠ i in l, AEStronglyMeasurable (φ i) (μ.restrict s))
    (hmg : IntegrableOn g s μ) (hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)) :
    ∀ᶠ i in l, IntegrableOn (fun x => φ i x • g x) s μ

Proof state:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
simp [h] at h'i

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem lintegral_rpow_sum_enorm_sub_le_rpow_tsum
    {f : ℕ → α → E} {p : ℝ} (hp1 : 1 ≤ p) {B : ℕ → ℝ≥0∞} (n : ℕ)
    (hn : eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' i, B i) :
    (∫⁻ a, (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ≤ (∑' i, B i) ^ p

Proof state:
case h.e_a
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ∀ i ∈ Finset.range (n + 1), 0 ≤ ‖f (i + 1) a - f i a‖

Tactic:
exact fun x _ => norm_nonneg _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
⊢ ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
have hp_pos : 0 < p := zero_lt_one.trans_le hp1

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.Inv_append (h1 : State.Inv cnf1) (h2 : State.Inv cnf2) :
    State.Inv (cnf1 ++ cnf2)

Proof state:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h2 : Inv cnf2
assign1 : Nat → Bool
h1 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf1
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Tactic:
specialize h2 assign1

Result:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf1
h2 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf2
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Proof state:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
⊢ Inv (cnf1 ++ cnf2)

Tactic:
intro assign1

Result:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Proof state:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h1 : Inv cnf1
h2 : Inv cnf2
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Tactic:
specialize h1 assign1

Result:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
h2 : Inv cnf2
assign1 : Nat → Bool
h1 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf1
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Proof state:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true
h2 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
⊢ CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true ∧ CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true

Tactic:
constructor <;> assumption

Result:
no goals

Proof state:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf1
h2 : CNF.Sat (cnfSatAssignment aig✝ assign1) cnf2
⊢ CNF.Sat (cnfSatAssignment aig✝ assign1) (cnf1 ++ cnf2)

Tactic:
simp [CNF.sat_def] at h1 h2 ⊢

Result:
aig✝ : AIG Nat
cnf1 cnf2 : CNF aig✝.CNFVar
assign1 : Nat → Bool
h1 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true
h2 : CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
⊢ CNF.eval (cnfSatAssignment aig✝ assign1) cnf1 = true ∧ CNF.eval (cnfSatAssignment aig✝ assign1) cnf2 = true
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.kronecker [MulZeroClass α] {A : Matrix m m α} {B : Matrix n n α} (hA : A.IsDiag)
    (hB : B.IsDiag) : (A ⊗ₖ B).IsDiag

Proof state:
case mk.mk.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Tactic:
simp [hA hac]

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Tactic:
rcases h with hac | hbd

Result:
case mk.mk.inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

case mk.mk.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Proof state:
case mk.mk
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Tactic:
simp only [Prod.mk.inj_iff, Ne, not_and_or] at h

Result:
case mk.mk
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Proof state:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
⊢ (kroneckerMap (fun x1 x2 => x1 * x2) A B).IsDiag

Tactic:
rintro ⟨a, b⟩ ⟨c, d⟩ h

Result:
case mk.mk
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Proof state:
case mk.mk.inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x1 x2 => x1 * x2) A B (a, b) (c, d) = 0

Tactic:
simp [hB hbd]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
theorem ι_comp_sigmaObjIso_hom (f : α → D ⥤ C) (d : D) (s : α) :
    (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s => (f s).obj d) s

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasColimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (Sigma.ι f s).app d ≫ (sigmaObjIso f d).hom = Sigma.ι (fun s => (f s).obj d) s

Tactic:
simp [sigmaObjIso]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem norm_fderiv_norm_id_rpow (x : E) {p : ℝ} (hp : 1 < p) :
    ‖fderiv ℝ (fun x ↦ ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p - 2 + 1 ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ 0 ≤ ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖fderiv ℝ (fun x => ‖x‖ ^ p) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
rw [fderiv_norm_rpow x hp, norm_smul, norm_mul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)

Tactic:
rw [← Real.rpow_add_one' (by positivity) (by linarith)]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
  abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc, innerSL_apply_norm]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Data/List/ToFinsupp.lean
theorem toFinsupp_concat_eq_toFinsupp_add_single {R : Type*} [AddZeroClass R] (x : R) (xs : List R)
    [DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0] [DecidablePred fun i => getD xs i 0 ≠ 0] :
    toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single xs.length x

Proof state:
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i => xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x

Tactic:
rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
addLeftEmbedding_apply, add_zero]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0
inst✝ : DecidablePred fun i => xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x

Tactic:
classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
  addLeftEmbedding_apply, add_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem eq_singleton_left_of_prod_subset_idRel {X : Type*} {S T : Set X} (hS : S.Nonempty)
    (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ x, S = {x}

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : S ×ˢ T ⊆ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
x : X
hx : x ∈ S
⊢ x = s

Tactic:
rw [prod_subset_iff] at h_diag

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
x : X
hx : x ∈ S
⊢ x = s

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hs : (s, t) ∈ idRel
hx : (x, t) ∈ idRel
⊢ x = s

Tactic:
simp only [idRel, mem_setOf_eq] at hx hs

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hs : s = t
hx : x = t
⊢ x = s

Proof state:
X : Type u_2
S T : Set X
hS : S.Nonempty
hT : T.Nonempty
h_diag : S ×ˢ T ⊆ idRel
⊢ ∃ x, S = {x}

Tactic:
rcases hS, hT with ⟨⟨s, hs⟩, ⟨t, ht⟩⟩

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : S ×ˢ T ⊆ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
⊢ ∃ x, S = {x}

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : S ×ˢ T ⊆ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
⊢ ∃ x, S = {x}

Tactic:
refine ⟨s, eq_singleton_iff_nonempty_unique_mem.mpr ⟨⟨s, hs⟩, fun x hx ↦ ?_⟩⟩

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : S ×ˢ T ⊆ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
x : X
hx : x ∈ S
⊢ x = s

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hx : x ∈ S
hs : (s, t) ∈ idRel
⊢ x = s

Tactic:
replace hx := h_diag x hx t ht

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hs : (s, t) ∈ idRel
hx : (x, t) ∈ idRel
⊢ x = s

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s : X
hs : s ∈ S
t : X
ht : t ∈ T
x : X
hx : x ∈ S
⊢ x = s

Tactic:
replace hs := h_diag s hs t ht

Result:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hx : x ∈ S
hs : (s, t) ∈ idRel
⊢ x = s

Proof state:
case intro.intro
X : Type u_2
S T : Set X
h_diag : ∀ x ∈ S, ∀ y ∈ T, (x, y) ∈ idRel
s t : X
ht : t ∈ T
x : X
hs : s = t
hx : x = t
⊢ x = s

Tactic:
rwa [← hs] at hx

Result:
no goals