harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Basic.lean
lemma support_smul_subset_right [Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) :
    support (f • g) ⊆ support g :=
  fun x hbf hf ↦ hbf <| by rw [Pi.smul_apply', hf, smul_zero]

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
g : α → M
x : α
hbf : x ∈ support (f • g)
hf : g x = 0
⊢ (f • g) x = 0

Tactic:
rw [Pi.smul_apply', hf, smul_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem add_div_two_lt_right : (a + b) / 2 < b ↔ a < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
⊢ (a + b) / 2 < b ↔ a < b

Tactic:
simp [div_lt_iff₀, mul_two]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem one : padicNorm p 1 = 1

Proof state:
p : ℕ
⊢ padicNorm p 1 = 1

Tactic:
simp [padicNorm]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem inv_hom_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
    η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)

Tactic:
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp, norm_cast] lemma enorm_le_coe : ‖x‖ₑ ≤ r ↔ ‖x‖₊ ≤ r

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
r : ℝ≥0
⊢ ‖x‖ₑ ≤ ↑r ↔ ‖x‖₊ ≤ r

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f

Proof state:
case h.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x✝¹ : E
x✝ : F
⊢ (f.flip.flip x✝¹) x✝ = (f x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ f.flip.flip = f

Tactic:
ext

Result:
case h.h
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x✝¹ : E
x✝ : F
⊢ (f.flip.flip x✝¹) x✝ = (f x✝¹) x✝
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
@[simp]
lemma dist_prod_same_right {x₁ x₂ : α} {y : β} : dist (x₁, y) (x₂, y) = dist x₁ x₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x₁ x₂ : α
y : β
⊢ dist (x₁, y) (x₂, y) = dist x₁ x₂

Tactic:
simp [Prod.dist_eq, dist_nonneg]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovaryOn_iff_forall_mul_nonneg :
    MonovaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

Tactic:
simp only [smul_eq_mul, monovaryOn_iff_forall_smul_nonneg]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem ediam_univ_eq_top_iff_noncompact [ProperSpace α] :
    EMetric.diam (univ : Set α) = ∞ ↔ NoncompactSpace α

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ EMetric.diam univ = ⊤ ↔ NoncompactSpace α

Tactic:
rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
  Classical.not_not]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_iff_ofReal {f : α → ℝ} (h : 0 ≤ᵐ[μ] f) :
    HasFiniteIntegral f μ ↔ (∫⁻ a, ENNReal.ofReal (f a) ∂μ) < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᶠ[ae μ] f
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤

Tactic:
rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma edge_comm : edge s t = edge t s

Proof state:
V : Type u_1
s t : V
⊢ edge s t = edge t s

Tactic:
rw [edge, edge, Sym2.eq_swap]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ioo_map_sectR : (Ioo a b).map (.sectR c _) = Ioo (c, a) (c, b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioo a b) = Ioo (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem map_traverse {α β γ} (g : α → G β) (f : β → γ) (x : σ ⊕ α) :
    (f <$> ·) <$> Sum.traverse g x = Sum.traverse (f <$> g ·) x

Proof state:
σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x => f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x => f <$> g x) x

Tactic:
cases x <;> simp [Sum.traverse, id_map, functor_norm] <;> congr

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem singleton_sigma_singleton {a : ∀ i, α i} :
    (({i} : Set ι).sigma fun i ↦ ({a i} : Set (α i))) = {⟨i, a i⟩}

Proof state:
ι : Type u_1
α : ι → Type u_3
i : ι
a : (i : ι) → α i
⊢ ({i}.sigma fun i => {a i}) = {⟨i, a i⟩}

Tactic:
rw [sigma_singleton, image_singleton]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_image_le (hs : s.Finite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
⊢ ↑(f '' s).ncard ≤ ↑s.ncard

Tactic:
rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
⊢ (f '' s).encard ≤ s.encard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
⊢ (f '' s).ncard ≤ s.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
⊢ ↑(f '' s).ncard ≤ ↑s.ncard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
⊢ (f '' s).encard ≤ s.encard

Tactic:
apply encard_image_le

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
rw [div_eq_mul_inv]

Result:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Proof state:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Tactic:
exact mul_mem hx (inv_mem hy)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a

Proof state:
a b : Int
⊢ (a + b) % a = b % a

Tactic:
rw [Int.add_comm, Int.add_emod_self]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean
theorem lift_genericMonicPoly [CommRing K] [Nontrivial K] {n : ℕ} (v : Fin (n+1) → K) :
    FreeCommRing.lift v (genericMonicPoly n) =
    (((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc)).1.eval
      (v (Fin.last _))

Proof state:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : Nontrivial K
n : ℕ
v : Fin (n + 1) → K
⊢ (lift v) (genericMonicPoly n) =
    eval (v (Fin.last n)) ↑(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))

Tactic:
simp only [genericMonicPoly, map_add, map_pow, lift_of, map_sum, map_mul, monicEquivDegreeLT,
  degreeLTEquiv, Equiv.symm_trans_apply, LinearEquiv.coe_toEquiv_symm, EquivLike.coe_coe,
  LinearEquiv.coe_symm_mk, Function.comp_apply, Equiv.coe_fn_symm_mk, eval_add, eval_pow, eval_X,
  eval_finset_sum, eval_monomial]

Result:
no goals
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- A subset of a delta-generated space is open iff its preimage is open for every
  continuous map from ℝⁿ to X. -/
lemma DeltaGeneratedSpace.isOpen_iff [DeltaGeneratedSpace X] {u : Set X} :
    IsOpen u ↔ ∀ (n : ℕ) (p : ContinuousMap ((Fin n) → ℝ) X), IsOpen (p ⁻¹' u)

Proof state:
X : Type u_1
tX : TopologicalSpace X
inst✝ : DeltaGeneratedSpace X
u : Set X
⊢ IsOpen u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

Tactic:
exact isOpen_deltaGenerated_iff

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem Eq.rec_eq_cast {α : Sort _} {P : α → Sort _} {x y : α} (h : x = y) (z : P x) :
    h ▸ z = cast (congr_arg P h) z

Proof state:
α : Sort u_1
P : α → Sort u_2
x y : α
h : x = y
z : P x
⊢ h ▸ z = cast ⋯ z

Tactic:
induction h

Result:
case refl
α : Sort u_1
P : α → Sort u_2
x y : α
z : P x
⊢ ⋯ ▸ z = cast ⋯ z

Proof state:
case refl
α : Sort u_1
P : α → Sort u_2
x y : α
z : P x
⊢ ⋯ ▸ z = cast ⋯ z

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_edist_eq_of_L2 (x y : WithLp 2 (α × β)) :
    edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2 : ℝ)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ edist x y = (edist x.1 y.1 ^ 2 + edist x.2 y.2 ^ 2) ^ (1 / 2)

Tactic:
simp [prod_edist_eq_add]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b)
    (f g : R[A]) :
    (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb

Tactic:
exact (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦
  degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb

Tactic:
classical
exact (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦
  degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_nonpos_of_nonpos_of_nonneg {a b : Int}
  (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

Proof state:
a b : Int
ha : a ≤ 0
hb : 0 ≤ b
h : a * b ≤ 0 * b
⊢ a * b ≤ 0

Tactic:
rwa [Int.zero_mul] at h

Result:
no goals

Proof state:
a b : Int
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
have h : a * b ≤ 0 * b := Int.mul_le_mul_of_nonneg_right ha hb

Result:
a b : Int
ha : a ≤ 0
hb : 0 ≤ b
h : a * b ≤ 0 * b
⊢ a * b ≤ 0
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_le_bound' (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M)
    (hM : ∀ x, ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  opNorm_le_bound f hMp fun x =>
    (ne_or_eq ‖x‖ 0).elim (hM x) fun h => by
      simp only [h, mul_zero, norm_image_of_norm_zero f f.2 h, le_refl]

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖
x : E
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ M * ‖x‖

Tactic:
simp only [h, mul_zero, norm_image_of_norm_zero f f.2 h, le_refl]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_zero_left (x : V) : o.oangle 0 x = 0

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

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)]
lemma leOnePart_eq_one : a⁻ᵐ = 1 ↔ 1 ≤ a

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = 1 ↔ 1 ≤ a

Tactic:
simp [leOnePart_eq_one']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).1.size ≤ m.1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).val.size ≤ m.val.size + 1

Tactic:
simp_to_model [insert] using List.length_insertEntry_le

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem re_T_inv_smul : (T⁻¹ • z).re = z.re - 1

Proof state:
z : ℍ
⊢ (T⁻¹ • z).re = z.re - 1

Tactic:
simpa using re_T_zpow_smul z (-1)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- Basis elements have strictly monotone natural degree. -/
lemma basis_natDegree_strictMono : StrictMono <| natDegree ∘ (S.basis hCoeff) := fun _ _  ↦ by simp

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
x✝¹ x✝ : ℕ
⊢ x✝¹ < x✝ → (natDegree ∘ ⇑(S.basis hCoeff)) x✝¹ < (natDegree ∘ ⇑(S.basis hCoeff)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma toColex_lt_toColex :
    toColex s < toColex t ↔ s ≠ t ∧ ∀ ⦃a⦄, a ∈ s → a ∉ t → ∃ b, b ∈ t ∧ b ∉ s ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
⊢ { ofColex := s } < { ofColex := t } ↔ s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b

Tactic:
simp [lt_iff_le_and_ne, toColex_le_toColex, and_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_succ (f : ℕ → β) (n : ℕ) :
    (∏ x ∈ range (n + 1), f x) = (∏ x ∈ range n, f x) * f n

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

Tactic:
simp only [mul_comm, prod_range_succ_comm]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
@[simp]
lemma factorizationLCMRight_zero_right : factorizationLCMRight a 0 = 1

Proof state:
a : ℕ
⊢ a.factorizationLCMRight 0 = 1

Tactic:
simp [factorizationLCMRight]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_top {p : α → Prop} : (∃ᶠ x in ⊤, p x) ↔ ∃ x, p x

Proof state:
α : Type u
p : α → Prop
⊢ (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x

Tactic:
simp [Filter.Frequently]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGE_eq_false {o : Ordering} : o.isGE = false ↔ o = .lt

Proof state:
o : Ordering
⊢ o.isGE = false ↔ o = lt

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem Codisjoint.left_le_of_le_inf_left (h : b ⊓ a ≤ c) (hd : Codisjoint b c) : a ≤ c :=
  hd.left_le_of_le_inf_right <| by rwa [inf_comm]

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c

Tactic:
rwa [inf_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b

Proof state:
β✝ : Type u_1
b : β✝
α✝ : Type u_2
x : α✝ ⊕ β✝
h : x.isRight = true
⊢ x.getRight h = b ↔ x = inr b

Tactic:
cases x <;> simp at h ⊢

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
    getKey? k (insertList l toInsert) = getKey? k l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getKey? k (insertList l toInsert) = getKey? k l

Tactic:
rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?,
  getEntry?_insertList_of_contains_eq_false not_contains]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
⊢ getKey? k (insertList l toInsert) = getKey? k l

Tactic:
rw [← containsKey_eq_contains_map_fst] at not_contains

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getKey? k (insertList l toInsert) = getKey? k l
-- Mathlib/RingTheory/Localization/FractionRing.lean
@[simp]
lemma ringEquivOfRingEquiv_algebraMap
    (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a)

Proof state:
A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
a : A
⊢ (ringEquivOfRingEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

Tactic:
simp [ringEquivOfRingEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α}
    (distinct : l.Pairwise (fun a b => (a == b) = false)) :
    (∀ (a : α), a ∈ m → l.contains a = false) →
      (insertManyIfNewUnit m l).size = m.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (∀ (a : α), m.contains a = true → l.contains a = false) → (insertManyIfNewUnit m l).size = m.size + l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_list

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (∀ (a : α), a ∈ m → l.contains a = false) → (insertManyIfNewUnit m l).size = m.size + l.length

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (∀ (a : α), m.contains a = true → l.contains a = false) → (insertManyIfNewUnit m l).size = m.size + l.length
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_neg_left {x y : E} : ⟪-x, y⟫ = -⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x y : E
⊢ inner (-x) y = -inner x y

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Basis.lean
theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) :
    (basisSpanSingleton b hx i : S) = x * b i

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ ↑((basisSpanSingleton b hx) i) = x * b i

Tactic:
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
  Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
  LinearEquiv.restrictScalars_apply, LinearMap.mulLeft_apply, LinearMap.mul_apply']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : (p * q).Monic
⊢ q.Monic

Tactic:
contrapose! hpq

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.Monic
⊢ ¬(p * q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
rwa [leadingCoeff_monic_mul hp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.Monic
⊢ ¬(p * q).Monic

Tactic:
rw [Monic.def] at hpq ⊢

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1
-- Mathlib/Order/Filter/Prod.lean
theorem compl_diagonal_mem_prod {l₁ l₂ : Filter α} : (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Proof state:
α : Type u_1
l₁ l₂ : Filter α
⊢ (diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

Tactic:
simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleMap_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) :
    circleMap c R θ ∈ sphere c R

Proof state:
c : ℂ
R : ℝ
hR : 0 ≤ R
θ : ℝ
⊢ circleMap c R θ ∈ sphere c R

Tactic:
simpa only [abs_of_nonneg hR] using circleMap_mem_sphere' c R θ

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem conj_comp (e : α ≃ β) (f₁ f₂ : α → α) : e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

Proof state:
α : Sort u
β : Sort v
e : α ≃ β
f₁ f₂ : α → α
⊢ e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

Tactic:
apply arrowCongr_comp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem prec1 {f} (m : ℕ) (hf : Nat.Primrec f) :
    Nat.Primrec fun n => n.rec m fun y IH => f <| Nat.pair y IH :=
  ((prec (const m) (hf.comp right)).comp (zero.pair Primrec.id)).of_eq fun n => by simp

Proof state:
f : ℕ → ℕ
m : ℕ
hf : Nat.Primrec f
n : ℕ
⊢ unpaired (fun z n => Nat.rec m (fun y IH => f (unpair (Nat.pair z (Nat.pair y IH))).2) n) (Nat.pair 0 (id n)) =
    Nat.rec m (fun y IH => f (Nat.pair y IH)) n

Tactic:
simp

Result:
no goals