harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem smoothingFun_of_powMul (hμ1 : μ 1 ≤ 1) {x : R}
    (hx : ∀ (n : ℕ) (_hn : 1 ≤ n), μ (x ^ n) = μ x ^ n) : smoothingFun μ x = μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun x_1 => μ x

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
⊢ smoothingSeminormSeq μ x n = μ x

Tactic:
simp only [smoothingSeminormSeq]

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = μ x

Tactic:
intro n hn

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
⊢ smoothingSeminormSeq μ x n = μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → smoothingSeminormSeq μ x b = μ x

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ ∀ (b : ℕ), 1 ≤ b → smoothingSeminormSeq μ x b = μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ smoothingFun μ x = μ x

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
  tendsto_const_nhds

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
⊢ smoothingSeminormSeq μ x =ᶠ[atTop] fun x_1 => μ x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sort_cons {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) :
    sort r (cons a s h₂) = a :: sort r s

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
a : α
s : Finset α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ sort r (cons a s h₂) = a :: sort r s

Tactic:
rw [sort, cons_val, Multiset.sort_cons r a _ h₁, sort_val]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Basic.lean
theorem arrowCongr_comp {N N₂ N₃ : Sort _} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃]
    [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃)
    (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
    arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f)

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
⊢ (e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
x✝ : N
⊢ ((e₁.arrowCongr e₃) (g ∘ₗ f)) x✝ = ((e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f) x✝

Proof state:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
N : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R N
inst✝¹ : Module R N₂
inst✝ : Module R N₃
e₁ : M ≃ₗ[R] N
e₂ : M₂ ≃ₗ[R] N₂
e₃ : M₃ ≃ₗ[R] N₃
f : M →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
x✝ : N
⊢ ((e₁.arrowCongr e₃) (g ∘ₗ f)) x✝ = ((e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f) x✝

Tactic:
simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem OrderIso.essSup_apply {m : MeasurableSpace α} {γ} [CompleteLattice γ] (f : α → β)
    (μ : Measure α) (g : β ≃o γ) : g (essSup f μ) = essSup (fun x => g (f x)) μ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ g (essSup f μ) = essSup (fun x => g (f x)) μ

Tactic:
refine OrderIso.limsup_apply g ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => g (f x)

case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => g (f x)

Proof state:
case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => g (f x)

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => g (f x)

case refine_4
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_3
inst✝ : CompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => g (f x)

Tactic:
all_goals isBoundedDefault

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBy_iff_torsionBy_eq_top : IsTorsionBy R M a ↔ torsionBy R M a = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBy R M a ↔ torsionBy R M a = ⊤

Tactic:
rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
  isTorsionBySet_iff_torsionBySet_eq_top]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem summable_norm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : ↑r < p.radius) :
    Summable fun n : ℕ => ‖p n‖ * (r : ℝ) ^ n

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ Summable fun n => ‖p n‖ * ↑r ^ n

Tactic:
exact .of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg _))
  hp ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun n => ‖p n‖ * ↑r ^ n

Tactic:
obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
⊢ Summable fun n => ‖p n‖ * ↑r ^ n
-- Mathlib/Probability/Distributions/Poisson.lean
lemma poissonPMFReal_nonneg {r : ℝ≥0} {n : ℕ} : 0 ≤ poissonPMFReal r n

Proof state:
r : ℝ≥0
n : ℕ
⊢ 0 ≤ poissonPMFReal r n

Tactic:
unfold poissonPMFReal

Result:
r : ℝ≥0
n : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ n / ↑n !

Proof state:
r : ℝ≥0
n : ℕ
⊢ 0 ≤ rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
@[simp]
lemma bnot_isNone (a : Option α) : (! a.isNone) = a.isSome

Proof state:
α : Type u_1
a : Option α
⊢ (!a.isNone) = a.isSome

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem coe_le_iff : ↑a ≤ x ↔ ∀ b : α, x = ↑b → a ≤ b

Proof state:
α : Type u_1
a : α
inst✝ : LE α
x : WithTop α
⊢ ↑a ≤ x ↔ ∀ (b : α), x = ↑b → a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem injective_of_mono {G H : AddCommGrp.{0}} (f : G ⟶ H) [Mono f] : Function.Injective f :=
  fun g₁ g₂ h => by
  have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f

Proof state:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ g₁ = g₂

Tactic:
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by aesop_cat

Result:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂

Proof state:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂

Tactic:
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0

Result:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂

Proof state:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂

Tactic:
apply asHom_injective t1

Result:
no goals

Proof state:
G H : AddCommGrp
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem and_and_right : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c

Proof state:
a b c : Prop
⊢ (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c

Tactic:
rw [and_and_and_comm, and_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_X_add_C [Semiring S] (r : S) : (X + C r).leadingCoeff = 1

Proof state:
S : Type v
inst✝ : Semiring S
r : S
⊢ (X + C r).leadingCoeff = 1

Tactic:
rw [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem PairwiseDisjoint.image_of_le (hs : s.PairwiseDisjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) :
    (g '' s).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
⊢ (g '' s).PairwiseDisjoint f

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
hs : s.PairwiseDisjoint f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)

Tactic:
exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem colimitPresheafObjIsoComponentwiseLimit_hom_π (F : J ⥤ PresheafedSpace.{_, _, v} C)
    (U : Opens (Limits.colimit F).carrier) (j : J) :
    (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π _ (op j) =
      (colimit.ι F j).c.app (op U)

Proof state:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) =
    (colimit.ι F j).c.app (op U)

Tactic:
rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_biUnion_toMeasurable {I : Set β} (hc : I.Countable) (s : β → Set α) :
    μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
⊢ μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

Tactic:
haveI := hc.toEncodable

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
this : Encodable ↑I
⊢ μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
I : Set β
hc : I.Countable
s : β → Set α
this : Encodable ↑I
⊢ μ (⋃ b ∈ I, toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)

Tactic:
simp only [biUnion_eq_iUnion, measure_iUnion_toMeasurable]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem star_mul_self_eq_zero_iff (x : E) : x⋆ * x = 0 ↔ x = 0

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0

Tactic:
exact mul_self_eq_zero.trans norm_eq_zero

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x⋆ * x = 0 ↔ x = 0

Tactic:
rw [← norm_eq_zero, norm_star_mul_self]

Result:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x‖ * ‖x‖ = 0 ↔ x = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_map_iff {f : α → β} :
    L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
L₁ L₂ : Array β
l : Array α
f : α → β
⊢ L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rw [eq_comm, map_eq_append_iff]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem smul_induction {C : Word M → Prop} (h_empty : C empty)
    (h_smul : ∀ (i) (m : M i) (w), C w → C (of m • w)) (w : Word M) : C w

Proof state:
case h_empty
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
C : Word M → Prop
h_empty : C empty
h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)
⊢ C empty

Tactic:
exact h_empty

Result:
no goals

Proof state:
case h_cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
C : Word M → Prop
h_empty : C empty
h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : C w✝
⊢ C (of m✝ • w✝)

Tactic:
exact h_smul _ _ _ ih

Result:
no goals

Proof state:
case h_cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
C : Word M → Prop
h_empty : C empty
h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : C w✝
⊢ C (cons m✝ w✝ h1✝ h2✝)

Tactic:
rw [cons_eq_smul]

Result:
case h_cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
C : Word M → Prop
h_empty : C empty
h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)
i✝ : ι
m✝ : M i✝
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some i✝
h2✝ : m✝ ≠ 1
ih : C w✝
⊢ C (of m✝ • w✝)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
C : Word M → Prop
h_empty : C empty
h_smul : ∀ (i : ι) (m : M i) (w : Word M), C w → C (of m • w)
w : Word M
⊢ C w

Tactic:
induction w using consRecOn with
| h_empty => exact h_empty
| h_cons _ _ _ _ _ ih =>
  rw [cons_eq_smul]
  exact h_smul _ _ _ ih

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
/-- Characterisation of `2`-Freiman homomorphisms. -/
@[to_additive "Characterisation of `2`-Freiman homomorphisms."]
lemma isMulFreimanHom_two :
    IsMulFreimanHom 2 A B f ↔ MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A,
      a * b = c * d → f a * f b = f c * f d where
  mp hf := ⟨hf.mapsTo, fun _ ha _ hb _ hc _ hd ↦ hf.mul_eq_mul ha hb hc hd⟩
  mpr hf := ⟨hf.1, by aesop (add simp card_eq_two)⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 2 → t.card = 2 → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
aesop (add simp card_eq_two)

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
lemma sSup_mem_of_not_isSuccPrelimit (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Tactic:
exact eq_of_le_of_not_lt (le_sSup his) (hy.2 hi) ▸ his

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt

Result:
case intro.intro.intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
i : α
his : i ∈ s
hi : y < i
⊢ sSup s ∈ s

Proof state:
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Result:
case intro
α : Type u_2
inst✝ : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
lemma dvd_comp_C_mul_X_add_C_iff (p q : R[X]) (a b : R) [Invertible a] :
    p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟ a * (X - C b)) ∣ q

Proof state:
R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q

Tactic:
convert map_dvd_iff <| algEquivCMulXAddC a b using 2

Result:
case h.e'_1.h.e'_3
R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p = (algEquivCMulXAddC a b) (p.comp (C ⅟a * (X - C b)))

Proof state:
case h.e'_1.h.e'_3
R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p = (algEquivCMulXAddC a b) (p.comp (C ⅟a * (X - C b)))

Tactic:
simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
lemma cast_commute (q : ℚ≥0) (a : α) : Commute (↑q) a

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q) a

Tactic:
simpa only [cast_def] using (q.num.cast_commute a).div_left (q.den.cast_commute a)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem transpose_zpow (A : M) : ∀ n : ℤ, (A ^ n)ᵀ = Aᵀ ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, transpose_pow]
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᵀ = Aᵀ ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, transpose_pow]

Result:
no goals