harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
/-- If `𝕜₁` is a normed field contained as subfield of a larger normed field `𝕜₂`, and if `a : A`
is an element whose `𝕜₂` spectrum restricts to `𝕜₁`, then the spectral radii over each scalar
field coincide. -/
lemma spectralRadius_eq {𝕜₁ 𝕜₂ A : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂]
    [NormedRing A] [NormedAlgebra 𝕜₁ A] [NormedAlgebra 𝕜₂ A] [NormedAlgebra 𝕜₁ 𝕜₂]
    [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂ → 𝕜₁} {a : A} (h : SpectrumRestricts a f) :
    spectralRadius 𝕜₁ a = spectralRadius 𝕜₂ a

Proof state:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ (algebraMap 𝕜₁ 𝕜₂) x ∈ spectrum 𝕜₂ a

Tactic:
exact (spectrum.algebraMap_mem_iff _).mpr hx

Result:
no goals

Proof state:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
y : 𝕜₁
hy : y ∈ spectrum 𝕜₁ a
hx : (algebraMap 𝕜₁ 𝕜₂) y ∈ spectrum 𝕜₂ a
⊢ ↑‖(algebraMap 𝕜₁ 𝕜₂) y‖₊ ≤ ⨆ k ∈ spectrum 𝕜₁ a, ↑‖k‖₊

Tactic:
exact this y ▸ le_iSup₂ (α := ℝ≥0∞) y hy

Result:
no goals

Proof state:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ ↑‖x‖₊ ≤ ⨆ k ∈ spectrum 𝕜₂ a, ↑‖k‖₊

Tactic:
refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_

Result:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst✝⁶ : NormedField 𝕜₁
inst✝⁵ : NormedField 𝕜₂
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜₁ A
inst✝² : NormedAlgebra 𝕜₂ A
inst✝¹ : NormedAlgebra 𝕜₁ 𝕜₂
inst✝ : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), ‖(algebraMap 𝕜₁ 𝕜₂) x‖₊ = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ (algebraMap 𝕜₁ 𝕜₂) x ∈ spectrum 𝕜₂ a
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Proof state:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose!

Result:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Proof state:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Tactic:
rintro (hs | rfl)

Result:
case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty

Proof state:
case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.zpow

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Proof state:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Result:
case mpr.intro
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Proof state:
case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro
α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_zpow hn

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) :
    Monic (h.unit⁻¹ • p)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ ↑h.unit⁻¹ • p.leadingCoeff = 1

Tactic:
obtain ⟨k, hk⟩ := h

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = p.leadingCoeff
⊢ ↑(IsUnit.unit ⋯)⁻¹ • p.leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).Monic

Tactic:
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ ↑h.unit⁻¹ • p.leadingCoeff = 1

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = p.leadingCoeff
⊢ k = ⋯.unit * 1

Tactic:
simp [Units.ext_iff, IsUnit.unit_spec]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = p.leadingCoeff
⊢ ↑(IsUnit.unit ⋯)⁻¹ • p.leadingCoeff = 1

Tactic:
simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]

Result:
case intro
R : Type u
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = p.leadingCoeff
⊢ k = ⋯.unit * 1
-- Mathlib/ModelTheory/Fraisse.lean
theorem exists_cg_is_age_of (hn : K.Nonempty)
    (hc : (Quotient.mk' '' K).Countable)
    (fg : ∀ M : Bundled.{w} L.Structure, M ∈ K → Structure.FG L M) (hp : Hereditary K)
    (jep : JointEmbedding K) : ∃ M : Bundled.{w} L.Structure, Structure.CG L M ∧ L.age M = K

Proof state:
case intro
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, Quotient.mk' x = ⟦a⟧) ↔ ∃ y, F y = ⟦a⟧
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
simp_rw [Quotient.eq_mk_iff_out] at hF

Result:
case intro
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
lemma sheafAdjunctionCocontinuous_counit_app_val (F : Sheaf J A) :
    ((G.sheafAdjunctionCocontinuous A J K).counit.app F).val =
      (G.op.ranAdjunction A).counit.app F.val :=
  ((G.op.ranAdjunction A).map_restrictFullyFaithful_counit_app
    (fullyFaithfulSheafToPresheaf K A) (fullyFaithfulSheafToPresheaf J A)
    (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
    (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans
      (by aesop_cat)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf J A
⊢ (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm.inv.app
        ((G.sheafPushforwardCocontinuous A J K).obj F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
          ((G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm.inv.app F) ≫
        (G.op.ranAdjunction A).counit.app ((sheafToPresheaf J A).obj F) =
    (G.op.ranAdjunction A).counit.app F.val

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem sInf_image_Icc_le (h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) :
    sInf (f '' Icc a b) ≤ f c

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
have := mem_image_of_mem f hc

Result:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
exact this.1

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
rw [h.image_Icc (hc.1.trans hc.2)] at this

Result:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_pow' : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
  Nat.recOn n (by simp) fun n ih h => by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff ^ Nat.zero ≠ 0 → (p ^ Nat.zero).leadingCoeff = p.leadingCoeff ^ Nat.zero

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]

Result:
no goals

Proof state:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h

Result:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Proof state:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0

Tactic:
rwa [pow_succ', ← ih h₁] at h

Result:
no goals

Proof state:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]

Result:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Proof state:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ n.succ = 0

Tactic:
rw [pow_succ, h₁, zero_mul]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_congr (_ : a = a') (_ : b = b') (_ : a' + b' = c) : (a + b : R) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' + b' = c
⊢ a + b = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'
-- Mathlib/Probability/StrongLaw.lean
theorem integral_truncation_le_integral_of_nonneg (hf : Integrable f μ) (h'f : 0 ≤ f) {A : ℝ} :
    ∫ x, truncation f A x ∂μ ≤ ∫ x, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
⊢ ∫ (x : α), truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ

Tactic:
apply integral_mono_of_nonneg
  (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ 0 x ≤ truncation f A x

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ f x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ 0 x ≤ truncation f A x

Tactic:
exact truncation_nonneg _ (h'f x)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
x : α
⊢ truncation f A x ≤ f x

Tactic:
calc
  truncation f A x ≤ |truncation f A x| := le_abs_self _
  _ ≤ |f x| := abs_truncation_le_abs_self _ _ _
  _ = f x := abs_of_nonneg (h'f x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z)

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), ((x ||| y) &&& z).testBit i = (x &&& z ||| y &&& z).testBit i

Tactic:
simp [Bool.and_or_distrib_right]

Result:
no goals

Proof state:
x y z : Nat
⊢ (x ||| y) &&& z = x &&& z ||| y &&& z

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), ((x ||| y) &&& z).testBit i = (x &&& z ||| y &&& z).testBit i
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_add [Add α] (M : Matrix m n α) (N : Matrix m n α) : (M + N)ᵀ = Mᵀ + Nᵀ

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
⊢ (M + N)ᵀ = Mᵀ + Nᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M + N)ᵀ i✝ j✝ = (Mᵀ + Nᵀ) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M + N)ᵀ i✝ j✝ = (Mᵀ + Nᵀ) i✝ j✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem inter_sdiff_self (s₁ s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
  eq_empty_of_forall_not_mem <| by
    simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ x ∉ s₁)

Tactic:
rintro x ⟨h, _, hn⟩

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₁
left✝ : x ∈ s₂
hn : x ∉ s₁
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ ∀ (x : α), x ∉ s₁ ∩ (s₂ \ s₁)

Tactic:
simp only [mem_inter, mem_sdiff]

Result:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ x ∉ s₁)

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₁
left✝ : x ∈ s₂
hn : x ∉ s₁
⊢ False

Tactic:
exact hn h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
private lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux [Fintype V] {v w : V}
    (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) :
    (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
h : p.toSubgraph.Adj v w'
⊢ False

Tactic:
exact hw'1 (hp.snd_of_toSubgraph_adj h)

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have : (G \  p.toSubgraph.spanningCoe).Adj w v := by
  simp only [sdiff_adj, Subgraph.spanningCoe_adj]
  exact ⟨hw'2.symm, fun h ↦ hnpvw' h.symm⟩

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
this : (G \ p.toSubgraph.spanningCoe).Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
h : p.toSubgraph.Adj w' v
⊢ False

Tactic:
exact hnpvw' h.symm

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w
hw'1 : p.snd ≠ w
hw'2 : G.Adj v w
hnpvw' : ¬p.toSubgraph.Adj v w
this : (G \ p.toSubgraph.spanningCoe).Adj w v
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
exact this.reachable

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
private lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux [Fintype V] {v w : V}
    (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) :
    (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ (Walk.cons ⋯ p).IsPath

Tactic:
rw [Walk.cons_isPath_iff]

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ p.IsPath ∧ w' ∉ p.support

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have hle : (G \ (p.cons hw'2.symm).toSubgraph.spanningCoe) ≤ (G \ p.toSubgraph.spanningCoe) := by
  apply sdiff_le_sdiff (by rfl) ?hcd
  aesop

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
private lemma IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux [Fintype V] {v w : V}
    (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) :
    (G \ p.toSubgraph.spanningCoe).Reachable w v

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
have hp'p : (p.cons hw'2.symm).IsPath := by
  rw [Walk.cons_isPath_iff]
  refine ⟨hp, fun hw' ↦ ?_⟩
  exact hw'1 (hcyc.snd_of_mem_support_of_isPath_of_adj _ hww' hw' hp hw'2)

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' => p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
hle : G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe
hp'p : (Walk.cons ⋯ p).IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n

Proof state:
case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑(pos m)).testBit n

Tactic:
rw [cast_pos]

Result:
case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑m).testBit n

Proof state:
case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m.bit0).testBit (n + 1)

Tactic:
rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]

Result:
no goals

Proof state:
case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
⊢ false = (↑one).testBit (n + 1)

Tactic:
simp [Nat.testBit_add_one]

Result:
no goals

Proof state:
case pos.zero.one

⊢ true = (↑one).testBit 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

Tactic:
rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]

Result:
no goals

Proof state:
case pos
n : ℕ
m : PosNum
⊢ m.testBit n = (↑m).testBit n

Tactic:
induction' n with n IH generalizing m <;> obtain - | m | m := m
    <;> simp only [PosNum.testBit]

Result:
case pos.zero.one

⊢ true = (↑one).testBit 0

case pos.zero.bit1
m : PosNum
⊢ true = (↑m.bit1).testBit 0

case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

case pos.succ.one
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
⊢ false = (↑one).testBit (n + 1)

case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m.bit1).testBit (n + 1)

case pos.succ.bit0
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m.bit0).testBit (n + 1)

Proof state:
case zero
n : ℕ
⊢ false = (↑zero).testBit n

Tactic:
rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]

Result:
no goals

Proof state:
case pos.succ.bit1
n : ℕ
IH : ∀ (m : PosNum), m.testBit n = (↑m).testBit n
m : PosNum
⊢ m.testBit n = (↑m.bit1).testBit (n + 1)

Tactic:
rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]

Result:
no goals

Proof state:
case pos.zero.bit0
m : PosNum
⊢ false = (↑m.bit0).testBit 0

Tactic:
rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]

Result:
no goals