harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/BooleanAlgebra.lean
lemma univ_val_map_subtype_val [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.val.map ((↑) : { a // p a } → α) = (univ.filter p).val

Proof state:
case h
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
apply univ_map_subtype

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map Subtype.val univ.val = (filter p univ).val

Tactic:
apply (map_val (Function.Embedding.subtype p) univ).symm.trans

Result:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ (map (Embedding.subtype p) univ).val = (filter p univ).val

Proof state:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ (map (Embedding.subtype p) univ).val = (filter p univ).val

Tactic:
apply congr_arg

Result:
case h
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma PosSMulStrictMono.lift [PosSMulStrictMono α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b) : PosSMulStrictMono α β where
  elim a ha b₁ b₂ hb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
hb : b₁ < b₂
⊢ a • b₁ < a • b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : α → β → True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : α → β → True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Tactic:
exact smul_lt_smul_of_pos_left hb ha

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem orthogonal_eq_top_iff : Kᗮ = ⊤ ↔ K = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : Kᗮ = ⊤
this : K ⊓ Kᗮ = ⊥
⊢ K = ⊥

Tactic:
rwa [h, inf_comm, top_inf_eq] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ → K = ⊥

Tactic:
intro h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ ↔ K = ⊥

Tactic:
refine
  ⟨?_, by
    rintro rfl
    exact bot_orthogonal_eq_top⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ → K = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
exact bot_orthogonal_eq_top

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K = ⊥ → Kᗮ = ⊤

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥

Tactic:
have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : Kᗮ = ⊤
this : K ⊓ Kᗮ = ⊥
⊢ K = ⊥
-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_eq_zero_iff {p : R[X]} {x : R} :
    rootMultiplicity x p = 0 ↔ IsRoot p x → p = 0

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0

Tactic:
simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff,
  Nat.cast_zero, multiplicity_eq_zero, dvd_iff_isRoot, not_imp_not]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0

Tactic:
classical
simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff,
  Nat.cast_zero, multiplicity_eq_zero, dvd_iff_isRoot, not_imp_not]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem ret_bind (a : α) (f : α → WSeq β) : bind (ret a) f ~ʷ f a

Proof state:
α : Type u
β : Type v
a : α
f : α → WSeq β
⊢ (ret a).bind f ~ʷ f a

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem head_darts_fst {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
    (p.darts.head hp).fst = a

Proof state:
case nil
V : Type u
G : SimpleGraph V
a : V
hp : nil.darts ≠ []
⊢ (nil.darts.head hp).toProd.1 = a

Tactic:
contradiction

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
a b v✝ : V
h✝ : G.Adj a v✝
p✝ : G.Walk v✝ b
hp : (cons h✝ p✝).darts ≠ []
⊢ ((cons h✝ p✝).darts.head hp).toProd.1 = a

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (p.darts.head hp).toProd.1 = a

Tactic:
cases p

Result:
case nil
V : Type u
G : SimpleGraph V
a : V
hp : nil.darts ≠ []
⊢ (nil.darts.head hp).toProd.1 = a

case cons
V : Type u
G : SimpleGraph V
a b v✝ : V
h✝ : G.Adj a v✝
p✝ : G.Walk v✝ b
hp : (cons h✝ p✝).darts ≠ []
⊢ ((cons h✝ p✝).darts.head hp).toProd.1 = a
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_pi_empty {ι : Type u} {α : ι → Type v} [Fintype ι] [IsEmpty ι]
    {m : ∀ i, MeasurableSpace (α i)} (μ : ∀ i, Measure (α i)) :
    MeasurePreserving (MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit) (Measure.pi μ)
      (Measure.dirac ())

Proof state:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving (⇑e) (Measure.pi μ) (Measure.dirac ())

Tactic:
refine ⟨e.measurable, ?_⟩

Result:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.map (⇑e) (Measure.pi μ) = Measure.dirac ()

Proof state:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ Measure.map (⇑e) (Measure.pi μ) = Measure.dirac ()

Tactic:
rw [Measure.pi_of_empty, Measure.map_dirac e.measurable]

Result:
no goals

Proof state:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (Measure.pi μ) (Measure.dirac ())

Tactic:
set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit

Result:
ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving (⇑e) (Measure.pi μ) (Measure.dirac ())
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_mul : (p * q).smeval x  = p.smeval x * q.smeval x

Proof state:
case h_monomial
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ ((monomial n) a * q).smeval x = ((monomial n) a).smeval x * q.smeval x

Tactic:
simp only [smeval_monomial, smeval_C_mul, smeval_mul_X_pow, smeval_monomial_mul, smul_mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p * q).smeval x = p.smeval x * q.smeval x

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs =>
  simp only [add_comp, hr, hs, smeval_add, add_mul]
| h_monomial n a =>
  simp only [smeval_monomial, smeval_C_mul, smeval_mul_X_pow, smeval_monomial_mul, smul_mul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
r s : R[X]
hr : (r * q).smeval x = r.smeval x * q.smeval x
hs : (s * q).smeval x = s.smeval x * q.smeval x
⊢ ((r + s) * q).smeval x = (r + s).smeval x * q.smeval x

Tactic:
simp only [add_comp, hr, hs, smeval_add, add_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_self {a : Int} (H : a ≠ 0) : a.tdiv a = 1

Proof state:
a : Int
H : a ≠ 0
⊢ a.tdiv a = 1

Tactic:
have := Int.mul_tdiv_cancel 1 H

Result:
a : Int
H : a ≠ 0
this : (1 * a).tdiv a = 1
⊢ a.tdiv a = 1

Proof state:
a : Int
H : a ≠ 0
this : (1 * a).tdiv a = 1
⊢ a.tdiv a = 1

Tactic:
rwa [Int.one_mul] at this

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@[simp] lemma cfc_apply_zero {f : R → R} : cfc f (0 : A) = algebraMap R A (f 0)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
⊢ cfc f 0 = (algebraMap R A) (f 0)

Tactic:
simpa using cfc_algebraMap (A := A) 0 f

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem toPOUFun_zero_of_zero {i : ι} {x : X} (h : f i x = 0) : f.toPOUFun i x = 0

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
h : (f i) x = 0
⊢ f.toPOUFun i x = 0

Tactic:
rw [toPOUFun, h, zero_mul]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_inter_add_ncard_diff_eq_ncard (s t : Set α)
    (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard

Tactic:
rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
  (hs.inter_of_left _) hs.diff, union_comm, diff_union_inter]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
protected lemma mk_eq_bot_iff {p : Submodule R M} (hp : p ∈ f.invtSubmodule) :
    (⟨p, hp⟩ : f.invtSubmodule) = ⊥ ↔ p = ⊥ :=
  Subtype.mk_eq_bot_iff (by simp [invtSubmodule]) _

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
simp [invtSubmodule]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem nodup_periodicOrbit : (periodicOrbit f x).Nodup

Proof state:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n

Tactic:
rwa [iterate_eq_iterate_iff_of_lt_minimalPeriod hm hn] at hmn

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
⊢ ∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y

Tactic:
intro m hm n hn hmn

Result:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n

Proof state:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n

Tactic:
rw [List.mem_range] at hm hn

Result:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n

Proof state:
α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).Nodup

Tactic:
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on (List.nodup_range _)]

Result:
α : Type u_1
f : α → α
x : α
⊢ ∀ x_1 ∈ List.range (minimalPeriod f x), ∀ y ∈ List.range (minimalPeriod f x), f^[x_1] x = f^[y] x → x_1 = y
-- Mathlib/Data/Nat/Cast/Basic.lean
@[simp, norm_cast] lemma cast_mul (m n : ℕ) : ((m * n : ℕ) : α) = m * n

Proof state:
α : Type u_1
inst✝ : NonAssocSemiring α
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
induction n <;> simp [mul_succ, mul_add, *]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem mul_right_dvd : a * u ∣ b ↔ a ∣ b :=
  Iff.intro (fun ⟨c, eq⟩ => ⟨↑u * c, eq.trans (mul_assoc _ _ _)⟩) fun h =>
    dvd_trans (Dvd.intro (↑u⁻¹) (by rw [mul_assoc, u.mul_inv, mul_one])) h

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a

Tactic:
rw [mul_assoc, u.mul_inv, mul_one]

Result:
no goals
-- Mathlib/Data/Finset/SymmDiff.lean
theorem mem_symmDiff : a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem _root_.Monotone.upperBounds_range_comp_tendsto_atTop [Preorder β] [Preorder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
    upperBounds (range (f ∘ g)) = upperBounds (range f)

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
a : α
ha : b ≤ g a
⊢ f b ≤ c

Tactic:
exact (hf ha).trans <| hc <| mem_range_self _

Result:
no goals

Proof state:
case intro
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ f b ≤ c

Tactic:
obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists

Result:
case intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
a : α
ha : b ≤ g a
⊢ f b ≤ c

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)

Tactic:
rintro c hc _ ⟨b, rfl⟩

Result:
case intro
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ f b ≤ c

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem Monic.add_of_lt {f g : MvPolynomial σ R} (hf : m.Monic f) (h : m.degree g ≺[m] m.degree f) :
    m.Monic (f + g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.Monic (f + g)

Tactic:
simp only [Monic, leadingCoeff_add_of_lt h, hf.leadingCoeff_eq_one]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_sup_self : a ⊓ (a ⊔ b) = a

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ (a ⊔ b) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density of `A` containing `0` is `1` if and only if `A` is the naturals. -/
lemma schnirelmannDensity_eq_one_iff_of_zero_mem (hA : 0 ∈ A) :
    schnirelmannDensity A = 1 ↔ A = Set.univ

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
rw [schnirelmannDensity_eq_one_iff]

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ

Tactic:
constructor

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A

Proof state:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A

Tactic:
rintro rfl

Result:
case mpr
inst✝ : DecidablePred fun x => x ∈ Set.univ
hA : 0 ∈ Set.univ
⊢ {0}ᶜ ⊆ Set.univ

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
⊢ x ∈ A

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case mp.inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

case mp.inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
hx : x ≠ 0
⊢ x ∈ A

Proof state:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

Tactic:
refine fun h => Set.eq_univ_of_forall fun x => ?_

Result:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
⊢ x ∈ A

Proof state:
case mp.inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

Tactic:
exact hA

Result:
no goals

Proof state:
case mp.inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
hx : x ≠ 0
⊢ x ∈ A

Tactic:
exact h hx

Result:
no goals

Proof state:
case mpr
inst✝ : DecidablePred fun x => x ∈ Set.univ
hA : 0 ∈ Set.univ
⊢ {0}ᶜ ⊆ Set.univ

Tactic:
exact Set.subset_univ {0}ᶜ

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem sMod_nonneg (p : ℕ) (hp : p ≠ 0) (i : ℕ) : 0 ≤ sMod p i

Proof state:
case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ 4 % (2 ^ p - 1)

Tactic:
exact sup_eq_right.mp rfl

Result:
no goals

Proof state:
case succ.a
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0

Tactic:
exact mersenne_int_ne_zero p hp

Result:
no goals

Proof state:
case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)

Tactic:
apply Int.emod_nonneg

Result:
case succ.a
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0

Proof state:
p : ℕ
hp : p ≠ 0
i : ℕ
⊢ 0 ≤ sMod p i

Tactic:
cases i <;> dsimp [sMod]

Result:
case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ 4 % (2 ^ p - 1)

case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingularLift_addMap {P Q : PointClass F} (hP : W.NonsingularLift P)
    (hQ : W.NonsingularLift Q) : W.NonsingularLift <| W.addMap P Q

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
⊢ W.NonsingularLift (W.addMap P Q)

Tactic:
rcases P

Result:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Proof state:
case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Tactic:
exact nonsingular_add hP hQ

Result:
no goals

Proof state:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
hQ : W.NonsingularLift Q
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝) Q)

Tactic:
rcases Q

Result:
case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
lemma LinearIndependent.eq_zero_of_pair' {x y : M} (h : LinearIndependent R ![x, y])
    {s t : R} (h' : s • x = t • y) : s = 0 ∧ t = 0

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ t = 0

Tactic:
suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩

Result:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ 0 = t

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s • x + 0 • y = 0 • x + t • y

Tactic:
simpa using h'

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ 0 = t

Tactic:
exact h.eq_of_pair (by simpa using h')

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem inits_reverse (l : List α) : inits (reverse l) = reverse (map reverse l.tails)

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse

Tactic:
simp [reverse_involutive.comp_self, ← map_reverse]

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse l.tails).reverse

Tactic:
rw [tails_eq_inits l]

Result:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse