harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).getKey! k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_inv_mul_iff_le : 1 ≤ b⁻¹ * a ↔ b ≤ a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem map_zipIdx (f : α → β) (l : Array α) (k : Nat) :
    map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
k : Nat
⊢ map (Prod.map f id) (l.zipIdx k) = (map f l).zipIdx k

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
k : Nat
toList✝ : List α
⊢ map (Prod.map f id) ({ toList := toList✝ }.zipIdx k) = (map f { toList := toList✝ }).zipIdx k

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
k : Nat
toList✝ : List α
⊢ map (Prod.map f id) ({ toList := toList✝ }.zipIdx k) = (map f { toList := toList✝ }).zipIdx k

Tactic:
simp [List.map_zipIdx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem two_pow_pred_lt_two_pow {w : Nat} (h : 0 < w) :
    2 ^ (w - 1) < 2 ^ w :=
  Nat.pow_pred_lt_pow (by omega) h

Proof state:
w : Nat
h : 0 < w
⊢ 1 < 2

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b)
    (hpb : p ∈ b.primeFactorsList) : (a * b).factorization p = b.factorization p

Proof state:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (a * b).factorization p = b.factorization p

Tactic:
rw [mul_comm]

Result:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (b * a).factorization p = b.factorization p

Proof state:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ (b * a).factorization p = b.factorization p

Tactic:
exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem inv_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < cos x) : (√(1 + tan x ^ 2))⁻¹ = cos x

Proof state:
x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = cos x

Tactic:
rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/--
The completed L-function of the (unique) Dirichlet character mod 1 is the completed Riemann zeta
function.
-/
lemma completedLFunction_modOne_eq {χ : DirichletCharacter ℂ 1} :
    completedLFunction χ = completedRiemannZeta

Proof state:
χ : DirichletCharacter ℂ 1
⊢ completedLFunction χ = completedRiemannZeta

Tactic:
ext

Result:
case h
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ completedLFunction χ x✝ = completedRiemannZeta x✝

Proof state:
case h
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ completedLFunction χ x✝ = completedRiemannZeta x✝

Tactic:
rw [completedLFunction, ZMod.completedLFunction_modOne_eq, map_one, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem fixedBy_eq_univ_iff_eq_one {m : M} : fixedBy α m = Set.univ ↔ m = 1

Proof state:
α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ fixedBy α m = Set.univ ↔ m = 1

Tactic:
rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]

Result:
α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ (fun x2 => m • x2) = fun x2 => 1 • x2

Proof state:
α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ (fun x2 => m • x2) = fun x2 => 1 • x2

Tactic:
simp_rw [funext_iff, one_smul, mem_fixedBy]

Result:
no goals
-- Mathlib/Data/DFinsupp/Module.lean
theorem comapDomain_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)]
    (h : κ → ι) (hh : Function.Injective h) (r : γ) (f : Π₀ i, β i) :
    comapDomain h hh (r • f) = r • comapDomain h hh f

Proof state:
case h
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (r • f)) i✝ = (r • comapDomain h hh f) i✝

Tactic:
rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain h hh (r • f) = r • comapDomain h hh f

Tactic:
ext

Result:
case h
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (r • f)) i✝ = (r • comapDomain h hh f) i✝
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConcaveOn.smul_convexOn' (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : AntivaryOn f g s) :
    ConcaveOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem Function.Injective.isOfFinOrder_iff [Monoid H] {f : G →* H} (hf : Injective f) :
    IsOfFinOrder (f x) ↔ IsOfFinOrder x

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
x : G
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
⊢ IsOfFinOrder (f x) ↔ IsOfFinOrder x

Tactic:
rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Polish.lean
theorem IsClopenable.compl [TopologicalSpace α] {s : Set α} (hs : IsClopenable s) :
    IsClopenable sᶜ

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopenable s
⊢ IsClopenable sᶜ

Tactic:
rcases hs with ⟨t, t_le, t_polish, h, h'⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed s
h' : IsOpen s
⊢ IsClopenable sᶜ

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t : TopologicalSpace α
t_le : t ≤ inst✝
t_polish : PolishSpace α
h : IsClosed s
h' : IsOpen s
⊢ IsClopenable sᶜ

Tactic:
exact ⟨t, t_le, t_polish, @IsOpen.isClosed_compl α t s h', @IsClosed.isOpen_compl α t s h⟩

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem sup_iff_not_inf_not : (φ ⊔ ψ) ⇔[T] (φ.not ⊓ ψ.not).not :=
  fun M v xs => by simp [imp_iff_not_or]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊔ ψ ⇔ ∼(∼φ ⊓ ∼ψ)).Realize v xs

Tactic:
simp [imp_iff_not_or]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_eq_sum : p.smeval x = p.sum (smul_pow x)

Proof state:
R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ p.smeval x = p.sum (smul_pow x)

Tactic:
rw [smeval_def]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
theorem complex_d_succ_comp (n : ℕ) :
    P.complex.d n (n + 1) ≫ P.complex.d (n + 1) (n + 2) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ P.complex.d n (n + 1) ≫ P.complex.d (n + 1) (n + 2) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pred_lt_castPred_iff {a b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ last n) :
    pred a ha < castPred b hb ↔ a ≤ b

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ a.pred ha < b.castPred hb ↔ a ≤ b

Tactic:
rw [lt_castPred_iff, castSucc_pred_lt_iff ha]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem coe_mk (hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure) :
    ⇑(HilbertBasis.mk hv hsp) = v

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
⊢ ⇑(HilbertBasis.mk hv hsp) = v

Tactic:
classical
apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure
⊢ ⇑(HilbertBasis.mk hv hsp) = v

Tactic:
apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem leftRel_eq : ⇑(leftRel s) = fun x y => x⁻¹ * y ∈ s :=
  funext₂ <| by
    simp only [eq_iff_iff]
    apply leftRel_apply

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s) a b ↔ a⁻¹ * b ∈ s

Tactic:
apply leftRel_apply

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s) a b = (a⁻¹ * b ∈ s)

Tactic:
simp only [eq_iff_iff]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s) a b ↔ a⁻¹ * b ∈ s
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_subset_right [DecidableEq β] :
    image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t' :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_subset_right

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∩ image2 f ↑s ↑t'

Tactic:
exact image2_inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∩ t')) ⊆ ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∩ image2 f ↑s ↑t'
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
    F.map (prod.map f g) ≫ prodComparison F A' B' =
      prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Tactic:
rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
  F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem toFractionRing_eq :
    (toFractionRing : RatFunc K → FractionRing K[X]) = IsLocalization.algEquiv K[X]⁰ _ _ :=
  funext fun ⟨x⟩ =>
    Localization.induction_on x fun x => by
      simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝¹ : RatFunc K
x✝ : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 }.toFractionRing =
    (IsLocalization.algEquiv K[X]⁰ (RatFunc K) (FractionRing K[X])) { toFractionRing := Localization.mk x.1 x.2 }

Tactic:
simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
  IsLocalization.map_mk', RingHom.id_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.apply_eq_self_iff : SameCycle f x y → (f x = x ↔ f y = y) := fun ⟨i, hi⟩ => by
  rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]

Proof state:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ f y = y

Tactic:
rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
  (f ^ i).injective.eq_iff]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma removeNth_zero (f : ∀ i, α i) : removeNth 0 f = tail f

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ removeNth 0 f x✝ = tail f x✝

Tactic:
simp [tail, removeNth]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
⊢ removeNth 0 f = tail f

Tactic:
ext

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ removeNth 0 f x✝ = tail f x✝
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2)
    (h_three : p ≠ 3) : 5 ≤ p

Proof state:
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False

Tactic:
decide +revert

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False

Tactic:
revert h_two h_three hp

Result:
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False

Proof state:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p

Tactic:
by_contra! h

Result:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
-- Mathlib/Data/Set/Image.lean
theorem subset_image_diff (f : α → β) (s t : Set α) : f '' s \ f '' t ⊆ f '' (s \ t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)

Tactic:
exact image_subset f subset_union_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)

Tactic:
rw [diff_subset_iff, ← image_union, union_diff_self]

Result:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).getKey? k = none

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).getKey? k = none

Tactic:
simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_le_smul_iff_of_neg_left [PosSMulMono α β] [PosSMulReflectLE α β] (ha : a < 0) :
    a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]

Result:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁴ : OrderedRing α
inst✝³ : OrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ -a • b₂ ≤ -a • b₁ ↔ b₂ ≤ b₁

Tactic:
exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_zero_iff_subsingleton_of_finite [Finite s] : s.infsep = 0 ↔ s.Subsingleton

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 → s.Subsingleton

Tactic:
exact fun H => (einfsep_pos_of_finite.ne' H).elim

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 → s.Subsingleton
-- Mathlib/GroupTheory/Perm/Support.lean
theorem pow_apply_eq_of_apply_apply_eq_self {x : α} (hffx : f (f x) = x) :
    ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x
  | 0 => Or.inl rfl
  | n + 1 =>
    (pow_apply_eq_of_apply_apply_eq_self hffx n).elim
      (fun h => Or.inr (by rw [pow_succ', mul_apply, h]))
      fun h => Or.inl (by rw [pow_succ', mul_apply, h, hffx])

Proof state:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = f x
⊢ (f ^ (n + 1)) x = x

Tactic:
rw [pow_succ', mul_apply, h, hffx]

Result:
no goals

Proof state:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = x
⊢ (f ^ (n + 1)) x = f x

Tactic:
rw [pow_succ', mul_apply, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma natDegree_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).natDegree = p.natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).natDegree = p.natDegree

Tactic:
simp [natDegree, degree_mul_C_of_isUnit ha]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_of_mem {o : Part α} {a : α} (h : a ∈ o) (f : α → Part β) : o.bind f = f a

Proof state:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ o.bind f = f a

Tactic:
rw [eq_some_iff.2 h, bind_some]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
    ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
  LinearMap.mkContinuous_norm_le _ (by positivity) _

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ 0 ≤ ∏ i : ι, ‖f i‖

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ =>
  ⟨L₁, concat L₂ a, by simp [← h, concat_eq_append, append_assoc]⟩

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
a : α✝
x✝ : l₁ <:+: l₂
L₁ L₂ : List α✝
h : L₁ ++ l₁ ++ L₂ = l₂
⊢ L₁ ++ l₁ ++ L₂.concat a = l₂.concat a

Tactic:
simp [← h, concat_eq_append, append_assoc]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_sq (h : 0 ≤ x) : √(x ^ 2) = x

Proof state:
x : ℝ
h : 0 ≤ x
⊢ √(x ^ 2) = x

Tactic:
rw [sq, sqrt_mul_self h]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (x : α) :
    f (x - c) = -f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
x : α
⊢ f (x - c) = -f x

Tactic:
simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem ne_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ y :=
  o.ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Part.lean
@[simp] lemma toOption_eq_none (o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
by_cases h : o.Dom <;> simp [h, toOption]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_ratCast_im (z : ℂ) (x : ℚ) : (z / x).im = z.im / x

Proof state:
z : ℂ
x : ℚ
⊢ (z / ↑x).im = z.im / ↑x

Tactic:
rw [div_ratCast]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem map_zero (h : QuasispectrumRestricts a f) : f 0 = 0

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Field S
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : Module S A
inst✝ : Algebra R S
a : A
f : S → R
h : QuasispectrumRestricts a f
⊢ f 0 = 0

Tactic:
rw [← h.left_inv 0, map_zero (algebraMap R S)]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_ι (x : M) : ι Q x⌊d = algebraMap R _ (d x)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : M
⊢ (contractRight ((ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)

Tactic:
rw [contractRight_eq, reverse_ι, contractLeft_ι, reverse.commutes]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_map (f : β → α) (l : Array β) : (map f l).eraseP p = map f (l.eraseP (p ∘ f))

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : Array β
⊢ (map f l).eraseP p = map f (l.eraseP (p ∘ f))

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ (map f { toList := l }).eraseP p = map f ({ toList := l }.eraseP (p ∘ f))

Proof state:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ (map f { toList := l }).eraseP p = map f ({ toList := l }.eraseP (p ∘ f))

Tactic:
simpa using List.eraseP_map f l

Result:
no goals