harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} :
    (empty c : Raw₀ α β).getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
a : α
fallback : β a
c : Nat
⊢ (empty c).getD a fallback = fallback

Tactic:
simp [getD, empty]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
@[simp]
lemma mapDomainAlgHom_id (k A) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] :
    mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k (AddMonoidAlgebra A G)

Proof state:
case H.H
G : Type u₂
k : Type u_3
A : Type u_4
inst✝³ : CommSemiring k
inst✝² : Semiring A
inst✝¹ : Algebra k A
inst✝ : AddMonoid G
x✝¹ : A[G]
x✝ : G
⊢ ((mapDomainAlgHom k A (AddMonoidHom.id G)) x✝¹) x✝ = ((AlgHom.id k A[G]) x✝¹) x✝

Tactic:
simp [AddMonoidHom.id, ← Function.id_def]

Result:
no goals

Proof state:
G : Type u₂
k : Type u_3
A : Type u_4
inst✝³ : CommSemiring k
inst✝² : Semiring A
inst✝¹ : Algebra k A
inst✝ : AddMonoid G
⊢ mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k A[G]

Tactic:
ext

Result:
case H.H
G : Type u₂
k : Type u_3
A : Type u_4
inst✝³ : CommSemiring k
inst✝² : Semiring A
inst✝¹ : Algebra k A
inst✝ : AddMonoid G
x✝¹ : A[G]
x✝ : G
⊢ ((mapDomainAlgHom k A (AddMonoidHom.id G)) x✝¹) x✝ = ((AlgHom.id k A[G]) x✝¹) x✝
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem mapAlg_eq_map (p : R[X]) : mapAlg R S p = map (algebraMap R S) p

Proof state:
case a
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n✝ : ℕ
⊢ (p.sum fun e a => C ((algebraMap R S) a) * X ^ e).coeff n✝ =
    (p.sum fun e a => (⇑C ∘ ⇑(algebraMap R S)) a * X ^ e).coeff n✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (mapAlg R S) p = map (algebraMap R S) p

Tactic:
simp only [mapAlg, aeval_def, eval₂_eq_sum, map, algebraMap_apply, RingHom.coe_comp]

Result:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (p.sum fun e a => C ((algebraMap R S) a) * X ^ e) = p.sum fun e a => (⇑C ∘ ⇑(algebraMap R S)) a * X ^ e

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (p.sum fun e a => C ((algebraMap R S) a) * X ^ e) = p.sum fun e a => (⇑C ∘ ⇑(algebraMap R S)) a * X ^ e

Tactic:
ext

Result:
case a
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n✝ : ℕ
⊢ (p.sum fun e a => C ((algebraMap R S) a) * X ^ e).coeff n✝ =
    (p.sum fun e a => (⇑C ∘ ⇑(algebraMap R S)) a * X ^ e).coeff n✝
-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- If a property of maps of topological spaces is stable under composition, the induced
morphism property of schemes is stable under composition. -/
lemma topologically_isStableUnderComposition
    (hP : ∀ {α β γ : Type u} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]
      (f : α → β) (g : β → γ) (_ : P f) (_ : P g), P (g ∘ f)) :
    (topologically P).IsStableUnderComposition where
  comp_mem {X Y Z} f g hf hg

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) g
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ≫ g)

Tactic:
simp only [topologically, Scheme.comp_coeBase, TopCat.coe_comp]

Result:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) g
⊢ P (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) g
⊢ P (⇑(ConcreteCategory.hom g.base) ∘ ⇑(ConcreteCategory.hom f.base))

Tactic:
exact hP _ _ hf hg

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
/-- This is a version of `IncidenceAlgebra.prod_mul_prod` that works over non-commutative rings. -/
lemma prod_mul_prod' [LocallyFiniteOrder α] [LocallyFiniteOrder β]
    [DecidableRel (α := α × β) (· ≤ ·)]
    (h : ∀ a₁ a₂ a₃ b₁ b₂ b₃,
        f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)) :
    f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Proof state:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
⊢ f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)

Tactic:
ext x y

Result:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁵ : Ring 𝕜
inst✝⁴ : Preorder α
inst✝³ : Preorder β
f₁ f₂ : IncidenceAlgebra 𝕜 α
g₁ g₂ : IncidenceAlgebra 𝕜 β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
h :
  ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)
x y : α × β
a✝ : x ≤ y
⊢ (f₁.prod g₁ * f₂.prod g₂) x y = ((f₁ * f₂).prod (g₁ * g₂)) x y

Tactic:
simp [Icc_prod_def, sum_mul_sum, h, sum_product]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem Reachable.elim_path {p : Prop} {u v : V} (h : G.Reachable u v)
    (hp : G.Path u v → p) : p

Proof state:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : G.Path u v → p
⊢ p

Tactic:
classical exact h.elim fun q => hp q.toPath

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
p : Prop
u v : V
h : G.Reachable u v
hp : G.Path u v → p
⊢ p

Tactic:
exact h.elim fun q => hp q.toPath

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_len_le_digits_len_succ (b n : ℕ) :
    (digits b n).length ≤ (digits b (n + 1)).length

Proof state:
case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
simpa [digits_len, hb, hn] using log_mono_right (le_succ _)

Result:
no goals

Proof state:
case inl
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (0 + 1)).length

Tactic:
simp

Result:
no goals

Proof state:
b n : ℕ
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

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

Result:
case inl
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (0 + 1)).length

case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Proof state:
case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
interval_cases b <;> simp_arith [digits_zero_succ', hn]

Result:
no goals

Proof state:
case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_le_pi_div_two {x} : arccos x ≤ π / 2 ↔ 0 ≤ x

Proof state:
x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma mabs_div_comm (a b : α) : |a / b|ₘ = |b / a|ₘ

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ mabs (a / b) = mabs (b / a)

Tactic:
rw [← mabs_inv, inv_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem ofAIG.Inv1 (aig : AIG α) : ∃ n, Inv1 n (ofAIG aig)

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)

Tactic:
dsimp only [ofAIG]

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map

Tactic:
exact (ofAIGAux aig).inv1

Result:
no goals

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∃ n, State.Inv1 n (ofAIG aig)

Tactic:
exists (ofAIGAux aig).max

Result:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)
-- Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
/-- The filter `CStarAlgebra.approximateUnit` generated by the sections
`{x | a ≤ x} ∩ closedBall 0 1` for `0 ≤ a` forms an increasing approximate unit. -/
lemma increasingApproximateUnit :
    IsIncreasingApproximateUnit (approximateUnit A) where
  tendsto_mul_left

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ (m : A), Tendsto (fun x => x * m) (approximateUnit A) (𝓝 m)

Tactic:
exact tendsto_mul_right_approximateUnit

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x

Tactic:
rw [(hasBasis_approximateUnit A).eventually_iff]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∃ i, (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, x ∈ {x | i ≤ x} ∩ closedBall 0 1 → IsSelfAdjoint x

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ (0 ≤ 0 ∧ ‖0‖ < 1) ∧ ∀ ⦃x : A⦄, x ∈ {x | 0 ≤ x} → 0 ≤ x

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
i✝ : A
hx : 0 ≤ i✝ ∧ ‖i✝‖ < 1
⊢ i✝ ∈ closedBall 0 1

Tactic:
simpa using hx.2.le

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in 𝓟 (closedBall 0 1), ‖x‖ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ (m : A), Tendsto (fun x => m * x) (approximateUnit A) (𝓝 m)

Tactic:
rw [tendsto_mul_left_iff_tendsto_mul_right]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ (m : A), Tendsto (fun x => x * m) (approximateUnit A) (𝓝 m)

A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ᶠ (x : A) in approximateUnit A, IsSelfAdjoint x

Proof state:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : 0 ≤ x ∧ ‖x‖ < 1
⊢ (0 ≤ x ∧ ‖x‖ < 1) ∧ ∀ ⦃x_1 : A⦄, x_1 ∈ {x_2 | x ≤ x_2} ∩ closedBall 0 1 → IsSelfAdjoint x_1

Tactic:
exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩

Result:
no goals

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∃ i, (0 ≤ i ∧ ‖i‖ < 1) ∧ ∀ ⦃x : A⦄, x ∈ {x | i ≤ x} ∩ closedBall 0 1 → IsSelfAdjoint x

Tactic:
peel (hasBasis_approximateUnit A).ex_mem with x hx

Result:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : 0 ≤ x ∧ ‖x‖ < 1
⊢ (0 ≤ x ∧ ‖x‖ < 1) ∧ ∀ ⦃x_1 : A⦄, x_1 ∈ {x_2 | x ≤ x_2} ∩ closedBall 0 1 → IsSelfAdjoint x_1
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitePos_mul_of_infinitePos_not_infinitesimal_pos {x y : ℝ*} :
    InfinitePos x → ¬Infinitesimal y → 0 < y → InfinitePos (x * y) := fun hx hy₁ hy₂ r => by
  have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
  let ⟨r₁, hy₁''⟩ := hy₁'
  have hyr : 0 < r₁ ∧ ↑r₁ ≤ y

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y

Tactic:
rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''

Result:
no goals

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ ↑r < x * y

Tactic:
have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by
  rwa [Classical.not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁''

Result:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑r < x * y

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
⊢ ↑r < x * y

Tactic:
have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)

Result:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
⊢ ↑r < x * y

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
⊢ ↑r < x * y

Tactic:
let ⟨r₁, hy₁''⟩ := hy₁'

Result:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ ↑r < x * y

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y

Tactic:
exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))

Result:
no goals

Proof state:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑r < x * y

Tactic:
rw [← div_mul_cancel₀ r (ne_of_gt hyr.1), coe_mul]

Result:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem bot_strongly_regular : (⊥ : SimpleGraph V).IsSRGWith (Fintype.card V) 0 ℓ 0 where
  card := rfl
  regular := bot_degree
  of_adj := fun _ _ h => h.elim
  of_not_adj := fun v w _h => by
    simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
    ext
    simp [mem_commonNeighbors]

Proof state:
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
_h : v ≠ w
⊢ (fun v w => ¬⊥.Adj v w → Fintype.card ↑(⊥.commonNeighbors v w) = 0) v w

Tactic:
simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]

Result:
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
_h : v ≠ w
⊢ filter (Membership.mem (⊥.commonNeighbors v w)) univ = ∅

Proof state:
case h
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (Membership.mem (⊥.commonNeighbors v w)) univ ↔ a✝ ∈ ∅

Tactic:
simp [mem_commonNeighbors]

Result:
no goals

Proof state:
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
_h : v ≠ w
⊢ filter (Membership.mem (⊥.commonNeighbors v w)) univ = ∅

Tactic:
ext

Result:
case h
V : Type u
inst✝ : Fintype V
ℓ : ℕ
v w : V
_h : v ≠ w
a✝ : V
⊢ a✝ ∈ filter (Membership.mem (⊥.commonNeighbors v w)) univ ↔ a✝ ∈ ∅
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_lt' (hy : 0 < y) : √x < y ↔ x < y ^ 2

Proof state:
x y : ℝ
hy : 0 < y
⊢ √x < y ↔ x < y ^ 2

Tactic:
rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem Disjoint.dedup_append {xs ys : List α} (h : Disjoint xs ys) :
    dedup (xs ++ ys) = dedup xs ++ dedup ys

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False

Tactic:
exact h hx (mem_dedup.mp hy)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.Disjoint ys.dedup

Tactic:
intro a hx hy

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup

Tactic:
rw [List.dedup_append, Disjoint.union_eq]

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.Disjoint ys.dedup
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.div_right (hs : IsOpen s) : IsOpen (s / t)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen s
⊢ IsOpen (⋃ a ∈ t, (fun x => x / a) '' s)

Tactic:
exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen s
⊢ IsOpen (s / t)

Tactic:
rw [← iUnion_div_right_image]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen s
⊢ IsOpen (⋃ a ∈ t, (fun x => x / a) '' s)
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_unique {j : N →* P} (hj : ∀ x, j (f.toMap x) = g x) : f.lift hg = j

Proof state:
case h.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ f.toMap (f.sec x✝).1 = f.toMap ↑(f.sec x✝).2 * x✝

Tactic:
rw [← sec_spec']

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ j (f.toMap (f.sec x✝).1) = j (f.toMap ↑(f.sec x✝).2 * x✝)

Tactic:
apply congr_arg

Result:
case h.h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ f.toMap (f.sec x✝).1 = f.toMap ↑(f.sec x✝).2 * x✝

Proof state:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ (f.lift hg) x✝ = j x✝

Tactic:
rw [lift_spec, ← hj, ← hj, ← j.map_mul]

Result:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ j (f.toMap (f.sec x✝).1) = j (f.toMap ↑(f.sec x✝).2 * x✝)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
⊢ f.lift hg = j

Tactic:
ext

Result:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f.toMap x) = g x
x✝ : N
⊢ (f.lift hg) x✝ = j x✝
-- Mathlib/Algebra/Lie/Sl2.lean
lemma f_ne_zero (t : IsSl2Triple h e f) : f ≠ 0

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ f ≠ 0

Tactic:
contrapose! this

Result:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : f = 0
⊢ h = 0

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : f = 0
⊢ h = 0

Tactic:
simpa [this] using t.lie_e_f.symm

Result:
no goals

Proof state:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ f ≠ 0

Tactic:
have := t.h_ne_zero

Result:
L : Type u_2
inst✝ : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
⊢ f ≠ 0
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma deriv_smoothingFn {x : ℝ} (hx : 1 < x) : deriv ε x = -x⁻¹ / (log x ^ 2)

Proof state:
x : ℝ
hx : 1 < x
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)

Result:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Proof state:
x : ℝ
hx : 1 < x
⊢ 0 < x

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
show deriv (fun z => 1 / log z) x = -x⁻¹ / (log x ^ 2)

Result:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ deriv (fun z => 1 / log z) x = -x⁻¹ / log x ^ 2

Proof state:
x : ℝ
hx : 1 < x
this : log x ≠ 0
⊢ deriv (fun z => 1 / log z) x = -x⁻¹ / log x ^ 2

Tactic:
rw [deriv_div] <;> aesop

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_finset_singleton (b : α) : stabilizer G ({b} : Finset α) = stabilizer G b

Proof state:
case h
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
⊢ stabilizer G {b} = stabilizer G b

Tactic:
ext

Result:
case h
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem le_of_opNorm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=
  (f.le_opNorm x).trans (by gcongr)

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
h : ‖f‖ ≤ c
x : V₁
⊢ ‖f‖ * ‖x‖ ≤ c * ‖x‖

Tactic:
gcongr

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_midpoint_rev_left (p₁ p₂ p₃ : P) : ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃

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
⊢ ∡ (midpoint ℝ p₂ p₁) p₂ p₃ = ∡ p₁ p₂ p₃

Tactic:
rw [midpoint_comm, oangle_midpoint_left]

Result:
no goals