harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_whiskerRight {f g h : C}
    {η η' : f ⟶ g} {θ : f ⊗ h ⟶ g ⊗ h}
    (e_η : η = η') (e_θ : η' ▷ h = θ) :
    η ▷ h = θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : f ⟶ g
θ : f ⊗ h ⟶ g ⊗ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
simp [e_η, e_θ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_cons_of_pos {l : List α} {p} (h : p a) : (a :: l).eraseP p = l

Proof state:
α : Type u_1
a : α
l : List α
p : α → Bool
h : p a = true
⊢ eraseP p (a :: l) = l

Tactic:
simp [eraseP_cons, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKeyD_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a fallback : α} :
    m.getKeyD a fallback = List.getKeyD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a fallback : α
⊢ m.getKeyD a fallback = List.getKeyD a (toListModel m.val.buckets) fallback

Tactic:
rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hm]

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConcaveOn.lipschitzOnWith_of_abs_le (hf : ConcaveOn ℝ (ball x₀ r) f) (hε : 0 < ε)
    (hM : ∀ a, dist a x₀ < r → |f a| ≤ M) :
    LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ ∀ (a : E), dist a x₀ < r → |(-f) a| ≤ M

Tactic:
simpa using hM

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))

Tactic:
simpa using hf.neg.lipschitzOnWith_of_abs_le hε <| by simpa using hM

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_le_iff₃ : a ⨳ b ⨳ c ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c,
    a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' <
      d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Proof state:
a b c d : Ordinal.{u}
⊢ a ⨳ b ⨳ c ≤ d ↔
    ∀ a' < a,
      ∀ b' < b,
        ∀ c' < c, a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Tactic:
simpa using lt_nmul_iff₃.not

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem length_eq_reduceOption_length_add_filter_none {l : List (Option α)} :
    l.length = l.reduceOption.length + (l.filter Option.isNone).length

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length

Tactic:
simp_rw [reduceOption_length_eq, l.length_eq_length_filter_add Option.isSome, Option.bnot_isSome]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_equation (hf : Function.Injective f) (P : Fin 3 → A) :
    (W'.baseChange B).toProjective.Equation (f ∘ P) ↔
      (W'.baseChange A).toProjective.Equation P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.Equation (⇑f ∘ P) ↔ (baseChange W' A).toProjective.Equation P

Tactic:
rw [← RingHom.coe_coe, ← map_equation hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem ofReal_toReal_eq_iff : ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤ :=
  ⟨fun h => by
    rw [← h]
    exact ofReal_ne_top, ofReal_toReal⟩

Proof state:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ ENNReal.ofReal a.toReal ≠ ⊤

Tactic:
exact ofReal_ne_top

Result:
no goals

Proof state:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ a ≠ ⊤

Tactic:
rw [← h]

Result:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ ENNReal.ofReal a.toReal ≠ ⊤
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_left' (a b : α) : toIocMod hp (p + a) b = p + toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_right', add_comm]

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem mem_pure : b ∈ pure a ↔ b = a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ b ∈ pure a ↔ b = a

Tactic:
rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true

Proof state:
w : Nat
h : 0 < w
⊢ (1#w)[0] = true

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem map_birkhoffAverage (S : Type*) {F N : Type*}
    [DivisionSemiring S] [AddCommMonoid N] [Module S N] [FunLike F M N]
    [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) :
    g' (birkhoffAverage R f g n x) = birkhoffAverage S f (g' ∘ g) n x

Proof state:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁷ : DivisionSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_4
F : Type u_5
N : Type u_6
inst✝⁴ : DivisionSemiring S
inst✝³ : AddCommMonoid N
inst✝² : Module S N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
g' : F
f : α → α
g : α → M
n : ℕ
x : α
⊢ g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x

Tactic:
simp only [birkhoffAverage, map_inv_natCast_smul g' R S, map_birkhoffSum]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorMapObjDesc {X : GradedObject I C₁} {Y : GradedObject J C₂} {A : C₃} {k : K}
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p]
    (f : ∀ (i : I) (j : J) (_ : p ⟨i, j⟩ = k), (F.obj (X i)).obj (Y j) ⟶ A)
    (i : I) (j : J) (hij : p ⟨i, j⟩ = k) :
    ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)
i : I
j : J
hij : p (i, j) = k
⊢ ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij

Tactic:
apply ι_descMapObj

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem testBit_lor (m n k) : testBit (lor m n) k = (testBit m k || testBit n k)

Proof state:
m n : ℤ
k : ℕ
⊢ (m.lor n).testBit k = (m.testBit k || n.testBit k)

Tactic:
rw [← bitwise_or, testBit_bitwise]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
@[simp]
lemma map_incl_le {N' : LieSubmodule R L N} :
    N'.map N.incl ≤ 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 : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ N

Tactic:
conv_rhs => rw [← N.map_incl_top]

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 : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ map N.incl ⊤

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 : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' ≤ map N.incl ⊤

Tactic:
exact LieSubmodule.map_mono le_top

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem leftUnitor_tensor' (X Y : C) :
    (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y)

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem uniqueDiffOn_extChartAt_target (x : M) : UniqueDiffOn 𝕜 (extChartAt I x).target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (extChartAt I x).target

Tactic:
rw [extChartAt_target]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)

Tactic:
exact I.uniqueDiffOn_preimage (chartAt H x).open_target

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_inv (x : ℝ) : √x⁻¹ = (√x)⁻¹

Proof state:
x : ℝ
⊢ √x⁻¹ = (√x)⁻¹

Tactic:
rw [Real.sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, Real.sqrt]

Result:
no goals
-- Mathlib/Algebra/Group/Conj.lean
theorem MonoidHom.map_isConj (f : α →* β) {a b : α} : IsConj a b → IsConj (f a) (f b)
  | ⟨c, hc⟩ => ⟨Units.map f c, by rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑((Units.map f) c)) (f a) (f b)

Tactic:
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem one_mul_hom {Z : C} (f : Z ⟶ M.X) : (M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Mon_ C
Z : C
f : Z ⟶ M.X
⊢ (M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f

Tactic:
rw [tensorHom_def'_assoc, M.one_mul, leftUnitor_naturality]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ,
    (n + k).descFactorial k = (n + 1).ascFactorial k
  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
  | succ k => by
    rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
      add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]

Proof state:
n : ℕ
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0

Tactic:
rw [ascFactorial_zero, descFactorial_zero]

Result:
no goals

Proof state:
n k : ℕ
⊢ (n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ

Tactic:
rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ,
  add_descFactorial_eq_ascFactorial _ k, Nat.add_right_comm]

Result:
no goals
-- Mathlib/Condensed/Light/Epi.lean
lemma epi_iff_locallySurjective_on_lightProfinite : Epi f ↔
    ∀ (S : LightProfinite) (y : Y.val.obj ⟨S⟩),
      (∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : X.val.obj ⟨S'⟩),
        f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y)

Proof state:
X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : Y.val.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x, f.val.app (Opposite.op S') x = Y.val.map (Opposite.op φ) y

Tactic:
exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

Result:
no goals

Proof state:
X Y : LightCondSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : Y.val.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x, f.val.app (Opposite.op S') x = Y.val.map (Opposite.op φ) y

Tactic:
rw [← isLocallySurjective_iff_epi']

Result:
X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : Y.val.obj (Opposite.op S)),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x, f.val.app (Opposite.op S') x = Y.val.map (Opposite.op φ) y
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_inv' (a : E) : ‖a⁻¹‖ = ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ = ‖a‖

Tactic:
simpa using norm_div_rev 1 a

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
@[simp]
lemma rdrop_append_length_add {l₁ l₂ : List α} (k : ℕ) :
    List.rdrop (l₁ ++ l₂) (length l₂ + k) = List.rdrop l₁ k

Proof state:
α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k

Tactic:
rw [← rdrop_add, rdrop_append_length]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem codisjoint_iff_toSubmodule :
    Codisjoint N N' ↔ Codisjoint (N : Submodule R M) (N' : Submodule R M)

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
⊢ Codisjoint N N' ↔ Codisjoint ↑N ↑N'

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← toSubmodule_inj, sup_toSubmodule,
  top_toSubmodule, ← codisjoint_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Opposite.lean
lemma oppositeShiftFunctorAdd'_inv_app :
    (shiftFunctorAdd' (OppositeShift C A) a b c h).inv.app X =
      ((shiftFunctorAdd' C a b c h).hom.app X.unop).op

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b c : A
h : a + b = c
⊢ (shiftFunctorAdd' (OppositeShift C A) a b c h).inv.app X = ((shiftFunctorAdd' C a b c h).hom.app (Opposite.unop X)).op

Tactic:
subst h

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).inv.app X =
    ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app (Opposite.unop X)).op

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).inv.app X =
    ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app (Opposite.unop X)).op

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_inv_app]

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma hom_inv_apply {X Y : Semigrp} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : Semigrp
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
    (arr.push a).foldrM f init = f a init >>= arr.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
a : α
⊢ foldrM f init (arr.push a) = do
    let init ← f a init
    foldrM f init arr

Tactic:
simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
  List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_inv_right_eq {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
    lift f (g ≫ B.inv) ≫ B.mul = h ↔ f = lift h g ≫ B.mul

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ lift f (g ≫ B.inv) ≫ B.mul = h ↔ f = lift h g ≫ B.mul

Tactic:
rw [eq_comm, eq_lift_inv_right, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/Valuation/RankOne.lean
theorem zero_of_hom_zero {x : Γ₀} (hx : hom v x = 0) : x = 0

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
⊢ False

Tactic:
have hs := strictMono v h_lt

Result:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
hs : (hom v) 0 < (hom v) x
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
hs : (hom v) 0 < (hom v) x
⊢ False

Tactic:
rw [_root_.map_zero, hx] at hs

Result:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
hs : 0 < 0
⊢ False

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
hs : 0 < 0
⊢ False

Tactic:
exact hs.false

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
⊢ x = 0

Tactic:
refine (eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm

Result:
R : Type u_1
inst✝² : Ring R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.RankOne
x : Γ₀
hx : (hom v) x = 0
h_lt : 0 < x
⊢ False
-- Mathlib/Topology/Spectral/Hom.lean
theorem cancel_left {g : SpectralMap β γ} {f₁ f₂ : SpectralMap α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem keys_replace (a : α) (b : β a) (s : Finmap β) : (replace a b s).keys = s.keys :=
  induction_on s fun s => by simp

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ (replace a b ⟦s⟧).keys = ⟦s⟧.keys

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ioc_iff_Iic (h : a < b) :
    ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_modifyKey [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue! k' (modifyKey k f l) =
      if k == k' then
        getValue? k l |>.map f |>.get!
      else
        getValue! k' l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
hi : Inhabited β
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValue! k' (modifyKey k f l) = if (k == k') = true then (Option.map f (getValue? k l)).get! else getValue! k' l

Tactic:
simp [modifyKey_eq_alterKey, getValue!_alterKey, hl]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma toTriangle_is3Clique (hx : x ∈ t) : (graph t).IsNClique 3 (toTriangle x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 (toTriangle x)

Tactic:
simp only [toTriangle_apply, is3Clique_triple_iff, in₀₁_iff, in₀₂_iff, in₁₂_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
hx : x ∈ t
⊢ (∃ c, (x.1, x.2.1, c) ∈ t) ∧ (∃ b, (x.1, b, x.2.2) ∈ t) ∧ ∃ a, (a, x.2.1, x.2.2) ∈ t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
hx : x ∈ t
⊢ (∃ c, (x.1, x.2.1, c) ∈ t) ∧ (∃ b, (x.1, b, x.2.2) ∈ t) ∧ ∃ a, (a, x.2.1, x.2.2) ∈ t

Tactic:
exact ⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_right_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - c ≤ b

Proof state:
a b c : Int
h : a ≤ b + c
⊢ a - c ≤ b

Tactic:
have h := Int.add_le_add_right h (-c)

Result:
a b c : Int
h✝ : a ≤ b + c
h : a + -c ≤ b + c + -c
⊢ a - c ≤ b

Proof state:
a b c : Int
h✝ : a ≤ b + c
h : a + -c ≤ b + c + -c
⊢ a - c ≤ b

Tactic:
rwa [Int.add_neg_cancel_right] at h

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem think_bind (c) (f : α → Computation β) : bind (think c) f = think (bind c f) :=
  destruct_eq_think <| by simp [bind, Bind.f]

Proof state:
α : Type u
β : Type v
c : Computation α
f : α → Computation β
⊢ (c.think.bind f).destruct = Sum.inr (c.bind f)

Tactic:
simp [bind, Bind.f]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_adjoin_simple_le_finrank (α : E) (halg : IsAlgebraic F α) :
    finSepDegree F F⟮α⟯ ≤ finrank F F⟮α⟯

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : FiniteDimensional F ↥F⟮α⟯
⊢ finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯

Tactic:
exact Nat.le_of_dvd finrank_pos <| finSepDegree_adjoin_simple_dvd_finrank F E α

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯

Tactic:
haveI := adjoin.finiteDimensional halg.isIntegral

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : FiniteDimensional F ↥F⟮α⟯
⊢ finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_add_fract_le (a b : α) : fract a + fract b ≤ fract (a + b) + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ fract a + fract b ≤ fract (a + b) + 1

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋

Tactic:
exact mod_cast le_floor_add_floor a b

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem map_objAppend1 {α γ : TypeVec n} (g : α ⟹ γ) (a : P.A) (f' : P.drop.B a ⟹ α)
    (f : P.last.B a → P.W α) :
    appendFun g (P.wMap g) <$$> P.objAppend1 a f' f =
      P.objAppend1 a (g ⊚ f') fun x => P.wMap g (f x)

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ (g ::: P.wMap g) <$$> P.objAppend1 a f' f = P.objAppend1 a (g ⊚ f') fun x => P.wMap g (f x)

Tactic:
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ ⟨a, splitFun (g ⊚ f') (P.wMap g ∘ f)⟩ = ⟨a, splitFun (g ⊚ f') fun x => P.wMap g (f x)⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α γ : TypeVec.{u} n
g : α ⟹ γ
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
⊢ ⟨a, splitFun (g ⊚ f') (P.wMap g ∘ f)⟩ = ⟨a, splitFun (g ⊚ f') fun x => P.wMap g (f x)⟩

Tactic:
rfl

Result:
no goals