harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma ruzsaSzemerediNumber_spec :
    ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
      #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ #(⊥.cliqueFinset 3) = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∃ G x, #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear

Tactic:
classical
exact @Nat.findGreatest_spec _
  (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) _ _ (Nat.zero_le _)
  ⟨⊥, inferInstance, by simp, locallyLinear_bot⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∃ G x, #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear

Tactic:
exact @Nat.findGreatest_spec _
  (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj),
    #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) _ _ (Nat.zero_le _)
  ⟨⊥, inferInstance, by simp, locallyLinear_bot⟩

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem contsAux_stable_step_of_terminated (terminatedAt_n : g.TerminatedAt n) :
    g.contsAux (n + 2) = g.contsAux (n + 1)

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
rw [terminatedAt_iff_s_none] at terminatedAt_n

Result:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
simp only [contsAux, Nat.add_eq, Nat.add_zero, terminatedAt_n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
    (x.bind f).bind g = x.bind fun y => (f y).bind g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Option α
f : α → Option β
g : β → Option γ
⊢ (x.bind f).bind g = x.bind fun y => (f y).bind g

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permutation.lean
@[simp]
lemma transpose_permMatrix [Zero R] [One R] : (σ.permMatrix R).transpose = (σ⁻¹).permMatrix R

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Zero R
inst✝ : One R
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹

Tactic:
rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem add_oreDiv {r r' : X} {s : S} : r /ₒ s + r' /ₒ s = (r + r') /ₒ s

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s : ↥S
⊢ r /ₒ s + r' /ₒ s = (r + r') /ₒ s

Tactic:
simp [oreDiv_add_char s s 1 1 (by simp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Conj.lean
theorem map_conjAut (F : C ⥤ D) {X Y : C} (α : X ≅ Y) (f : Aut X) :
    F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom

Tactic:
simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)

Tactic:
ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_eq_zero_iff {ι : Type u} {f : ι → Ordinal.{max u v}} :
    sup.{_, v} f = 0 ↔ ∀ i, f i = 0

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ sup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
refine
  ⟨fun h i => ?_, fun h =>
    le_antisymm (sup_le fun i => Ordinal.le_zero.2 (h i)) (Ordinal.zero_le _)⟩

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = 0
i : ι
⊢ f i = 0

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = 0
i : ι
⊢ f i = 0

Tactic:
rw [← Ordinal.le_zero, ← h]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = 0
i : ι
⊢ f i ≤ sup f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
h : sup f = 0
i : ι
⊢ f i ≤ sup f

Tactic:
exact le_sup f i

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- A multiplicative ring norm satisfies `f n ≤ n` for every `n : ℕ`. -/
@[deprecated "Use AbsoluteValue.apply_nat_le_self instead" (since := "2025-01-07")]
lemma MulRingNorm_nat_le_nat {R : Type*} [Ring R] (n : ℕ) (f : MulRingNorm R) : f n ≤ n

Proof state:
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
n : ℕ
hn : f ↑n ≤ ↑n
⊢ f ↑n + f 1 = f ↑n + 1

Tactic:
rw [map_one]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
n : ℕ
f : MulRingNorm R
⊢ f ↑n ≤ ↑n

Tactic:
induction n with
| zero => simp only [Nat.cast_zero, map_zero, le_refl]
| succ n hn =>
  simp only [Nat.cast_succ]
  calc
    f (n + 1) ≤ f (n) + f 1 := f.add_le' ↑n 1
    _ = f (n) + 1 := by rw [map_one]
    _ ≤ n + 1 := add_le_add_right hn 1

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
⊢ f ↑0 ≤ ↑0

Tactic:
simp only [Nat.cast_zero, map_zero, le_refl]

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
n : ℕ
hn : f ↑n ≤ ↑n
⊢ f ↑(n + 1) ≤ ↑(n + 1)

Tactic:
simp only [Nat.cast_succ]

Result:
case succ
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
n : ℕ
hn : f ↑n ≤ ↑n
⊢ f (↑n + 1) ≤ ↑n + 1

Proof state:
case succ
R : Type u_2
inst✝ : Ring R
f : MulRingNorm R
n : ℕ
hn : f ↑n ≤ ↑n
⊢ f (↑n + 1) ≤ ↑n + 1

Tactic:
calc
  f (n + 1) ≤ f (n) + f 1 := f.add_le' ↑n 1
  _ = f (n) + 1 := by rw [map_one]
  _ ≤ n + 1 := add_le_add_right hn 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldrM_reverse [Monad m] (l : Vector α n) (f : α → β → m β) (b) :
    l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
l : Vector α n
f : α → β → m β
b : β
⊢ foldrM f b l.reverse = foldlM (fun x y => f y x) b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : Array α
⊢ foldrM f b { toArray := l, size_toArray := ⋯ }.reverse =
    foldlM (fun x y => f y x) b { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
b : β
l : Array α
⊢ foldrM f b { toArray := l, size_toArray := ⋯ }.reverse =
    foldlM (fun x y => f y x) b { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_cast (p : α → Bool) (l : Vector α n) : countP p (l.cast h) = countP p l

Proof state:
α : Type u_1
n a✝ : Nat
h : n = a✝
p : α → Bool
l : Vector α n
⊢ countP p (Vector.cast h l) = countP p l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a✝ : Nat
p : α → Bool
l : Array α
h : l.size = a✝
⊢ countP p (Vector.cast h { toArray := l, size_toArray := ⋯ }) = countP p { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
a✝ : Nat
p : α → Bool
l : Array α
h : l.size = a✝
⊢ countP p (Vector.cast h { toArray := l, size_toArray := ⋯ }) = countP p { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1)

Proof state:
n : ℕ
⊢ 2 ∣ (n + 1).centralBinom

Tactic:
use (n + 1 + n).choose n

Result:
case h
n : ℕ
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n

Proof state:
case h
n : ℕ
⊢ (n + 1).centralBinom = 2 * (n + 1 + n).choose n

Tactic:
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
    choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum ≠ 0) :
    xs.nonzeroMinimum ∈ xs

Proof state:
xs : List Nat
w : xs.nonzeroMinimum ≠ 0
⊢ xs.nonzeroMinimum ∈ xs

Tactic:
dsimp [nonzeroMinimum] at *

Result:
xs : List Nat
w : ¬(filter (fun x => decide ¬x = 0) xs).min?.getD 0 = 0
⊢ (filter (fun x => decide ¬x = 0) xs).min?.getD 0 ∈ xs

Proof state:
xs : List Nat
m : Option Nat
h : (filter (fun x => decide (x ≠ 0)) xs).min? = m
w : ¬m.getD 0 = 0
⊢ m.getD 0 ∈ xs

Tactic:
match m, w with
| some (m+1), _ => simp_all [min?_eq_some_iff'', mem_filter]

Result:
no goals

Proof state:
xs : List Nat
m✝ : Option Nat
w : ¬m✝.getD 0 = 0
m : Nat
x✝ : ¬(some (m + 1)).getD 0 = 0
h : (filter (fun x => decide (x ≠ 0)) xs).min? = some (m + 1)
⊢ (some (m + 1)).getD 0 ∈ xs

Tactic:
simp_all [min?_eq_some_iff'', mem_filter]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem div_I (z : K) : z / I = -(z * I)

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z / I = -(z * I)

Tactic:
rw [div_eq_mul_inv, inv_I, mul_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem neg_congr {a b : Int} (h₁ : a = b) : -a = -b

Proof state:
a b : Int
h₁ : a = b
⊢ -a = -b

Tactic:
subst h₁

Result:
a : Int
⊢ -a = -a

Proof state:
a : Int
⊢ -a = -a

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_const_lt_top [IsFiniteMeasure μ] {c : ℝ≥0∞} (hc : c ≠ ∞) : ∫⁻ _, c ∂μ < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ ∫⁻ (x : α), c ∂μ < ⊤

Tactic:
simpa only [Measure.restrict_univ] using setLIntegral_const_lt_top (univ : Set α) hc

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_indicator_le (f : α → E) : eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Tactic:
refine eLpNorm_mono_ae <| .of_forall fun x ↦ ?_

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ ‖s.indicator f x‖ ≤ ‖f x‖

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊

Tactic:
exact s.indicator_le_self _ x

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ ‖s.indicator f x‖ ≤ ‖f x‖

Tactic:
suffices ‖s.indicator f x‖₊ ≤ ‖f x‖₊ from NNReal.coe_mono this

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ ‖s.indicator f x‖₊ ≤ ‖f x‖₊

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ ‖s.indicator f x‖₊ ≤ ‖f x‖₊

Tactic:
rw [nnnorm_indicator_eq_indicator_nnnorm]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
f : α → E
x : α
⊢ s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictVarLeft' [DecidableEq α] {γ : Type*} {t : L.Term (α ⊕ γ)} {s : Set α}
    (h : ↑t.varFinsetLeft ⊆ s) {v : α → M} {xs : γ → M} :
    (t.restrictVarLeft (Set.inclusion h)).realize (Sum.elim (v ∘ (↑)) xs) =
      t.realize (Sum.elim v xs) :=
  realize_restrictVarLeft _ (by simp)

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
s : Set α
h : ↑t.varFinsetLeft ⊆ s
v : α → M
xs : γ → M
⊢ ∀ (a : { x // x ∈ t.varFinsetLeft }), Sum.elim (v ∘ Subtype.val) xs (Sum.inl (Set.inclusion h a)) = v ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem toSubtype'_of_subtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n Prop) :
    toSubtype' r ⊚ ofSubtype' r = id

Proof state:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ toSubtype' r ⊚ ofSubtype' r = id

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x

Tactic:
induction i
<;> dsimp only [id, toSubtype', comp, ofSubtype'] at *
<;> simp [Subtype.eta, *]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem ne_neg_self {n : ℕ} (hn : Odd n) {a : ZMod n} (ha : a ≠ 0) : a ≠ -a

Proof state:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ a ≠ -a

Tactic:
rwa [Ne, eq_neg_iff_add_eq_zero, add_self_eq_zero_iff_eq_zero hn]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_integrand_intervalIntegrable (s : ℂ) {X : ℝ} (hs : 0 < s.re) (hX : 0 ≤ X) :
    IntervalIntegrable (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) volume 0 X

Proof state:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntegrableOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 X) volume

Tactic:
exact IntegrableOn.mono_set (GammaIntegral_convergent hs) Ioc_subset_Ioi_self

Result:
no goals

Proof state:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntervalIntegrable (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) volume 0 X

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]

Result:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntegrableOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 X) volume
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma penultimate_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) :
    (p.concat h).penultimate = v

Proof state:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).penultimate = v

Tactic:
simp [penultimate, concat_eq_append, getVert_append]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma rel_symm : Symmetric (Rel t) := fun x y h ↦  by cases h <;> constructor <;> assumption

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
⊢ Rel t y x

Tactic:
cases h <;> constructor <;> assumption

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem rightUnitor_inv_braiding (X : C) : (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv

Tactic:
apply (cancel_mono (λ_ X).hom).1

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom) ≫ (λ_ X).hom = (λ_ X).inv ≫ (λ_ X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom) ≫ (λ_ X).hom = (λ_ X).inv ≫ (λ_ X).hom

Tactic:
simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_zpow_comm {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℤ) : (x ^ y) ^ n = (x ^ n) ^ y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
simp_rw [← rpow_intCast, ← rpow_mul hx, mul_comm y]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_div_comm : a / b / (c / d) = a / c / (b / d)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
lemma isCaratheodory_iUnion {s : ℕ → Set α} (h : ∀ i, m.IsCaratheodory (s i)) :
    m.IsCaratheodory (⋃ i, s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, s i)

Tactic:
rw [← iUnion_disjointed]

Result:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, disjointed s i)

Proof state:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, disjointed s i)

Tactic:
exact m.isCaratheodory_iUnion_of_disjoint (m.isCaratheodory_disjointed h)
  (disjoint_disjointed _)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_iUnion_atTop [Preorder ι] [IsCountablyGenerated (atTop : Filter ι)]
    {s : ι → Set α} (hm : Monotone s) : Tendsto (μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨆ i, μ (s i)))

Tactic:
exact tendsto_atTop_iSup fun n m hnm => measure_mono <| hm hnm

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
rw [hm.measure_iUnion]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (⨆ i, μ (s i)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
refine .of_neBot_imp fun h ↦ ?_

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))

Tactic:
have := (atTop_neBot_iff.1 h).2

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hm : Monotone s
h : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (⇑μ ∘ s) atTop (𝓝 (μ (⋃ n, s n)))
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma hf (j : Under j₀) :
    colimit.ι (kernel (g y)) j ≫ f y = (kernel.ι (g y)).app j :=
  (IsColimit.ι_map _ _ _ _).trans (by simp)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝ : SmallCategory J
Y : J ⥤ C
j₀ : J
y : X ⟶ Y.obj j₀
j : Under j₀
⊢ (kernel.ι (g y)).app j ≫ (constCocone (Under j₀) X).ι.app j = (kernel.ι (g y)).app j

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem nhds_def' (x : X) : 𝓝 x = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 s

Tactic:
simp only [nhds_def, mem_setOf_eq, @and_comm (x ∈ _), iInf_and]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_le_iff_le_rpow_of_base_lt_one (hx : 0 < x) : logb b x ≤ y ↔ b ^ y ≤ x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x

Tactic:
rw [← rpow_le_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hx]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Subalgebra.lean
theorem fg_bot_toSubmodule  : (⊥ : Subalgebra R A).toSubmodule.FG :=
  ⟨{1}, by simp [Algebra.toSubmodule_bot, one_eq_span]⟩

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ span R ↑{1} = toSubmodule ⊥

Tactic:
simp [Algebra.toSubmodule_bot, one_eq_span]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_div_im (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).im = round (x / y : ℂ).im

Proof state:
x y : ℤ[i]
⊢ (toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round ↑(↑(x * star y).im / ↑(norm y)) }).im =
    ↑(round (toComplex x / toComplex y).im)

Tactic:
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]

Result:
no goals

Proof state:
x y : ℤ[i]
⊢ (toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]

Result:
x y : ℤ[i]
⊢ (toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round ↑(↑(x * star y).im / ↑(norm y)) }).im =
    ↑(round (toComplex x / toComplex y).im)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_mod_of_dvd (a : Ordinal) {b c : Ordinal} (h : c ∣ b) : a % b % c = a % c

Proof state:
case intro
a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c

Tactic:
rw [mul_assoc, mul_add_mod_self]

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c

Tactic:
rcases h with ⟨d, rfl⟩

Result:
case intro
a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c

Proof state:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
nth_rw 2 [← div_add_mod a b]

Result:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
-- Mathlib/NumberTheory/MulChar/Basic.lean
/-- If `χ` is of odd order, then `χ(-1) = 1` -/
lemma val_neg_one_eq_one_of_odd_order {χ : MulChar R R'} {n : ℕ} (hn : Odd n) (hχ : χ ^ n = 1) :
    χ (-1) = 1

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ χ (-1) = 1

Tactic:
rw [← hn.neg_one_pow, map_pow, ← χ.pow_apply' (Nat.ne_of_odd_add hn), hχ]

Result:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ 1 (-1) = 1

Proof state:
R : Type u_1
R' : Type u_2
inst✝¹ : CommRing R
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ 1 (-1) = 1

Tactic:
exact MulChar.one_apply_coe (-1)

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
@[simp]
lemma trunc_mul_C (n : ℕ) (f : R⟦X⟧) (r : R) : trunc n (f * C R r) = trunc n f * .C r

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
i : ℕ
⊢ (trunc n (f * (C R) r)).coeff i = (trunc n f * Polynomial.C r).coeff i

Tactic:
simp [coeff_trunc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
⊢ trunc n (f * (C R) r) = trunc n f * Polynomial.C r

Tactic:
ext i

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
i : ℕ
⊢ (trunc n (f * (C R) r)).coeff i = (trunc n f * Polynomial.C r).coeff i