harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_toReal_eq_two_mul_add_two_pi {θ : Angle} :
    ((2 : ℤ) • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Proof state:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]

Result:
no goals
-- Mathlib/Probability/Kernel/SetIntegral.lean
lemma integral_integral_indicator (μ : Measure X) (f : X → Y → E) {s : Set X}
    (hs : MeasurableSet s) :
    ∫ x, ∫ y, s.indicator (f · y) x ∂κ x ∂μ = ∫ x in s, ∫ y, f x y ∂κ x ∂μ

Proof state:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x => f x y) x ∂κ x ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂κ x ∂μ

Tactic:
simp_rw [← integral_indicator hs, Kernel.integral_indicator₂]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_natCast_cpow_le_norm_natCast_cpow_iff {n : ℕ} (hn : 1 < n) {w z : ℂ} :
    ‖(n : ℂ) ^ w‖ ≤ ‖(n : ℂ) ^ z‖ ↔ w.re ≤ z.re

Proof state:
n : ℕ
hn : 1 < n
w z : ℂ
⊢ ‖↑n ^ w‖ ≤ ‖↑n ^ z‖ ↔ w.re ≤ z.re

Tactic:
simp_rw [norm_natCast_cpow_of_pos (Nat.zero_lt_of_lt hn),
  Real.rpow_le_rpow_left_iff (Nat.one_lt_cast.mpr hn)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_map (x y : V') (f : V ≃ₗᵢ[ℝ] V') :
    (Orientation.map (Fin 2) f.toLinearEquiv o).oangle x y = o.oangle (f.symm x) (f.symm y)

Proof state:
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V'
f : V ≃ₗᵢ[ℝ] V'
⊢ ((map (Fin 2) f.toLinearEquiv) o).oangle x y = o.oangle (f.symm x) (f.symm y)

Tactic:
simp [oangle, o.kahler_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_eq_decide (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
    (p && q) = decide (p ∧ q)

Proof state:
p q : Prop
dpq : Decidable (p ∧ q)
dp : Decidable p
dq : Decidable q
⊢ (decide p && decide q) = decide (p ∧ q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ∧ q)
dq : Decidable q
p : p✝
⊢ (decide p✝ && decide q) = decide (p✝ ∧ q)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem continuousAt_iff_lower_upperSemicontinuousAt {f : α → γ} :
    ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x

Tactic:
simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ←
  upperSemicontinuousWithinAt_univ_iff, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
    forIn o.toList b f = forIn o b f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
o : Option α
b : β
f : α → β → m (ForInStep β)
⊢ forIn o.toList b f = forIn o b f

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Basic.lean
theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (modn i m).val < m
  | _, ⟨_, _⟩, hp =>  by simp [modn]; apply Nat.mod_lt; assumption

Proof state:
n x✝ val✝ : Nat
isLt✝ : val✝ < n
hp : x✝ > 0
⊢ ↑(⟨val✝, isLt✝⟩.modn x✝) < x✝

Tactic:
simp [modn]

Result:
n x✝ val✝ : Nat
isLt✝ : val✝ < n
hp : x✝ > 0
⊢ val✝ % x✝ < x✝

Proof state:
n x✝ val✝ : Nat
isLt✝ : val✝ < n
hp : x✝ > 0
⊢ val✝ % x✝ < x✝

Tactic:
apply Nat.mod_lt

Result:
case a
n x✝ val✝ : Nat
isLt✝ : val✝ < n
hp : x✝ > 0
⊢ x✝ > 0

Proof state:
case a
n x✝ val✝ : Nat
isLt✝ : val✝ < n
hp : x✝ > 0
⊢ x✝ > 0

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem flatMap_nil (f : α → List β) : List.flatMap f [] = []

Proof state:
α : Type u
β : Type v
f : α → List β
⊢ flatMap f nil = nil

Tactic:
simp [flatten, List.flatMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem eq_of_isEqv [DecidableEq α] (a b : Vector α n) (h : Vector.isEqv a b (fun x y => x = y)) : a = b

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
a : Array α
b : Vector α a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv b fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ } = b

Tactic:
rcases b with ⟨b, h⟩

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ } = { toArray := b, size_toArray := h✝ }

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ }.toArray = { toArray := b, size_toArray := h✝ }.toArray

Tactic:
apply Array.eq_of_isEqv

Result:
case mk.mk.h
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ }.toArray fun x y => decide (x = y)) =
    true

Proof state:
case mk.mk.h
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ }.toArray fun x y => decide (x = y)) =
    true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : DecidableEq α
a b : Vector α n
h : (a.isEqv b fun x y => decide (x = y)) = true
⊢ a = b

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
a : Array α
b : Vector α a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv b fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ } = b

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ } = { toArray := b, size_toArray := h✝ }

Tactic:
rw [← Vector.toArray_inj]

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
a b : Array α
h✝ : b.size = a.size
h : ({ toArray := a, size_toArray := ⋯ }.isEqv { toArray := b, size_toArray := h✝ } fun x y => decide (x = y)) = true
⊢ { toArray := a, size_toArray := ⋯ }.toArray = { toArray := b, size_toArray := h✝ }.toArray
-- Mathlib/Analysis/RCLike/Inner.lean
lemma abs_wInner_le (hw : 0 ≤ w) : |⟪f, g⟫_[ℝ, w]| ≤ ⟪|f|, |g|⟫_[ℝ, w]

Proof state:
ι : Type u_1
inst✝ : Fintype ι
w f g : ι → ℝ
hw : 0 ≤ w
⊢ |wInner w f g| ≤ wInner w |f| |g|

Tactic:
simpa using norm_wInner_le (𝕜 := ℝ) hw

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_add_int : ∀ n : ℤ, Function.Commute f (· + n)
  | (n : ℕ) => f.commute_add_nat n
  | -[n+1] => by simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x => x + ↑-[n+1]

Tactic:
simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nhds_top_iff_nat {m : α → ℝ≥0∞} {f : Filter α} :
    Tendsto m f (𝓝 ∞) ↔ ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a :=
  tendsto_nhds_top_iff_nnreal.trans
    ⟨fun h n => by simpa only [ENNReal.coe_natCast] using h n, fun h x =>
      let ⟨n, hn⟩ := exists_nat_gt x
      (h n).mono fun _ => lt_trans <| by rwa [← ENNReal.coe_natCast, coe_lt_coe]⟩

Proof state:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a
n : ℕ
⊢ ∀ᶠ (a : α) in f, ↑n < m a

Tactic:
simpa only [ENNReal.coe_natCast] using h n

Result:
no goals

Proof state:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a
x : ℝ≥0
n : ℕ
hn : x < ↑n
x✝ : α
⊢ ↑x < ↑n

Tactic:
rwa [← ENNReal.coe_natCast, coe_lt_coe]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem deleteEdges_eq_inter_edgeSet (s : Set (Sym2 V)) :
    G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G.deleteEdges s).Adj x✝¹ x✝ ↔ (G.deleteEdges (s ∩ G.edgeSet)).Adj x✝¹ x✝

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

Tactic:
simp +contextual [imp_false]

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquivOfAlgEquiv_symm : (algEquivOfAlgEquiv S Q h H).symm =
    algEquivOfAlgEquiv Q S h.symm (show Submonoid.map h.symm T = M by
      erw [← H, ← Submonoid.comap_equiv_eq_map_symm,
        Submonoid.comap_map_eq_of_injective h.injective]) := rfl

Proof state:
R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ Submonoid.map h.symm T = M

Tactic:
erw [← H, ← Submonoid.comap_equiv_eq_map_symm,
  Submonoid.comap_map_eq_of_injective h.injective]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift_top (g : Set α → Filter β) : (⊤ : Filter α).lift g = g univ

Proof state:
α : Type u_1
β : Type u_2
g : Set α → Filter β
⊢ ⊤.lift g = g univ

Tactic:
simp [Filter.lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_reverse {l : Array α} {f : Nat → α → β} :
    l.reverse.mapIdx f = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
⊢ mapIdx f { toList := l }.reverse = (mapIdx (fun i => f ({ toList := l }.size - 1 - i)) { toList := l }).reverse

Tactic:
simp [List.mapIdx_reverse]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
⊢ mapIdx f l.reverse = (mapIdx (fun i => f (l.size - 1 - i)) l).reverse

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : List α
⊢ mapIdx f { toList := l }.reverse = (mapIdx (fun i => f ({ toList := l }.size - 1 - i)) { toList := l }).reverse
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃)

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker f ≤ comap f (ker g)

Tactic:
exact comap_mono bot_le

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker f ≤ ker (g.comp f)

Tactic:
rw [ker_comp]

Result:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ ker f ≤ comap f (ker g)
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_eq_top_iff (x : M) : (R ∙ x) = ⊤ ↔ ∀ v, ∃ r : R, r • x = v

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ span R {x} = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
rw [eq_top_iff, le_span_singleton_iff]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (∀ v ∈ ⊤, ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (∀ v ∈ ⊤, ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_insert_inr : (insert (inr b) u).toRight = insert b u.toRight

Proof state:
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toRight = insert b u.toRight

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_neg_natCast_nonneg (n : ℕ) : 0 ≤ log (-n)

Proof state:
n : ℕ
⊢ 0 ≤ log (-↑n)

Tactic:
rw [← log_neg_eq_log, neg_neg]

Result:
n : ℕ
⊢ 0 ≤ log ↑n

Proof state:
n : ℕ
⊢ 0 ≤ log ↑n

Tactic:
exact log_natCast_nonneg _

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
theorem exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] :
    ∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Line α ι, l.IsMono C :=
  let ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension'.{u,v} α (ULift.{u,v} κ)
  ⟨ι, ιfin, fun C =>
    let ⟨l, c, hc⟩ := hι (ULift.up ∘ C)
    ⟨l, c.down, fun x => by rw [← hc x, Function.comp_apply]⟩⟩

Proof state:
α : Type u
inst✝¹ : Finite α
κ : Type v
inst✝ : Finite κ
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → ULift.{u, v} κ), ∃ l, IsMono C l
C : (ι → α) → κ
l : Line α ι
c : ULift.{u, v} κ
hc : ∀ (x : α), (ULift.up ∘ C) (↑l x) = c
x : α
⊢ C (↑l x) = c.down

Tactic:
rw [← hc x, Function.comp_apply]

Result:
no goals
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem exp_one_lt_d9 : exp 1 < 2.7182818286 :=
  lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) (by norm_num)

Proof state:
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 2.7182818286

Tactic:
norm_num

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Filter.HasBasis.lift'_interior_eq_self {l : Filter X} {p : ι → Prop} {s : ι → Set X}
    (h : l.HasBasis p s) (ho : ∀ i, p i → IsOpen (s i)) : l.lift' interior = l :=
  le_antisymm l.lift'_interior_le <| h.lift'_interior.ge_iff.2 fun i hi ↦ by
    simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi

Proof state:
X : Type u
ι : Sort w
inst✝ : TopologicalSpace X
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
ho : ∀ (i : ι), p i → IsOpen (s i)
i : ι
hi : p i
⊢ interior (s i) ∈ l

Tactic:
simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem insert_inter_of_mem {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₂) :
    insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
  ext fun x => by
    have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
    simp only [mem_inter, mem_insert, or_and_left, this]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
simp only [mem_inter, mem_insert, or_and_left, this]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h

Result:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x = a → x ∈ s₂

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂

Tactic:
exact h

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem model_singleton_iff {φ : L.Sentence} : M ⊨ ({φ} : L.Theory) ↔ M ⊨ φ

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ M ⊨ {φ} ↔ M ⊨ φ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Set β) = 0 :=
  s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s • 0

Tactic:
simpa [mem_smul] using hs

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_mul {p q : ℝ} (hp : 0 ≤ p) :
    Real.toNNReal (p * q) = Real.toNNReal p * Real.toNNReal q :=
  NNReal.eq <| by simp [mul_max_of_nonneg, hp]

Proof state:
p q : ℝ
hp : 0 ≤ p
⊢ ↑(p * q).toNNReal = ↑(p.toNNReal * q.toNNReal)

Tactic:
simp [mul_max_of_nonneg, hp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem singleton_inj : #v[a] = #v[b] ↔ a = b

Proof state:
α✝ : Type u_1
a b : α✝
⊢ { toArray := #[a], size_toArray := ⋯ } = { toArray := #[b], size_toArray := ⋯ } ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_map_right (m : α → γ → δ) (n : β → γ) :
    map₂ m f (g.map n) = map₂ (fun a b => m a (n b)) f g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun a b => m a (n b)) f g

Tactic:
rw [map₂_swap, map₂_map_left, map₂_swap]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma lowerBounds_infClosure (s : Set α) : lowerBounds (infClosure s) = lowerBounds s :=
  (lowerBounds_mono_set subset_infClosure).antisymm <| by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact le_inf' _ _ fun b hb ↦ ha <| hts hb

Proof state:
case intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
ha : a ∈ lowerBounds s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
⊢ a ≤ t.inf' ht id

Tactic:
exact le_inf' _ _ fun b hb ↦ ha <| hts hb

Result:
no goals

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
⊢ lowerBounds s ⊆ lowerBounds (infClosure s)

Tactic:
rintro a ha _ ⟨t, ht, hts, rfl⟩

Result:
case intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
ha : a ∈ lowerBounds s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
⊢ a ≤ t.inf' ht id
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The sets of `N`-smooth and of `(N+1)`-smooth numbers are the same when `N` is not prime.
See `Nat.equivProdNatSmoothNumbers` for when `N` is prime. -/
lemma smoothNumbers_succ {N : ℕ} (hN : ¬ N.Prime) : N.succ.smoothNumbers = N.smoothNumbers

Proof state:
N : ℕ
hN : ¬Prime N
⊢ N.succ.smoothNumbers = N.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, Finset.range_succ, factoredNumbers_insert _ hN]

Result:
no goals
-- Mathlib/RingTheory/Etale/Basic.lean
theorem localization_map [FormallyEtale R S] : FormallyEtale Rₘ Sₘ

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this✝ : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
exact FormallyEtale.localization_base M

Result:
no goals

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this : FormallyEtale S Sₘ
⊢ FormallyEtale Rₘ Sₘ

Tactic:
haveI : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ

Result:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this✝ : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
⊢ FormallyEtale Rₘ Sₘ

Tactic:
haveI : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))

Result:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this : FormallyEtale S Sₘ
⊢ FormallyEtale Rₘ Sₘ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem sum_mkArray_nat (n : Nat) (a : Nat) : (mkVector n a).sum = n * a

Proof state:
n a : Nat
⊢ (mkVector n a).sum = n * a

Tactic:
simp [toArray_mkVector]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem compl_lt [LinearOrder α] : (· < · : α → α → _)ᶜ = (· ≥ ·)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 => x1 < x2)ᶜ = fun x1 x2 => x1 ≥ x2

Tactic:
ext

Result:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 < x2)ᶜ x✝¹ x✝ ↔ x✝¹ ≥ x✝

Proof state:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 < x2)ᶜ x✝¹ x✝ ↔ x✝¹ ≥ x✝

Tactic:
simp [compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f g : α → β
⊢ map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Tactic:
cases l <;> simp_all

Result:
no goals