harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerRight_naturality_comp (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
    (η.naturality (f ≫ g)).hom ▷ h ≫ (α_ _ _ _).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
      F.mapComp f g ▷ η.app c ▷ h ≫
        (α_ _ _ _).hom ▷ h ≫
          (α_ _ _ _).hom ≫
            F.map f ◁ (η.naturality g).hom ▷ h ≫
              (α_ _ _ _).inv ≫
                (α_ _ _ _).inv ▷ h ≫
                 (η.naturality f).hom ▷ G.map g ▷ h ≫ (α_ _ _ _).hom ▷ h ≫ (α_ _ _ _).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η : StrongOplaxNatTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ (η.naturality (f ≫ g)).hom ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ (η.naturality g).hom ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                (η.naturality f).hom ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom

Tactic:
apply η.toOplax.whiskerRight_naturality_comp

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Hom.lean
theorem SemiconjBy.of_map [MulHomClass F M N] (f : F) (hf : Function.Injective f)
    (h : SemiconjBy (f a) (f x) (f y)) : SemiconjBy a x y :=
  hf (by simpa only [SemiconjBy, map_mul] using h)

Proof state:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : SemiconjBy (f a) (f x) (f y)
⊢ f (a * x) = f (y * a)

Tactic:
simpa only [SemiconjBy, map_mul] using h

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem Equiv.Perm.ofFn_comp_perm {n : ℕ} {α : Type u} (σ : Equiv.Perm (Fin n)) (f : Fin n → α) :
    ofFn (f ∘ σ) ~ ofFn f

Proof state:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)

Tactic:
exact σ.map_finRange_perm.map f

Result:
no goals

Proof state:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ⇑σ) ~ ofFn f

Tactic:
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]

Result:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_flatMap {α β} (f : α → β) (l : List α) : map f l = l.flatMap fun x => [f x]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = flatMap (fun x => [f x]) l

Tactic:
simp only [← map_singleton]

Result:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = flatMap (fun x => map f [x]) l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = flatMap (fun x => map f [x]) l

Tactic:
rw [← flatMap_singleton' l, map_flatMap, flatMap_singleton']

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem prod_rightInvSeq (ω : List B) : prod (ris ω) = (π ω)⁻¹

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
induction' ω with i ω ih

Result:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹

case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
⊢ (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹

Proof state:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ (cs.rightInvSeq []).prod = (cs.wordProd [])⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
⊢ (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹

Tactic:
simp [rightInvSeq, ih, wordProd_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} (h : m.WF) :
    Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
fallback : β
f : β → β
h : m.WF
⊢ getD (modify m k f) k fallback = (Option.map f (get? m k)).getD fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_modify_self

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem toCharTwoJNeZeroNF_spec (ha₁ : W.a₁ ≠ 0) :
    (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).IsCharTwoJNeZeroNF

Proof state:
case a₁
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₁ = 1

Tactic:
simp [toCharTwoJNeZeroNF, ha₁]

Result:
no goals

Proof state:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ ((W.a₄ * W.a₁ + 2 * W.a₃ * W.a₂) * W.a₁ ^ 3 - W.a₁ * ((W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * W.a₁)) * W.a₁ ^ 2 +
      3 * W.a₃ ^ 2 * (W.a₁ * W.a₁ ^ 3) =
    0

Tactic:
linear_combination (W.a₁ ^ 4 * W.a₃ ^ 2 + W.a₁ ^ 5 * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).IsCharTwoJNeZeroNF

Tactic:
constructor

Result:
case a₁
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₁ = 1

case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₃ = 0

case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₄ = 0

Proof state:
case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.a₃ + W.a₃) * W.a₁ ^ 3 + 2 * (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) = 0

Tactic:
linear_combination (W.a₃ * W.a₁ ^ 3 + W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * CharP.cast_eq_zero F 2

Result:
no goals

Proof state:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₄ = 0

Tactic:
field_simp [toCharTwoJNeZeroNF]

Result:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ ((W.a₄ * W.a₁ + 2 * W.a₃ * W.a₂) * W.a₁ ^ 3 - W.a₁ * ((W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * W.a₁)) * W.a₁ ^ 2 +
      3 * W.a₃ ^ 2 * (W.a₁ * W.a₁ ^ 3) =
    0

Proof state:
case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).a₃ = 0

Tactic:
field_simp [toCharTwoJNeZeroNF]

Result:
case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.a₃ + W.a₃) * W.a₁ ^ 3 + 2 * (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) = 0
-- Mathlib/Data/Option/Basic.lean
theorem bind_eq_some' {x : Option α} {f : α → Option β} {b : β} :
    x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Proof state:
α : Type u_1
β : Type u_2
x : Option α
f : α → Option β
b : β
⊢ x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem valAux_one : valAux K v O p 1 = 1 :=
  (valAux_eq (hv := hv) <| show coeff (ModP O p) p 0 1 ≠ 0 from one_ne_zero).trans <| by
    rw [pow_zero, pow_one, RingHom.map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk hv,
      RingHom.map_one, v.map_one]
    change (1 : ModP O p) ≠ 0
    exact one_ne_zero

Proof state:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0

Tactic:
change (1 : ModP O p) ≠ 0

Result:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ 1 ≠ 0

Proof state:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ ModP.preVal K v O p ((coeff (ModP O p) p 0) 1) ^ p ^ 0 = 1

Tactic:
rw [pow_zero, pow_one, RingHom.map_one, ← (Ideal.Quotient.mk _).map_one, ModP.preVal_mk hv,
  RingHom.map_one, v.map_one]

Result:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_left_inj (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b

Tactic:
simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem apply_dualBasis_left (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (i j) :
    B (B.dualBasis hB b i) (b j) = if j = i then 1 else 0

Proof state:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0

Tactic:
rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
  LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
⊢ (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0

Tactic:
have := FiniteDimensional.of_fintype_basis b

Result:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
b : Basis ι K V
i j : ι
this : FiniteDimensional K V
⊢ (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem?_unattach {p : α → Prop} {l : List { x // p x }} (i : Nat) :
    l.unattach[i]? = l[i]?.map Subtype.val

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
i : Nat
⊢ l.unattach[i]? = Option.map Subtype.val l[i]?

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_relabel (f : α → β) (g : β → γ) (t : L.Term α) :
    (t.relabel f).relabel g = t.relabel (g ∘ f)

Proof state:
case func
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), relabel g (relabel f (_ts✝ a)) = relabel (g ∘ f) (_ts✝ a)
⊢ relabel g (relabel f (func _f✝ _ts✝)) = relabel (g ∘ f) (func _f✝ _ts✝)

Tactic:
simp [ih]

Result:
no goals

Proof state:
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
t : L.Term α
⊢ relabel g (relabel f t) = relabel (g ∘ f) t

Tactic:
induction t with
| var => rfl
| func _ _ ih => simp [ih]

Result:
no goals

Proof state:
case var
L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
a✝ : α
⊢ relabel g (relabel f (var a✝)) = relabel (g ∘ f) (var a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma biSup_add' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℕ∞) :
    (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a

Proof state:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
⊢ (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a

Tactic:
simp only [add_comm, add_biSup' h]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem divp_mul_eq_mul_divp (x y : α) (u : αˣ) : x /ₚ u * y = x * y /ₚ u

Proof state:
α : Type u
inst✝ : CommMonoid α
x y : α
u : αˣ
⊢ x /ₚ u * y = x * y /ₚ u

Tactic:
rw [divp, divp, mul_right_comm]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_union_left : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
simp only [disjoint_left, mem_union, or_imp, forall_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem not_mem_of_not_mem_push {a b : α} {l : Array α} (h : a ∉ l.push b) : a ∉ l

Proof state:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l.push b
⊢ ¬a ∈ l

Tactic:
simp only [mem_push, not_or] at h

Result:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l ∧ ¬a = b
⊢ ¬a ∈ l

Proof state:
α : Type u_1
a b : α
l : Array α
h : ¬a ∈ l ∧ ¬a = b
⊢ ¬a ∈ l

Tactic:
exact h.1

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_one_nat_atTop_iff {f : ℕ → E''} :
    f =O[atTop] (fun _n => 1 : ℕ → ℝ) ↔ ∃ C, ∀ n, ‖f n‖ ≤ C :=
  Iff.trans (isBigO_nat_atTop_iff fun _ h => (one_ne_zero h).elim) <| by
    simp only [norm_one, mul_one]

Proof state:
E'' : Type u_9
inst✝ : NormedAddCommGroup E''
f : ℕ → E''
⊢ (∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖1‖) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
simp only [norm_one, mul_one]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_le_powerset (n : ℕ) (s : Multiset α) : powersetCard n s ≤ powerset s :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]
    exact ((sublistsLen_sublist_sublists' _ _).map _).subperm

Proof state:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ powersetCard n ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]

Result:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'

Proof state:
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList l.sublists'

Tactic:
exact ((sublistsLen_sublist_sublists' _ _).map _).subperm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_filter (f : α → Bool) (l : Array α) :
    (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x))

Proof state:
α : Type u_1
p f : α → Bool
l : Array α
⊢ (filter f l).eraseP p = filter f (l.eraseP fun x => p x && f x)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p f : α → Bool
l : List α
⊢ (filter f { toList := l }).eraseP p = filter f ({ toList := l }.eraseP fun x => p x && f x)

Proof state:
case mk
α : Type u_1
p f : α → Bool
l : List α
⊢ (filter f { toList := l }).eraseP p = filter f ({ toList := l }.eraseP fun x => p x && f x)

Tactic:
simpa using List.eraseP_filter f l

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n

Proof state:
m n : Nat
H : n % m = 0
⊢ m ∣ n

Tactic:
exists n / m

Result:
m n : Nat
H : n % m = 0
⊢ n = m * (n / m)

Proof state:
m n : Nat
H : n % m = 0
⊢ n = m * (n / m)

Tactic:
have := (mod_add_div n m).symm

Result:
m n : Nat
H : n % m = 0
this : n = n % m + m * (n / m)
⊢ n = m * (n / m)

Proof state:
m n : Nat
H : n % m = 0
this : n = n % m + m * (n / m)
⊢ n = m * (n / m)

Tactic:
rwa [H, Nat.zero_add] at this

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[reassoc (attr := simp)]
lemma ιFunctorObj_πFunctorObj : ιFunctorObj f πX ≫ πFunctorObj f πX = πX

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
⊢ ιFunctorObj f πX ≫ πFunctorObj f πX = πX

Tactic:
simp [ιFunctorObj, πFunctorObj]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem iter_deriv_exp : ∀ n : ℕ, deriv^[n] exp = exp
  | 0 => rfl
  | n + 1 => by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Proof state:
n : ℕ
⊢ deriv^[n + 1] cexp = cexp

Tactic:
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem triangle_assoc_comp_right_inv (X Y : C) :
    (ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv

Tactic:
simp [← cancel_mono (X ◁ (λ_ Y).hom)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y)

Proof state:
⊢ ∀ (x y z : Bool), (x && y && z) = (x && z && y)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_conj (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : x ^ conj n = conj (conj x ^ n)

Proof state:
x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) x ^ n)

Tactic:
rw [conj_cpow _ _ hx, conj_conj]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem annihilator_span (s : Set M) :
    (Submodule.span R s).annihilator = ⨅ g : s, ker (toSpanSingleton R M g.1)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).annihilator = ⨅ g, ker (toSpanSingleton R M ↑g)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, ker (toSpanSingleton R M ↑g)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, ker (toSpanSingleton R M ↑g)

Tactic:
simp [mem_annihilator_span]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Basic.lean
theorem IsSquare.nonneg [Semiring R] [LinearOrder R] [IsRightCancelAdd R]
    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R]
    {x : R} (h : IsSquare x) : 0 ≤ x

Proof state:
case intro
R : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsRightCancelAdd R
inst✝³ : ZeroLEOneClass R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftStrictMono R
y : R
⊢ 0 ≤ y * y

Tactic:
exact mul_self_nonneg y

Result:
no goals

Proof state:
R : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsRightCancelAdd R
inst✝³ : ZeroLEOneClass R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftStrictMono R
x : R
h : IsSquare x
⊢ 0 ≤ x

Tactic:
rcases h with ⟨y, rfl⟩

Result:
case intro
R : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsRightCancelAdd R
inst✝³ : ZeroLEOneClass R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftStrictMono R
y : R
⊢ 0 ≤ y * y
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_add_const_Ioc : (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem multiset_prod_X_sub_C_nextCoeff (t : Multiset R) :
    nextCoeff (t.map fun x => X - C x).prod = -t.sum

Proof state:
case h
R : Type u
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ (X - C i✝).Monic

Tactic:
apply monic_X_sub_C

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i => (X - C i).nextCoeff) t).sum = -t.sum

Tactic:
simp only [nextCoeff_X_sub_C]

Result:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x => -x) t).sum = -t.sum

Proof state:
case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic

Tactic:
intros

Result:
case h
R : Type u
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ (X - C i✝).Monic

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x => -x) t).sum = -t.sum

Tactic:
exact t.sum_hom (-AddMonoidHom.id R)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun x => X - C x) t).prod.nextCoeff = -t.sum

Tactic:
rw [nextCoeff_multiset_prod]

Result:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i => (X - C i).nextCoeff) t).sum = -t.sum

case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.rotateL_lemma₁ {a b c : ℕ} (H2 : 3 * a ≤ b + c) (hb₂ : c ≤ 3 * b) : a ≤ 3 * b

Proof state:
a b c : ℕ
H2 : 3 * a ≤ b + c
hb₂ : c ≤ 3 * b
⊢ a ≤ 3 * b

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma opProdIsoCoprod_inv_inr : (opProdIsoCoprod A B).inv.unop ≫ coprod.inr.unop = prod.snd

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).inv.unop ≫ coprod.inr.unop = prod.snd

Tactic:
rw [← unop_comp, inr_opProdIsoCoprod_inv, Quiver.Hom.unop_op]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem trans_eq_refl_iff_eq_symm {f : α ≃ β} {g : β ≃ α} :
    f.trans g = Equiv.refl α ↔ f = g.symm

Proof state:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f = g.symm

Tactic:
rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

Result:
no goals
-- Mathlib/Algebra/Star/CHSH.lean
theorem sqrt_two_inv_mul_self : (√2)⁻¹ * (√2)⁻¹ = (2⁻¹ : ℝ)

Proof state:
⊢ (√2)⁻¹ * (√2)⁻¹ = 2⁻¹

Tactic:
rw [← mul_inv]

Result:
⊢ (√2 * √2)⁻¹ = 2⁻¹

Proof state:
⊢ (√2 * √2)⁻¹ = 2⁻¹

Tactic:
norm_num

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
lemma commShift_of_functor [E.functor.CommShift A] :
    letI := E.commShiftInverse A
    E.CommShift A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.functor.CommShift A
⊢ E.CommShift A

Tactic:
letI := E.commShiftInverse A

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.functor.CommShift A
this : E.inverse.CommShift A := E.commShiftInverse A
⊢ E.CommShift A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.functor.CommShift A
this : E.inverse.CommShift A := E.commShiftInverse A
⊢ E.CommShift A

Tactic:
exact CommShift.mk' _ _ (E.toAdjunction.commShift_of_leftAdjoint A).commShift_unit

Result:
no goals