harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpIndSMul_nonneg {E} [NormedLatticeAddCommGroup E] [NormedSpace ℝ E] [OrderedSMul ℝ E]
    [SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) (hx : 0 ≤ x) :
    (0 : α → E) ≤ᵐ[μ] condExpIndSMul hm hs hμs x

Proof state:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderedSMul ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
a : α
ha : 0 a ≤ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a
⊢ 0 a ≤ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x

Tactic:
exact smul_nonneg ha hx

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderedSMul ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ 0 ≤ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)

Tactic:
refine EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderedSMul ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ 0 ≤ᶠ[ae μ] fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderedSMul ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
⊢ 0 ≤ᶠ[ae μ] fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x

Tactic:
filter_upwards [condExpL2_indicator_nonneg hm hs hμs] with a ha

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : OrderedSMul ℝ E
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
hx : 0 ≤ x
a : α
ha : 0 a ≤ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a
⊢ 0 a ≤ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x
-- Mathlib/Data/Int/GCD.lean
theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = natAbs i * gcd j k

Proof state:
i j k : ℤ
⊢ (i.natAbs * j.natAbs).gcd (i.natAbs * k.natAbs) = i.natAbs * j.natAbs.gcd k.natAbs

Tactic:
apply Nat.gcd_mul_left

Result:
no goals

Proof state:
i j k : ℤ
⊢ (i * j).gcd (i * k) = i.natAbs * j.gcd k

Tactic:
rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]

Result:
i j k : ℤ
⊢ (i.natAbs * j.natAbs).gcd (i.natAbs * k.natAbs) = i.natAbs * j.natAbs.gcd k.natAbs
-- Mathlib/RingTheory/Adjoin/Field.lean
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `[E[L] : E] ≤ [L : F]`. -/
lemma Subalgebra.adjoin_rank_le {F : Type*} (E : Type*) {K : Type*}
    [CommRing F] [StrongRankCondition F] [CommRing E] [StrongRankCondition E] [Ring K]
    [SMul F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K]
    (L : Subalgebra F K) [Module.Free F L] :
    Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L

Proof state:
F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommRing F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommRing E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Ring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Submodule.span E (Set.range fun i => ↑((Module.Free.chooseBasis F ↥L) i))) ≤
    Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)

Tactic:
exact rank_span_le _ |>.trans Cardinal.mk_range_le

Result:
no goals

Proof state:
F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommRing F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommRing E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Ring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
  L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]

Result:
F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommRing F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommRing E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Ring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Submodule.span E (Set.range fun i => ↑((Module.Free.chooseBasis F ↥L) i))) ≤
    Cardinal.mk (Module.Free.ChooseBasisIndex F ↥L)
-- Mathlib/GroupTheory/Index.lean
theorem index_map_of_injective {f : G →* G'} (hf : Function.Injective f) :
    (H.map f).index = H.index * f.range.index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Function.Injective ⇑f
⊢ (map f H).index = H.index * f.range.index

Tactic:
rw [H.index_map, f.ker_eq_bot_iff.mpr hf, sup_bot_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Pairwise.lean
theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
    l' = map (get l) is ∧ is.Pairwise (· < ·)

Proof state:
α✝ : Type u_1
l' l : List α✝
h : l' <+ l
⊢ ∃ is, l' = map l.get is ∧ Pairwise (fun x1 x2 => x1 < x2) is

Tactic:
simpa using sublist_eq_map_getElem h

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
lemma commShift_of_inverse [E.inverse.CommShift A] :
    letI := E.commShiftFunctor A
    E.CommShift A

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

Tactic:
exact inferInstanceAs (E.symm.symm.CommShift A)

Result:
no goals

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

Tactic:
letI := E.commShiftFunctor A

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

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

Tactic:
have := E.symm.commShift_of_functor A

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.inverse.CommShift A
this✝ : E.functor.CommShift A := E.commShiftFunctor A
this : E.symm.CommShift A
⊢ E.CommShift A
-- Mathlib/Data/Finset/Basic.lean
lemma Nontrivial.exists_cons_eq {s : Finset α} (hs : s.Nontrivial) :
    ∃ t a ha b hb hab, (cons b t hb).cons a (mem_cons.not.2 <| not_or_intro hab ha) = s

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩

Result:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Proof state:
α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
classical
obtain ⟨a, ha, b, hb, hab⟩ := hs
have : b ∈ s.erase a := mem_erase.2 ⟨hab.symm, hb⟩
refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;>
  simp [insert_erase this, insert_erase ha, *]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;>
  simp [insert_erase this, insert_erase ha, *]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := hs

Result:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem bot_ext (x y : (⊥ : Submodule R M)) : x = y

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : ↥⊥
⊢ x = y

Tactic:
rcases x with ⟨x, xm⟩

Result:
case mk
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : ↥⊥
x : M
xm : x ∈ ⊥
⊢ ⟨x, xm⟩ = y

Proof state:
case mk.mk.e_val
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ x = y

Tactic:
rw [(Submodule.eq_bot_iff _).mp rfl x xm]

Result:
case mk.mk.e_val
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ 0 = y

Proof state:
case mk.mk.e_val
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ 0 = y

Tactic:
rw [(Submodule.eq_bot_iff _).mp rfl y ym]

Result:
no goals

Proof state:
case mk.mk
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ ⟨x, xm⟩ = ⟨y, ym⟩

Tactic:
congr

Result:
case mk.mk.e_val
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ x = y

Proof state:
case mk
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : ↥⊥
x : M
xm : x ∈ ⊥
⊢ ⟨x, xm⟩ = y

Tactic:
rcases y with ⟨y, ym⟩

Result:
case mk.mk
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ ⟨x, xm⟩ = ⟨y, ym⟩
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem succ_pred_iff_is_succ {o} : succ (pred o) = o ↔ ∃ a, o = succ a :=
  ⟨fun e => ⟨_, e.symm⟩, fun ⟨a, e⟩ => by simp only [e, pred_succ]⟩

Proof state:
o : Ordinal.{u_4}
x✝ : ∃ a, o = succ a
a : Ordinal.{u_4}
e : o = succ a
⊢ succ o.pred = o

Tactic:
simp only [e, pred_succ]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homEquiv_refl (f : L₁.obj X ⟶ L₁.obj Y) :
    homEquiv W L₁ L₁ f = f

Proof state:
C : Type u_1
D₁ : Type u_5
inst✝² : Category.{u_9, u_1} C
inst✝¹ : Category.{u_8, u_5} D₁
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝ : L₁.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₁ L₁) f = f

Tactic:
apply LocalizerMorphism.id_homMap

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem pow_smul_le_pow_smul (i j k : ℕ) : I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
exact smul_mono_right _ (F.pow_smul_le i j)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)

Tactic:
rw [add_comm, pow_add, mul_smul]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
i j k : ℕ
⊢ I ^ k • I ^ i • F.N j ≤ I ^ k • F.N (i + j)
-- Mathlib/Data/Set/NAry.lean
lemma image2_inter_left (hf : Injective2 f) :
    image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
⊢ image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t

Tactic:
simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
    Bounded r (s ∩ { b | ¬r b a }) ↔ Bounded r s

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) ↔ Bounded r s

Tactic:
refine ⟨?_, Bounded.mono inter_subset_left⟩

Result:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) → Bounded r s

Proof state:
case intro
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ b_1 ∈ s ∩ {b | ¬r b a}, r b_1 b
⊢ Bounded r s

Tactic:
obtain ⟨m, hm⟩ := H a b

Result:
case intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ b_1 ∈ s ∩ {b | ¬r b a}, r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b | ¬r b a}) → Bounded r s

Tactic:
rintro ⟨b, hb⟩

Result:
case intro
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ b_1 ∈ s ∩ {b | ¬r b a}, r b_1 b
⊢ Bounded r s

Proof state:
case intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ b_1 ∈ s ∩ {b | ¬r b a}, r b_1 b
m : α
hm : ∀ (c : α), r c a ∨ r c b → r c m
⊢ Bounded r s

Tactic:
exact ⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_zero_left (a) : deriv 0 a = a

Proof state:
a : Ordinal.{u_1}
⊢ deriv 0 a = a

Tactic:
rw [deriv_zero, id_eq]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
@[simp]
lemma primesBelow_zero : primesBelow 0 = ∅

Proof state:
⊢ primesBelow 0 = ∅

Tactic:
rw [primesBelow, Finset.range_zero, Finset.filter_empty]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma map_op_mul (s t : Finset α) :
    (s * t).map opEquiv.toEmbedding = t.map opEquiv.toEmbedding * s.map opEquiv.toEmbedding

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ map opEquiv.toEmbedding (s * t) = map opEquiv.toEmbedding t * map opEquiv.toEmbedding s

Tactic:
simp [map_eq_image, image_op_mul]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma Args.numeric_P24 {x₁ x₂ y} :
    (Args.P24 x₁ x₂ y).Numeric ↔ x₁.Numeric ∧ x₂.Numeric ∧ y.Numeric

Proof state:
x₁ x₂ y : PGame
⊢ (P24 x₁ x₂ y).Numeric ↔ x₁.Numeric ∧ x₂.Numeric ∧ y.Numeric

Tactic:
simp [Args.Numeric, Args.toMultiset]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_comp {F : Type*} [CommRing S] [FunLike F N S] [AddMonoidHomClass F N S]
    (f : M → N) (g : F) (x y : M) :
    polar (g ∘ f) x y = g (polar f x y)

Proof state:
S : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
F : Type u_8
inst✝² : CommRing S
inst✝¹ : FunLike F N S
inst✝ : AddMonoidHomClass F N S
f : M → N
g : F
x y : M
⊢ polar (⇑g ∘ f) x y = g (polar f x y)

Tactic:
simp only [polar, Pi.smul_apply, Function.comp_apply, map_sub]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_apply_right (a b : α) : swap a b b = a

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a b : α
⊢ (swap a b) b = a

Tactic:
by_cases h : b = a <;> simp [swap_apply_def, h]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem map_map (g : β → γ) (f : α → β) (o : Part α) : map g (map f o) = map (g ∘ f) o

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o

Tactic:
erw [← bind_some_eq_map, bind_map, bind_some_eq_map]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
lemma ThreeGPFree.smul_set₀ (hs : ThreeGPFree s) (ha : a ≠ 0) : ThreeGPFree (a • s)

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
⊢ ThreeGPFree (a • s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩ h

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => a • x) b * (fun x => a • x) d = (fun x => a • x) c * (fun x => a • x) c
⊢ (fun x => a • x) b = (fun x => a • x) c

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
hs : ThreeGPFree s
ha : a ≠ 0
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => a • x) b * (fun x => a • x) d = (fun x => a • x) c * (fun x => a • x) c
⊢ b * d = c * c

Tactic:
simpa [mul_mul_mul_comm _ _ a, ha] using h

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncLE.lean
lemma truncLE'_d_eq_toCycles {i j : ι} (hij : c.Rel i j) {i' j' : ι'}
    (hi' : e.f i = i') (hj' : e.f j = j') (hj : e.BoundaryLE j) :
    (K.truncLE' e).d i j = (K.truncLE'XIso e hi' (e.not_boundaryLE_prev hij)).hom ≫
      K.toCycles i' j' ≫ (K.truncLE'XIsoCycles e hj' hj).inv :=
  Quiver.Hom.op_inj (by
    simpa [truncLE', truncLE'XIso, truncLE'XIsoCycles]
      using K.op.truncGE'_d_eq_fromOpcycles e.op hij hj' hi' (by simpa))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op = ((K.truncLE'XIso e hi' ⋯).hom ≫ K.toCycles i' j' ≫ (K.truncLE'XIsoCycles e hj' hj).inv).op

Tactic:
simpa [truncLE', truncLE'XIso, truncLE'XIsoCycles]
  using K.op.truncGE'_d_eq_fromOpcycles e.op hij hj' hi' (by simpa)

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ e.op.BoundaryGE j

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_two : sin (π / 2) = 1 :=
  calc
    sin (π / 2) = Real.sin (π / 2)

Proof state:
⊢ sin (↑π / 2) = sin ↑(π / 2)

Tactic:
simp

Result:
no goals

Proof state:
⊢ ↑(Real.sin (π / 2)) = 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ sin (↑π / 2) = ↑(Real.sin (π / 2))

Tactic:
rw [ofReal_sin]

Result:
⊢ sin (↑π / 2) = sin ↑(π / 2)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem sat_and {x y : BVLogicalExpr} {assign} (hx : Sat x assign) (hy : Sat y assign) :
    Sat (.gate .and x y) assign

Proof state:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : x.Sat assign
hy : y.Sat assign
⊢ Sat (BoolExpr.gate Gate.and x y) assign

Tactic:
simp only [Sat] at *

Result:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true

Proof state:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true

Tactic:
simp [hx, hy, Gate.eval]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_eq_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈ l, P a} :
    l.attachWith P H = #[] ↔ l = #[]

Proof state:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ { toList := toList✝ }.attachWith P H = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
P : α → Prop
H : ∀ (a : α), a ∈ l → P a
⊢ l.attachWith P H = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ { toList := toList✝ }.attachWith P H = #[] ↔ { toList := toList✝ } = #[]
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem isUnit_iff_exists_inv' [CommMonoid M] {a : M} : IsUnit a ↔ ∃ b, b * a = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsUnit a ↔ ∃ b, b * a = 1

Tactic:
simp [isUnit_iff_exists_inv, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem decomposition.decompose'_eq :
    decomposition.decompose' = fun φ : MvPolynomial σ R =>
      DirectSum.mk (fun i : ℕ => ↥(homogeneousSubmodule σ R i)) (φ.support.image Finsupp.degree)
        fun m => ⟨homogeneousComponent m φ, homogeneousComponent_mem m φ⟩

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image degree φ.support)) fun m =>
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑(weight fun x => 1)) φ.support)) fun m =>
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑(weight fun x => 1)) φ.support)) fun m =>
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Category/Frm.lean
lemma inv_hom_apply {X Y : Frm} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

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

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma deleteEdges_empty : G.deleteEdges ∅ = G

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.deleteEdges ∅ = G

Tactic:
simp [deleteEdges]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem closedBall_one_div_singleton : closedBall 1 δ / {x} = closedBall x⁻¹ δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall 1 δ / {x} = closedBall x⁻¹ δ

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_coe_mul_coe (f g : R[X]) : derivativeFun (f * g : R⟦X⟧) =
    f * derivative g + g * derivative f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (↑f * ↑g).derivativeFun = ↑f * ↑(derivative g) + ↑g * ↑(derivative f)

Tactic:
rw [← coe_mul, derivativeFun_coe, derivative_mul,
  add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]

Result:
no goals