harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.mul_const (hc : HasDerivAt c c' x) (d : 𝔸) :
    HasDerivAt (fun y => c y * d) (c' * d) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivAt c c' x
d : 𝔸
⊢ HasDerivAt (fun y => c y * d) (c' * d) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' univ x
d : 𝔸
⊢ HasDerivWithinAt (fun y => c y * d) (c' * d) univ x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' univ x
d : 𝔸
⊢ HasDerivWithinAt (fun y => c y * d) (c' * d) univ x

Tactic:
exact hc.mul_const d

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_neg {n' a : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn : n' + a = n) :
    (-γ).rightUnshift n hn = -γ.rightUnshift n hn

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.rightUnshift n hn

Tactic:
apply _root_.map_neg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (-γ).rightUnshift n hn = -γ.rightUnshift n hn

Tactic:
change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.rightUnshift n hn
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_filter {xs : Array α} (p q : α → Bool) :
    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a)

Proof state:
α : Type u_1
xs : Array α
p q : α → Bool
⊢ find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
⊢ find? q (filter p { toList := toList✝ }) = find? (fun a => decide (p a = true ∧ q a = true)) { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
⊢ find? q (filter p { toList := toList✝ }) = find? (fun a => decide (p a = true ∧ q a = true)) { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_apply_left {f : α → β} (hf : Function.Injective f) (x z : α) (y : M) :
    single (f x) y (f z) = single x y z

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hf : Injective f
x z : α
y : M
⊢ (single (f x) y) (f z) = (single x y) z

Tactic:
simp only [single_apply, hf.eq_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hf : Injective f
x z : α
y : M
⊢ (single (f x) y) (f z) = (single x y) z

Tactic:
classical simp only [single_apply, hf.eq_iff]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem isUnit_iff_ne_zero : IsUnit a ↔ a ≠ 0 :=
  (Units.exists_iff_ne_zero (p := (· = a))).trans (by simp)

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ (∃ x, x ≠ 0 ∧ x = a) ↔ a ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem smul_eq_C_mul (f : MvPowerSeries σ R) (a : R) : a • f = C σ R a * f

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ (coeff R n✝) (a • f) = (coeff R n✝) ((C σ R) a * f)

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
⊢ a • f = (C σ R) a * f

Tactic:
ext

Result:
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
a : R
n✝ : σ →₀ ℕ
⊢ (coeff R n✝) (a • f) = (coeff R n✝) ((C σ R) a * f)
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp]
lemma enorm_inv {a : α} (ha : a ≠ 0) : ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Tactic:
simp [enorm, ENNReal.coe_inv, ha]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma le_div_comm₀ (ha : 0 < a) (hc : 0 < c) : a ≤ b / c ↔ c ≤ b / a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
⊢ a ≤ b / c ↔ c ≤ b / a

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b / c ↔ c ≤ b / a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
ha : 0 < a
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b / c ↔ c ≤ b / a

Tactic:
rw [le_div_iff₀ ha, le_div_iff₀' hc]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_le_tsub_add_tsub : a - c ≤ a - b + (b - c)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a - c ≤ a - b + (b - c)

Tactic:
rw [tsub_le_iff_left, ← add_assoc, add_right_comm]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a ≤ c + (b - c) + (a - b)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a ≤ c + (b - c) + (a - b)

Tactic:
exact le_add_tsub.trans (add_le_add_right le_add_tsub _)

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem discreteTopology_iff_finite_and_isPrime_imp_isMaximal :
    DiscreteTopology (PrimeSpectrum R) ↔
    Finite (PrimeSpectrum R) ∧ ∀ I : Ideal R, I.IsPrime → I.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ DiscreteTopology (PrimeSpectrum R) ↔ Finite (PrimeSpectrum R) ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem degree_toSubring : (toSubring p T hp).degree = p.degree

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).degree = p.degree

Tactic:
simp [degree]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) :
    X.σ j.succ ≫ X.δ (Fin.castSucc i) = X.δ i ≫ X.σ j

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem le_antisymm {a b : ℤ√d} (ab : a ≤ b) (ba : b ≤ a) : a = b :=
  eq_of_sub_eq_zero <| nonneg_antisymm ba (by rwa [neg_sub])

Proof state:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
ba : b ≤ a
⊢ (-(a - b)).Nonneg

Tactic:
rwa [neg_sub]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_inf {H₁ H₂ : Subgraph G} : (H₁ ⊓ H₂).edgeSet = H₁.edgeSet ∩ H₂.edgeSet :=
  Set.ext <| Sym2.ind (by simp)

Proof state:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊓ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∩ H₂.edgeSet

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_eq_nil_iff {p : Perm α} {x} : toList p x = [] ↔ x ∉ p.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ p.toList x = [] ↔ x ∉ p.support

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_empty : toSet ∅ = ∅

Proof state:
⊢ ∅.toSet = ∅

Tactic:
simp [toSet]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem principal_units_le_units : A.principalUnitGroup ≤ A.unitGroup := fun a h => by
  simpa only [add_sub_cancel] using A.valuation.map_one_add_of_lt h

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : Kˣ
h : a ∈ A.principalUnitGroup
⊢ a ∈ A.unitGroup

Tactic:
simpa only [add_sub_cancel] using A.valuation.map_one_add_of_lt h

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma isLoop_iff_closure_eq_loops_and_mem_ground :
    M.IsLoop e ↔ M.closure {e} = M.loops ∧ e ∈ M.E where
  mp h := ⟨h.closure, h.mem_ground⟩
  mpr h

Proof state:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ M.IsLoop e

Tactic:
rw [isLoop_iff, ← singleton_subset_iff, ← closure_subset_closure_iff_subset_closure, h.1]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma pow_rpow_inv_natCast {n : ℕ} (hn : n ≠ 0) (x : ℝ≥0∞) : (x ^ n) ^ (n⁻¹ : ℝ) = x

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ ↑n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← rpow_natCast, ← rpow_mul, mul_inv_cancel₀ (by positivity), rpow_one]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem mem_support_normalize_iff (a : α) : a ∈ (normalize f hf0 hf).support ↔ f a ≠ 0

Proof state:
α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ (normalize f hf0 hf).support ↔ f a ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_cons {i} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i)
    (hgr : g ∉ (φ i).range) : (cons g w hmw hgr).prod = of i g * w.prod

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
g : G i
w : NormalWord d
hmw : w.fstIdx ≠ some i
hgr : g ∉ (φ i).range
⊢ (cons g w hmw hgr).prod = (of i) g * w.prod

Tactic:
simp [prod, cons, ← of_apply_eq_base φ i, equiv_fst_eq_mul_inv, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_inf : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆

Tactic:
constructor <;>
apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆

Tactic:
rw [le_inf_iff]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem adjoint_apply_of_not_dense (hT : ¬Dense (T.domain : Set E)) (y : T†.domain) : T† y = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ (if hT : Dense ↑T.domain then adjointAux hT else 0) y = 0

Tactic:
simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ ↑T† y = 0

Tactic:
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ (if hT : Dense ↑T.domain then adjointAux hT else 0) y = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ ↑T† y = 0

Tactic:
classical
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithBot.toDual_lt_toDual_iff {x y : WithBot α} : x.toDual < y.toDual ↔ y < x

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ WithBot.toDual x < WithBot.toDual y ↔ y < x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_pow (a : M) {n : Nat} (hn : 0 < n) : radical (a ^ n) = radical a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : 0 < n
⊢ radical (a ^ n) = radical a

Tactic:
simp_rw [radical, primeFactors_pow a hn]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.sub (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
h₂ : f₂ =O[l] g
⊢ (fun x => f₁ x - f₂ x) =O[l] g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Basic.lean
lemma left_hom_inv_right [IsIso e] : L.map (e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Proof state:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ L.map e.left ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp :
    ((coproducts.{w} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ ((coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
apply transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem leftInvSeq_reverse (ω : List B) :
    lis (ω.reverse) = (ris ω).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} {x : A} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
ι : Sort u_1
S : ι → NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
/-- `M.restrictSubtype M.E` is isomorphic to `M`. -/
lemma map_val_restrictSubtype_ground_eq (M : Matroid α) :
    (M.restrictSubtype M.E).map (↑) Subtype.val_injective.injOn = M

Proof state:
α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E).map Subtype.val ⋯ = M

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_ker {x : L} : x ∈ ker f ↔ f x = 0 :=
  show x ∈ LieSubmodule.toSubmodule (f.ker) ↔ _ by
    simp only [ker_toSubmodule, LinearMap.mem_ker, coe_toLinearMap]

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
x : L
⊢ x ∈ ↑f.ker ↔ f x = 0

Tactic:
simp only [ker_toSubmodule, LinearMap.mem_ker, coe_toLinearMap]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem AntitoneOn.concaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D))
    (h_anti : AntitoneOn (deriv f) (interior D)) : ConcaveOn ℝ D f :=
  haveI : MonotoneOn (deriv (-f)) (interior D)

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
h_anti : AntitoneOn (deriv f) (interior D)
⊢ MonotoneOn (deriv (-f)) (interior D)

Tactic:
simpa only [← deriv.neg] using h_anti.neg

Result:
no goals
-- Mathlib/Tactic/Group.lean
theorem zpow_trick_one {G : Type*} [Group G] (a b : G) (m : ℤ) :
    a * b * b ^ m = a * b ^ (m + 1)

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)

Tactic:
rw [mul_assoc, mul_self_zpow]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem normalizer_sup_eq_top' {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal]
    [Finite (Sylow p N)] (P : Sylow p G) (hP : P ≤ N) : P.normalizer ⊔ N = ⊤

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ (↑P).normalizer ⊔ N = ⊤

Tactic:
rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
  inf_of_le_left hP]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_map_iff {l₁ : List β} {f : α → β} :
    l₁ <+ l₂.map f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.map f

Proof state:
β : Type u_1
α : Type u_2
l₂ : List α
l₁ : List β
f : α → β
⊢ l₁ <+ map f l₂ ↔ ∃ l', l' <+ l₂ ∧ l₁ = map f l'

Tactic:
simp only [← filterMap_eq_map, sublist_filterMap_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNFRec_zero {C : Ordinal → Sort*} (b : Ordinal) (H0 : C 0)
    (H : ∀ o, o ≠ 0 → C (o % b ^ log b o) → C o) : CNFRec b H0 H 0 = H0

Proof state:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ b.CNFRec H0 H 0 = H0

Tactic:
rw [CNFRec, dif_pos rfl]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
lemma sub_half (a : K) : a - a / 2 = a / 2

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a - a / 2 = a / 2

Tactic:
rw [sub_eq_iff_eq_add, add_halves]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem results_of_terminates' (s : Computation α) [T : Terminates s] {a} (h : a ∈ s) :
    Results s a (length s)

Proof state:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results a s.length

Tactic:
rw [← get_eq_of_mem _ h]

Result:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length

Proof state:
α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results s.get s.length

Tactic:
apply results_of_terminates

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
@[simp] lemma Finset.centerMass_neg_left : t.centerMass (-w) z = t.centerMass w z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
⊢ t.centerMass (-w) z = t.centerMass w z

Tactic:
simp [centerMass, inv_neg]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Locally.lean
lemma locally_of_locally {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
    (hPQ : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, P f → Q f)
    {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S} (hf : Locally P f) : Locally Q f

Proof state:
case intro.intro
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
exact ⟨s, hsone, fun t ht ↦ hPQ (hs t ht)⟩

Result:
no goals

Proof state:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q) f

Tactic:
obtain ⟨s, hsone, hs⟩ := hf

Result:
case intro.intro
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => Q) f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a ∈ l

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l.reverse.head?
⊢ a ∈ l.reverse

Tactic:
exact mem_of_mem_head? h

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l.getLast?
⊢ a ∈ l

Tactic:
rw [getLast?_eq_head?_reverse] at h

Result:
α : Type u_1
l : List α
a : α
h : a ∈ l.reverse.head?
⊢ a ∈ l

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l.reverse.head?
⊢ a ∈ l

Tactic:
rw [← mem_reverse]

Result:
α : Type u_1
l : List α
a : α
h : a ∈ l.reverse.head?
⊢ a ∈ l.reverse
-- Mathlib/Algebra/Ring/Commute.lean
lemma neg_sq (a : R) : (-a) ^ 2 = a ^ 2

Proof state:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a) ^ 2 = a ^ 2

Tactic:
simp [sq]

Result:
no goals