harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
    tensorHom (𝟙 (ModuleCat.of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)

Tactic:
apply TensorProduct.ext

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ (mk R ↑(of R R) ↑M).compr₂ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    (mk R ↑(of R R) ↑M).compr₂ (Hom.hom ((leftUnitor M).hom ≫ f))

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ (mk R ↑(of R R) ↑M).compr₂ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    (mk R ↑(of R R) ↑M).compr₂ (Hom.hom ((leftUnitor M).hom ≫ f))

Tactic:
ext x

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (((mk R ↑(of R R) ↑M).compr₂ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom))) 1) x =
    (((mk R ↑(of R R) ↑M).compr₂ (Hom.hom ((leftUnitor M).hom ≫ f))) 1) x

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (leftUnitor N).hom) ((Hom.hom (tensorHom (𝟙 (of R R)) f)) (1 ⊗ₜ[R] x)) =
    (Hom.hom f) ((Hom.hom (leftUnitor M).hom) (1 ⊗ₜ[R] x))

Tactic:
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (1, x).1 • (Hom.hom f) (1, x).2 = (Hom.hom f) (1 • x)

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (1, x).1 • (Hom.hom f) (1, x).2 = 1 • (Hom.hom f) x

Tactic:
rfl

Result:
no goals

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (1, x).1 • (Hom.hom f) (1, x).2 = (Hom.hom f) (1 • x)

Tactic:
rw [LinearMap.map_smul]

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (𝟙 (of R R))) (1, x).1 • (Hom.hom f) (1, x).2 = 1 • (Hom.hom f) x

Proof state:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (((mk R ↑(of R R) ↑M).compr₂ (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom))) 1) x =
    (((mk R ↑(of R R) ↑M).compr₂ (Hom.hom ((leftUnitor M).hom ≫ f))) 1) x

Tactic:
dsimp

Result:
case hf.H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ (Hom.hom (leftUnitor N).hom) ((Hom.hom (tensorHom (𝟙 (of R R)) f)) (1 ⊗ₜ[R] x)) =
    (Hom.hom f) ((Hom.hom (leftUnitor M).hom) (1 ⊗ₜ[R] x))
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem sup_toSubalgebra_of_isAlgebraic_left [Algebra.IsAlgebraic K E1] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have := sup_toSubalgebra_of_isAlgebraic_right E2 E1

Result:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Hom.lean
theorem ext_of_ring {f g : R →ₗc[R] A} (h : f 1 = g 1) : f = g :=
  coe_linearMap_injective (by ext; assumption)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ ((fun x => ↑x) f) 1 = ((fun x => ↑x) g) 1

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ (fun x => ↑x) f = (fun x => ↑x) g

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ ((fun x => ↑x) f) 1 = ((fun x => ↑x) g) 1
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem support_integralNormalization_subset :
    (integralNormalization p).support ⊆ p.support

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : ℕ
⊢ a✝ ∈ p.integralNormalization.support → a✝ ∈ p.support

Tactic:
simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.support ⊆ p.support

Tactic:
intro

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : ℕ
⊢ a✝ ∈ p.integralNormalization.support → a✝ ∈ p.support
-- Mathlib/Algebra/MvPolynomial/Eval.lean
lemma comp_aeval_apply {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B)
    (p : MvPolynomial σ R) :
    φ (aeval f p) = aeval (fun i ↦ φ (f i)) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = (aeval fun i => φ (f i)) p

Tactic:
rw [← comp_aeval, AlgHom.coe_comp, comp_apply]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_smul (d : ℕ) (u : PrimeMultiset) : (d • u).prod = u.prod ^ d

Proof state:
d : ℕ
u : PrimeMultiset
⊢ (d • u).prod = u.prod ^ d

Tactic:
induction d with
| zero => simp only [zero_nsmul, pow_zero, prod_zero]
| succ n ih => rw [succ_nsmul, prod_add, ih, pow_succ]

Result:
no goals

Proof state:
case zero
u : PrimeMultiset
⊢ (0 • u).prod = u.prod ^ 0

Tactic:
simp only [zero_nsmul, pow_zero, prod_zero]

Result:
no goals

Proof state:
case succ
u : PrimeMultiset
n : ℕ
ih : (n • u).prod = u.prod ^ n
⊢ ((n + 1) • u).prod = u.prod ^ (n + 1)

Tactic:
rw [succ_nsmul, prod_add, ih, pow_succ]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Finite.lean
lemma RingHom.surjective_of_tmul_eq_tmul_of_finite {R S}
    [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
    (h₁ : ∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s) : Function.Surjective (algebraMap R S)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
h✝ : Nontrivial (S ⧸ R')
x y : S
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] 1 * 1 ⊗ₜ[R] y

Tactic:
simp [h₁]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
let R' := LinearMap.range (Algebra.ofId R S).toLinearMap

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
R' : Submodule R S := LinearMap.range (Algebra.ofId R S).toLinearMap
⊢ Function.Surjective ⇑(algebraMap R S)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_sub_right (d) : (∫ x in a..b, f (x - d)) = ∫ x in a - d..b - d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (x - d) = ∫ (x : ℝ) in a - d..b - d, f x

Tactic:
simpa only [sub_eq_add_neg] using integral_comp_add_right f (-d)

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittMul (n : ℕ) : constantCoeff (wittMul p n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 * X 1) = 0

Tactic:
simp only [mul_zero, RingHom.map_mul, constantCoeff_X]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittMul p n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (X 0 * X 1) = 0
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem mem_toCone' : x ∈ hs.toCone s ↔ ∃ c : 𝕜, 0 < c ∧ c • x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s

Tactic:
refine hs.mem_toCone.trans ⟨?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
⊢ c⁻¹ • c • y ∈ s

Tactic:
rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ c • x ∈ s) → ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
rintro ⟨c, hc, hcx⟩

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ c⁻¹ • c • x = x

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ (∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x) → ∃ c, 0 < c ∧ c • x ∈ s

Tactic:
rintro ⟨c, hc, y, hy, rfl⟩

Result:
case refine_1.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
⊢ ∃ c_1, 0 < c_1 ∧ c_1 • c • y ∈ s

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ ∃ c, 0 < c ∧ ∃ y ∈ s, c • y = x

Tactic:
exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
hc : 0 < c
y : E
hy : y ∈ s
⊢ ∃ c_1, 0 < c_1 ∧ c_1 • c • y ∈ s

Tactic:
exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_le_aleph0 {c : Cardinal.{u}} : lift.{v} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
simpa using lift_le (b := ℵ₀)

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem StrictConcaveOn.secant_strict_mono (hf : StrictConcaveOn 𝕜 s f) {a x y : 𝕜} (ha : a ∈ s)
    (hx : x ∈ s) (hy : y ∈ s) (hxa : x ≠ a) (hya : y ≠ a) (hxy : x < y) :
    (f y - f a) / (y - a) < (f x - f a) / (x - a)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
rw [← neg_lt_neg_iff]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ -((f x - f a) / (x - a)) < -((f y - f a) / (y - a))

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ -((f x - f a) / (x - a)) < -((f y - f a) / (y - a))

Tactic:
convert key using 1 <;> field_simp <;> ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
simp only [Pi.neg_apply] at key

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : (-f x - -f a) / (x - a) < (-f y - -f a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
-- Mathlib/Computability/DFA.lean
theorem eval_comap (f : α' → α) (x : List α') : (M.comap f).eval x = M.eval (x.map f)

Proof state:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
f : α' → α
x : List α'
⊢ (comap f M).eval x = M.eval (List.map f x)

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_smul_measure_of_ne_zero {c : ℝ≥0∞} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞)
    (μ : Measure α) : eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c

Result:
no goals

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [hp_top, eLpNormEssSup_smul_measure hc]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0∞
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [hp0]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem nat_card_range_toPermHom :
    Nat.card (toPermHom g).range =
      ∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!

Proof state:
case e_α.e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ ↑(toPermHom g).range = {k | sc ∘ ⇑k = sc}

Tactic:
ext

Result:
case e_α.e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
x✝ : Perm { x // x ∈ g.cycleFactorsFinset }
⊢ x✝ ∈ ↑(toPermHom g).range ↔ x✝ ∈ {k | sc ∘ ⇑k = sc}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Nat.card ↑↑(toPermHom g).range = Nat.card ↑{k | sc ∘ ⇑k = sc}

Tactic:
congr

Result:
case e_α.e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ ↑(toPermHom g).range = {k | sc ∘ ⇑k = sc}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Nat.card ↥(toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
suffices Fintype.card (toPermHom g).range =
  Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
  simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
    Finset.univ_eq_attach]
  simp_rw [← CycleType.count_def]
  apply Finset.prod_congr _ (fun _ _ => rfl)
  ext n
  simp only [Finset.univ_eq_attach, Finset.mem_image, Finset.mem_attach,
      hsc, true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
  simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : { x // x ∈ g.cycleFactorsFinset } → ℕ := fun c => (↑c).support.card
hsc : sc = fun c => (↑c).support.card
⊢ Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
-- Mathlib/Data/Set/Function.lean
theorem range_extend {f : α → β} (hf : Injective f) (g : α → γ) (g' : β → γ) :
    range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
refine (range_extend_subset _ _ _).antisymm ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')

Tactic:
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')

Tactic:
rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)

Result:
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
    (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
  | ⟨r, hr⟩ => by
    refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
    · exact fun i ↦ norm_nonneg _
    · simpa only using hr

Proof state:
case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Tactic:
simpa only using hr

Result:
no goals

Proof state:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Summable f

Tactic:
refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩

Result:
case refine_1
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

case refine_2
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Proof state:
case refine_1
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

Tactic:
exact fun i ↦ norm_nonneg _

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Colorable.of_embedding {V' : Type*} {G' : SimpleGraph V'} (f : G ↪g G') {n : ℕ}
    (h : G'.Colorable n) : G.Colorable n :=
  ⟨(h.toColoring (by simp)).comp f⟩

Proof state:
V : Type u
G : SimpleGraph V
V' : Type u_3
G' : SimpleGraph V'
f : G ↪g G'
n : ℕ
h : G'.Colorable n
⊢ n ≤ card (Fin n)

Tactic:
simp

Result:
no goals