harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma singularPart_compl_mutuallySingularSetSlice (κ η : Kernel α γ) [IsSFiniteKernel κ]
    [IsSFiniteKernel η] (a : α) :
    singularPart κ η a (mutuallySingularSetSlice κ η a)ᶜ = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun b =>
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b

Tactic:
exact measurable_singularPart_fun_right κ η a

Result:
no goals

Proof state:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x =>
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)

Tactic:
simp_rw [ofNNReal_toNNReal]

Result:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x =>
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
refine ae_of_all _ (fun x hx ↦ ?_)

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_le_one_or_val_inv_lt_one (v : Valuation K Γ₀) (x : K) : v x ≤ 1 ∨ v x⁻¹ < 1

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Tactic:
by_cases h : x = 0

Result:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Proof state:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Tactic:
simp only [h, _root_.map_zero, zero_le', inv_zero, zero_lt_one, or_self]

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ < 1

Tactic:
simp only [← one_lt_val_iff v h, le_or_lt]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem ofOption {f : α → Option β} (hf : Computable f) : Partrec fun a => (f a : Part β) :=
  (Nat.Partrec.ppred.comp hf).of_eq fun n => by
    rcases decode (α := α) n with - | a <;> simp
    rcases f a with - | b <;> simp

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f a)

Tactic:
rcases f a with - | b <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a => map encode (↑f a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a => map encode ((fun a => ↑(f a)) a)

Tactic:
rcases decode (α := α) n with - | a <;> simp

Result:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f a)
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_inv (r : ℝ) : ((r⁻¹ : ℝ) : ℂ) = (r : ℂ)⁻¹ :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
r : ℝ
⊢ (↑r⁻¹).re = (↑r)⁻¹.re ∧ (↑r⁻¹).im = (↑r)⁻¹.im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem sup_sigma [SemilatticeSup β] [OrderBot β] :
    (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩

Tactic:
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]

Result:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a), a ∈ s → b ∈ t a → f ⟨a, b⟩ ≤ s.sup fun i => (t i).sup fun b => f ⟨i, b⟩) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f ⟨b, b_1⟩ ≤ (s.sigma t).sup f

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a), a ∈ s → b ∈ t a → f ⟨a, b⟩ ≤ s.sup fun i => (t i).sup fun b => f ⟨i, b⟩) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f ⟨b, b_1⟩ ≤ (s.sigma t).sup f

Tactic:
exact
  ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
    le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
    {f : Option β → Option β} : Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get!

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
k : α
inst✝ : Inhabited β
f : Option β → Option β
⊢ get! (alter m k f) k = (f (get? m k)).get!

Tactic:
simp [get!_alter]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- The derivative of `x ↦ f (-x)` at `a` is the negative of the derivative of `f` at `-a`. -/
lemma deriv_comp_neg : deriv (fun x ↦ f (-x)) x = -deriv f (-x)

Proof state:
case neg
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f✝ : 𝕜 → F
x : 𝕜
f : ¬DifferentiableAt 𝕜 f✝ (-x)
⊢ deriv (fun x => f✝ (-x)) x = -deriv f✝ (-x)

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_comp_neg.not.2 f),
  deriv_zero_of_not_differentiableAt f, neg_zero]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f✝ : 𝕜 → F
x : 𝕜
f : DifferentiableAt 𝕜 f✝ (-x)
⊢ deriv (fun x => f✝ (-x)) x = -deriv f✝ (-x)

Tactic:
simpa only [deriv_neg, neg_one_smul] using deriv.scomp _ f (differentiable_neg _)

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ deriv (fun x => f (-x)) x = -deriv f (-x)

Tactic:
by_cases f : DifferentiableAt 𝕜 f (-x)

Result:
case pos
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f✝ : 𝕜 → F
x : 𝕜
f : DifferentiableAt 𝕜 f✝ (-x)
⊢ deriv (fun x => f✝ (-x)) x = -deriv f✝ (-x)

case neg
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f✝ : 𝕜 → F
x : 𝕜
f : ¬DifferentiableAt 𝕜 f✝ (-x)
⊢ deriv (fun x => f✝ (-x)) x = -deriv f✝ (-x)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_right_of_oangle_sign_eq_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = 1) : p₁ ≠ p₃ :=
  left_ne_right_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : (∡ p₁ p₂ p₃).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
/-- If `A` has small difference, then it has small doubling, with the constant squared.

This is a consequence of the Ruzsa triangle inequality. -/
@[to_additive
"If `A` has small difference, then it has small doubling, with the constant squared.

This is a consequence of the Ruzsa triangle inequality."]
lemma mulConst_le_divConst_sq : σₘ[A] ≤ δₘ[A] ^ 2

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#(A / A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
rw [← divConst_mul_card]

Result:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * ↑(#A) * (δₘ[A] * ↑(#A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
positivity

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * (↑(#A) * ↑(#A)) ≤ δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
calc
  _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
  _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
  _ = _ := by rw [← divConst_mul_card]; ring

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)

Result:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * (↑(#A) * ↑(#A)) ≤ δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#A) ≤ ↑(#(A / A)) * ↑(#(A / A))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A * A) * #A ≤ #(A / A) * #(A / A)

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
⊢ σₘ[∅] ≤ δₘ[∅] ^ 2

case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] ≤ δₘ[A] ^ 2

Proof state:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
⊢ σₘ[∅] ≤ δₘ[∅] ^ 2

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A * A)) * ↑(#A)

Tactic:
rw [← mul_assoc, mulConst_mul_card]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * ↑(#A) * (δₘ[A] * ↑(#A)) = δₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A * A) * #A ≤ #(A / A) * #(A / A)

Tactic:
exact ruzsa_triangle_inequality_mul_div_div ..

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem injective_ofQuotientStabilizer : Function.Injective (ofQuotientStabilizer α x) :=
  fun y₁ y₂ =>
  Quotient.inductionOn₂' y₁ y₂ fun g₁ g₂ (H : g₁ • x = g₂ • x) =>
    Quotient.sound' <| by
      rw [leftRel_apply]
      show (g₁⁻¹ * g₂) • x = x
      rw [mul_smul, ← H, inv_smul_smul]

Proof state:
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x

Tactic:
show (g₁⁻¹ * g₂) • x = x

Result:
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x

Proof state:
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x

Tactic:
rw [mul_smul, ← H, inv_smul_smul]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (leftRel (stabilizer α x)) g₁ g₂

Tactic:
rw [leftRel_apply]

Result:
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_spanningCoe_eq :
    G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.spanningCoe.deleteEdges s).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).spanningCoe.Adj x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.spanningCoe.deleteEdges s).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).spanningCoe.Adj x✝¹ x✝
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma rotate_distinguished_triangle' (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT : T ∈ distinguishedTriangles C) : T.rotate ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles C
⊢ T.rotate ∈ distinguishedTriangles C

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT

Result:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ T.rotate ∈ distinguishedTriangles C

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ T.rotate ∈ distinguishedTriangles C

Tactic:
exact ⟨_, _, _, ⟨(rotate _).mapIso e ≪≫ CochainComplex.mappingCone.rotateTrianglehIso φ⟩⟩

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc'_one (n : σ →₀ ℕ) : trunc' R n 1 = 1 :=
  MvPolynomial.ext _ _ fun m ↦ by
    classical
    rw [coeff_trunc', coeff_one]
    split_ifs with H H'
    · subst m; simp only [MvPolynomial.coeff_zero_one]
    · rw [MvPolynomial.coeff_one, if_neg (Ne.symm H')]
    · rw [MvPolynomial.coeff_one, if_neg ?_]
      rintro rfl
      exact H (zero_le n)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False

Tactic:
exact H (zero_le n)

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) 1) = MvPolynomial.coeff m 1

Tactic:
rw [coeff_trunc', coeff_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m

Tactic:
rintro rfl

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1

Tactic:
split_ifs with H H'

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : m ≤ n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : m ≤ n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

Tactic:
subst m

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1

Tactic:
rw [MvPolynomial.coeff_one, if_neg ?_]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1

Tactic:
simp only [MvPolynomial.coeff_zero_one]

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

Tactic:
rw [MvPolynomial.coeff_one, if_neg (Ne.symm H')]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
    (∀ v : BitVec (n + 1), P v) ↔ (∀ (x : Bool) (v : BitVec n), P (v.cons x))

Proof state:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
⊢ P v

Tactic:
have w : v = (v.setWidth n).cons v.msb := by simp

Result:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
w : v = cons v.msb (setWidth n v)
⊢ P v

Proof state:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
⊢ (∀ (x : Bool) (v : BitVec n), P (cons x v)) → ∀ (v : BitVec (n + 1)), P v

Tactic:
intro h v

Result:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
⊢ P v

Proof state:
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
⊢ v = cons v.msb (setWidth n v)

Tactic:
simp

Result:
no goals

Proof state:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
w : v = cons v.msb (setWidth n v)
⊢ P v

Tactic:
rw [w]

Result:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
w : v = cons v.msb (setWidth n v)
⊢ P (cons v.msb (setWidth n v))

Proof state:
case mp
n : Nat
P : BitVec (n + 1) → Prop
⊢ (∀ (v : BitVec (n + 1)), P v) → ∀ (x : Bool) (v : BitVec n), P (cons x v)

Tactic:
intro h _ _

Result:
case mp
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (v : BitVec (n + 1)), P v
x✝ : Bool
v✝ : BitVec n
⊢ P (cons x✝ v✝)

Proof state:
n : Nat
P : BitVec (n + 1) → Prop
⊢ (∀ (v : BitVec (n + 1)), P v) ↔ ∀ (x : Bool) (v : BitVec n), P (cons x v)

Tactic:
constructor

Result:
case mp
n : Nat
P : BitVec (n + 1) → Prop
⊢ (∀ (v : BitVec (n + 1)), P v) → ∀ (x : Bool) (v : BitVec n), P (cons x v)

case mpr
n : Nat
P : BitVec (n + 1) → Prop
⊢ (∀ (x : Bool) (v : BitVec n), P (cons x v)) → ∀ (v : BitVec (n + 1)), P v

Proof state:
case mpr
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (x : Bool) (v : BitVec n), P (cons x v)
v : BitVec (n + 1)
w : v = cons v.msb (setWidth n v)
⊢ P (cons v.msb (setWidth n v))

Tactic:
apply h

Result:
no goals

Proof state:
case mp
n : Nat
P : BitVec (n + 1) → Prop
h : ∀ (v : BitVec (n + 1)), P v
x✝ : Bool
v✝ : BitVec n
⊢ P (cons x✝ v✝)

Tactic:
apply h

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsOpen.isGδ {s : Set X} (h : IsOpen s) : IsGδ s :=
  ⟨{s}, by simp [h], countable_singleton _, (Set.sInter_singleton _).symm⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsOpen s
⊢ ∀ t ∈ {s}, IsOpen t

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem isMaximal_inf_right_of_isMaximal_sup {x y : X} (hxz : IsMaximal x (x ⊔ y))
    (hyz : IsMaximal y (x ⊔ y)) : IsMaximal (x ⊓ y) y

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y

Tactic:
rw [inf_comm]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (y ⊔ x)
hyz : IsMaximal y (y ⊔ x)
⊢ IsMaximal (y ⊓ x) y

Tactic:
exact isMaximal_inf_left_of_isMaximal_sup hyz hxz

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y

Tactic:
rw [sup_comm] at hxz hyz

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (y ⊔ x)
hyz : IsMaximal y (y ⊔ x)
⊢ IsMaximal (y ⊓ x) y
-- Mathlib/Topology/Category/Compactum.lean
theorem subset_cl {X : Compactum} (A : Set X) : A ⊆ cl A := fun a ha =>
  ⟨X.incl a, ha, by simp⟩

Proof state:
X : Compactum
A : Set X.A
a : X.A
ha : a ∈ A
⊢ X.str (X.incl a) = a

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpBFamily_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c}
    (hc : IsRegular c) (ho : Cardinal.lift.{v, u} o.card < c) (hc' : c ≠ ℵ₀)
    (hf : ∀ (i hi), ∀ b < c.ord, f i hi b < c.ord) {a} :
    a < c.ord → nfpBFamily.{u, v} o f a < c.ord :=
  nfpFamily_lt_ord_lift_of_isRegular hc (by rwa [mk_toType]) hc' fun _ => hf _ _

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord
a : Ordinal.{max u v}
⊢ lift.{?u.134523, u} #o.toType < c

Tactic:
rwa [mk_toType]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n

Proof state:
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

Tactic:
rw [log_zero_right, log_zero_right]

Result:
no goals

Proof state:
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n

Tactic:
apply le_log_of_pow_le hc

Result:
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n

Proof state:
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n

Tactic:
calc
  c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
  _ ≤ n := pow_log_le_self _ hn

Result:
no goals

Proof state:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n