harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [F.LaxMonoidal] :
    (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
      (μ F m n).app X ≫ (F.map (f ⊗ g)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
this :
  ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X)) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X

Tactic:
simpa using this

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X

Tactic:
have := congr_app (μ_natural F f g) X

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
this : ((F.map f ⊗ F.map g) ≫ μ F m' n').app X = (μ F m n ≫ F.map (f ⊗ g)).app X
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
this : ((F.map f ⊗ F.map g) ≫ μ F m' n').app X = (μ F m n ≫ F.map (f ⊗ g)).app X
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X

Tactic:
dsimp at this

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
this :
  ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X)) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ g)).app X
-- Mathlib/Topology/Algebra/Algebra.lean
theorem Subalgebra.isClosed_topologicalClosure (s : Subalgebra R A) :
    IsClosed (s.topologicalClosure : Set A)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed ↑s.topologicalClosure

Tactic:
convert @isClosed_closure A s _

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSum_isBase_iff {h B} :
    (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
⊢ (M.disjointSum N h).IsBase B ↔ M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_filter (f : Π₀ i, β i) : (f.filter p).support = {x ∈ f.support | p x}

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (filter p f).support = Finset.filter (fun x => p x) f.support

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ (filter p f).support ↔ i ∈ Finset.filter (fun x => p x) f.support

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ (filter p f).support ↔ i ∈ Finset.filter (fun x => p x) f.support

Tactic:
by_cases h : p i <;> simp [h]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem intCast_lt_cast {m : ℤ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℤ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
rw [← cast_lt (K := K), cast_intCast]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
/-- We can inflate a set `s` to any bigger size. -/
lemma Finset.exists_superset_card_eq [Fintype α] {n : ℕ} {s : Finset α} (hsn : #s ≤ n)
    (hnα : n ≤ Fintype.card α) :
    ∃ t, s ⊆ t ∧ #t = n

Proof state:
α : Type u_1
inst✝ : Fintype α
n : ℕ
s : Finset α
hsn : #s ≤ n
hnα : n ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem mem_nhds_bot_iff {s : Set EReal} : s ∈ 𝓝 (⊥ : EReal) ↔ ∃ y : ℝ, Iio (y : EReal) ⊆ s :=
  nhds_bot_basis.mem_iff.trans <| by simp only [true_and]

Proof state:
s : Set EReal
⊢ (∃ i, True ∧ Iio ↑i ⊆ s) ↔ ∃ y, Iio ↑y ⊆ s

Tactic:
simp only [true_and]

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem image_coev {y : Y} (s : Set X) : coev X Y y '' s = {y} ×ˢ s

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
y : Y
s : Set X
⊢ ⇑(coev X Y y) '' s = {y} ×ˢ s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_cons_of_pos {p : α → Bool} {a : α} {l} (pa : p a) :
    filter p (a :: l) = a :: filter p l

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

Tactic:
rw [filter, pa]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_coe [AddGroupWithOne R] {f : ArithmeticFunction ℕ} :
    ((f : ArithmeticFunction ℤ) : ArithmeticFunction R) = (f : ArithmeticFunction R)

Proof state:
case h
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑f x✝ = ↑f x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
⊢ ↑↑f = ↑f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑f x✝ = ↑f x✝
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem TendstoInMeasure.exists_seq_tendstoInMeasure_atTop {u : Filter ι} [NeBot u]
    [IsCountablyGenerated u] {f : ι → α → E} {g : α → E} (hfg : TendstoInMeasure μ f u g) :
    ∃ ns : ℕ → ι, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n => f (ns n)) atTop g

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n => f (ns n)) atTop g

Tactic:
obtain ⟨ns, h_tendsto_ns⟩ : ∃ ns : ℕ → ι, Tendsto ns atTop u := exists_seq_tendsto u

Result:
case intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ ns, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n => f (ns n)) atTop g

Proof state:
case intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ns : ℕ → ι
h_tendsto_ns : Tendsto ns atTop u
⊢ ∃ ns, Tendsto ns atTop u ∧ TendstoInMeasure μ (fun n => f (ns n)) atTop g

Tactic:
exact ⟨ns, h_tendsto_ns, fun ε hε => (hfg ε hε).comp h_tendsto_ns⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_finsupp_eq_sum_left {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
    ⟪linearCombination 𝕜 v l₁, linearCombination 𝕜 v l₂⟫ = l₁.sum fun i y => conj y * l₂ i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ inner ((linearCombination 𝕜 v) l₁) ((linearCombination 𝕜 v) l₂) = l₁.sum fun i y => (starRingEnd 𝕜) y * l₂ i

Tactic:
simp only [l₁.linearCombination_apply _, Finsupp.sum_inner, hv.inner_right_finsupp, smul_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_C_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) :
    Monic (C b * p)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b * p).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ (C b * p).leadingCoeff = 1

Tactic:
nontriviality

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b * p).leadingCoeff = 1

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

Tactic:
unfold Monic

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ (C b * p).leadingCoeff = 1
-- Mathlib/CategoryTheory/Monad/Adjunction.lean
lemma comparison_full [R.Full] {L : C ⥤ D} (adj : R ⊣ L) :
    (Comonad.comparison adj).Full where
  map_surjective f := ⟨R.preimage f.f, by aesop_cat⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : R.Full
L : C ⥤ D
adj : R ⊣ L
X✝ Y✝ : D
f : (Comonad.comparison adj).obj X✝ ⟶ (Comonad.comparison adj).obj Y✝
⊢ (Comonad.comparison adj).map (R.preimage f.f) = f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
lemma of_cons (a : α) (m : Multiset α) : (FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m))) =
    @HMul.hMul _ (FreeCommRing α) (FreeCommRing α) _ (of a)
    (FreeAbelianGroup.of (Multiplicative.ofAdd m))

Proof state:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
rw [← Multiset.singleton_add, ofAdd_add,
  of, FreeAbelianGroup.of_mul_of]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_top_top : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, ⊤)

Proof state:
⊢ ContinuousAt (fun p => p.1 + p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]

Result:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 + a.2

Proof state:
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.1 ∧ ↑r < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Tactic:
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2

Result:
no goals

Proof state:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 + a.2

Tactic:
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
  (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_

Result:
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.1 ∧ ↑r < x✝.2
⊢ ↑r < x✝.1 + x✝.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem contains_push [BEq α] {l : Vector α n} {a : α} {b : α} :
    (l.push a).contains b = (l.contains b || b == a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).contains b = ({ toArray := l, size_toArray := ⋯ }.contains b || b == a)

Tactic:
simp [Array.contains_push]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
l : Vector α n
a b : α
⊢ (l.push a).contains b = (l.contains b || b == a)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.push a).contains b = ({ toArray := l, size_toArray := ⋯ }.contains b || b == a)
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive (attr := simp)]
lemma locallyLipschitzOn_inv_iff : LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f : α → E
s : Set α
⊢ LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

Tactic:
simp [LocallyLipschitzOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : take n (l₁ ++ l₂) = l₁

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ take l₁.length (l₁ ++ l₂) = l₁

Tactic:
apply take_left

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ take n (l₁ ++ l₂) = l₁

Tactic:
rw [← h]

Result:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ take l₁.length (l₁ ++ l₂) = l₁
-- Mathlib/Data/Multiset/Count.lean
theorem countP_pos {s} : 0 < countP p s ↔ ∃ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ 0 < countP p (Quot.mk (⇑(isSetoid α)) _l) ↔ ∃ a ∈ Quot.mk (⇑(isSetoid α)) _l, p a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem next_cons_cons_eq' (y z : α) (h : x ∈ y :: z :: l) (hx : x = y) :
    next (y :: z :: l) x h = z

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).next x h = z

Tactic:
rw [next, nextOr, if_pos hx]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Spanning.compl_coindep (hS : M.Spanning S) : M.Coindep (M.E \ S)

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ M.Coindep (M.E \ S)

Tactic:
rwa [← spanning_iff_compl_coindep]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_eq_self (hf : Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n :=
  ⟨fun H ↦ not_even_iff_odd.1 fun hn ↦ hne <| by rwa [hf.iterate_even hn, eq_comm] at H,
    hf.iterate_odd⟩

Proof state:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = f
hn : Even n
⊢ f = id

Tactic:
rwa [hf.iterate_even hn, eq_comm] at H

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ιMulti_zero_apply (v : Fin 0 → M) : ιMulti R 0 v = 1

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Fin 0 → M
⊢ (ιMulti R 0) v = 1

Tactic:
simp [ιMulti]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_neg_I : arg (-I) = -(π / 2)

Proof state:
⊢ (-I).arg = -(π / 2)

Tactic:
simp [arg, le_refl]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem restrict_iInf_restrict {ι} (s : Set α) (m : ι → OuterMeasure α) :
    restrict s (⨅ i, restrict s (m i)) = restrict s (⨅ i, m i) :=
  calc restrict s (⨅ i, restrict s (m i))
    _ = restrict (range ((↑) : s → α)) (⨅ i, restrict s (m i))

Proof state:
α : Type u_1
ι : Sort u_2
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨅ i, (restrict s) (m i)) = (restrict (range Subtype.val)) (⨅ i, (restrict s) (m i))

Tactic:
rw [Subtype.range_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
lemma hasFiniteIntegral_const_iff_isFiniteMeasure {c : β} (hc : c ≠ 0) :
    HasFiniteIntegral (fun _ ↦ c) μ ↔ IsFiniteMeasure μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ HasFiniteIntegral (fun x => c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [hasFiniteIntegral_const_iff, hc, isFiniteMeasure_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem mem_toCotangent_ker {x : I} : x ∈ LinearMap.ker I.toCotangent ↔ (x : R) ∈ I ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ I ^ 2

Tactic:
rw [← I.map_toCotangent_ker]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi : cos π = -1

Proof state:
⊢ ↑(-1) = -1

Tactic:
simp

Result:
no goals

Proof state:
⊢ cos ↑π = -1

Tactic:
rw [← ofReal_cos, Real.cos_pi]

Result:
⊢ ↑(-1) = -1
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_lt₃' {a' b' c' : Ordinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) :
    a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
      a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Proof state:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') +
        toNatOrdinal (b' ⨳ c' ⨳ a)) =
    toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c' ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a'))

Tactic:
abel_nf

Result:
no goals

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' < b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a

Tactic:
convert nmul_nadd_lt₃ hb hc ha using 1 <;>
  (simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]; abel_nf)

Result:
no goals

Proof state:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a = b ⨳ c ⨳ a ♯ b' ⨳ c' ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a'

Tactic:
simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]

Result:
case h.e'_4
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a') +
        toNatOrdinal (b' ⨳ c' ⨳ a)) =
    toOrdinal
      (toNatOrdinal (b ⨳ c ⨳ a) + toNatOrdinal (b' ⨳ c' ⨳ a) + toNatOrdinal (b' ⨳ c ⨳ a') + toNatOrdinal (b ⨳ c' ⨳ a'))

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') <
    a ⨳ (b ⨳ c) ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')

Tactic:
simp only [nmul_comm _ (_ ⨳ _)]

Result:
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ b ⨳ c ⨳ a' ♯ b' ⨳ c ⨳ a ♯ b ⨳ c' ⨳ a ♯ b' ⨳ c' ⨳ a' < b ⨳ c ⨳ a ♯ b' ⨳ c ⨳ a' ♯ b ⨳ c' ⨳ a' ♯ b' ⨳ c' ⨳ a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Bitwise/Lemmas.lean
theorem shiftRight_zero (n : Int) : n >>> 0 = n

Proof state:
n : Int
⊢ n >>> 0 = n

Tactic:
simp [Int.shiftRight_eq_div_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem out [NormedSpace ℂ E] (hf : CircleIntegrable f c R) :
    IntervalIntegrable (fun θ : ℝ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0
      (2 * π)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume

Tactic:
refine (hf.norm.const_mul |R|).mono' ?_ ?_

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ AEStronglyMeasurable (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ι 0 (2 * π)), ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ AEStronglyMeasurable (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))

Tactic:
exact ((continuous_circleMap _ _).aestronglyMeasurable.mul_const I).smul hf.aestronglyMeasurable

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : CircleIntegrable f c R
⊢ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
simp only [CircleIntegrable, deriv_circleMap, intervalIntegrable_iff] at *

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ι 0 (2 * π)), ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖

Tactic:
simp [norm_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • A⁻¹ *ᵥ b = cramer A b

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • A⁻¹ *ᵥ b = A.cramer b

Tactic:
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul,
  h.mul_val_inv, one_smul]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem bind_decode₂_iff {f : α →. σ} :
    Partrec f ↔ Nat.Partrec fun n => Part.bind (decode₂ α n) fun a => (f a).map encode :=
  ⟨fun hf =>
    nat_iff.1 <|
      (Computable.ofOption Primrec.decode₂.to_comp).bind <|
        (map hf (Computable.encode.comp snd).to₂).comp snd,
    fun h =>
    map_encode_iff.1 <| by simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)⟩

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
h : Nat.Partrec fun n => (↑(decode₂ α n)).bind fun a => Part.map encode (f a)
⊢ Partrec fun a => Part.map encode (f a)

Tactic:
simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Idempotent.lean
lemma eq_of_mul_eq_add_eq_one [Semiring α] (a : α) {b c : α}
    (mul : a * b = c * a) (add_ab : a + b = 1) (add_ac : a + c = 1) :
    b = c :=
  calc b = (a + c) * b

Proof state:
α : Type u_1
inst✝ : Semiring α
a b c : α
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ c * (a + b) = c

Tactic:
rw [add_ab, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
a b c : α
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ (a + c) * b = c * (a + b)

Tactic:
rw [add_mul, mul, mul_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
a b c : α
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ b = (a + c) * b

Tactic:
rw [add_ac, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Int.lean
lemma add_two_le_iff_lt_of_even_sub {m n : ℤ} (even : Even (n - m)) : m + 2 ≤ n ↔ m < n

Proof state:
m n : ℤ
even : Even (n - m)
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
m n : ℤ
even : Even (n - m)
⊢ m + 2 ≤ n ↔ m < n

Tactic:
rw [add_comm]

Result:
m n : ℤ
even : Even (n - m)
⊢ 2 + m ≤ n ↔ m < n

Proof state:
m n : ℤ
even : Even (n - m)
⊢ 2 + m ≤ n ↔ m < n

Tactic:
exact le_add_iff_lt_of_dvd_sub (by decide) even.two_dvd

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem Algebra.isIntegral_sup {S T : Subalgebra R A} :
    Algebra.IsIntegral R (S ⊔ T : Subalgebra R A) ↔
      Algebra.IsIntegral R S ∧ Algebra.IsIntegral R T

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T

Tactic:
simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]

Result:
no goals