harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_dvd {f : α → N} (a : α) (hf : (mulSupport f).Finite) : f a ∣ finprod f

Proof state:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f

Tactic:
exact one_dvd (finprod f)

Result:
no goals

Proof state:
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
⊢ f a ∣ finprod f

Tactic:
by_cases ha : a ∈ mulSupport f

Result:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Proof state:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∈ mulSupport f
⊢ f a ∣ finprod f

Tactic:
rw [finprod_eq_prod_of_mulSupport_toFinset_subset f hf (Set.Subset.refl _)]

Result:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ hf.toFinset, f i

Proof state:
case pos
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∈ mulSupport f
⊢ f a ∣ ∏ i ∈ hf.toFinset, f i

Tactic:
exact Finset.dvd_prod_of_mem f ((Finite.mem_toFinset hf).mpr ha)

Result:
no goals

Proof state:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
rw [nmem_mulSupport.mp ha]

Result:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : (mulSupport f).Finite
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem hom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : CliffordAlgebra Q →ₐ[R] A} :
    f.toLinearMap.comp (ι Q) = g.toLinearMap.comp (ι Q) → f = g

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ f = g

Tactic:
apply (lift Q).symm.injective

Result:
case a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ (lift Q).symm f = (lift Q).symm g

Proof state:
case a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ (lift Q).symm f = (lift Q).symm g

Tactic:
rw [lift_symm_apply, lift_symm_apply]

Result:
case a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ ⟨f.toLinearMap ∘ₗ ι Q, ⋯⟩ = ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
⊢ f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q → f = g

Tactic:
intro h

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ f = g

Proof state:
case a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ ⟨f.toLinearMap ∘ₗ ι Q, ⋯⟩ = ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩

Tactic:
simp only [h]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/UpperLower.lean
theorem IsUpperSet.interior (h : IsUpperSet s) : IsUpperSet (interior s)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)

Tactic:
exact h.compl.closure

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)

Tactic:
rw [← isLowerSet_compl, ← closure_compl]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (closure sᶜ)
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.of_zpow {n : ℤ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f

Proof state:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle

Tactic:
cases n

Result:
case ofNat
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.ofNat a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a✝).support
⊢ f.IsCycle

case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle

Proof state:
case ofNat
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.ofNat a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.ofNat a✝).support
⊢ f.IsCycle

Tactic:
exact h1.of_pow h2

Result:
no goals

Proof state:
case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ (a✝ + 1))⁻¹.IsCycle
h2 : f.support ⊆ (f ^ (a✝ + 1)).support
⊢ f.IsCycle

Tactic:
exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

Result:
no goals

Proof state:
case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ Int.negSucc a✝).IsCycle
h2 : f.support ⊆ (f ^ Int.negSucc a✝).support
⊢ f.IsCycle

Tactic:
simp only [le_eq_subset, zpow_negSucc, Perm.support_inv] at h1 h2

Result:
case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ (a✝ + 1))⁻¹.IsCycle
h2 : f.support ⊆ (f ^ (a✝ + 1)).support
⊢ f.IsCycle
-- Mathlib/Algebra/Ring/Basic.lean
lemma neg_inv : -a⁻¹ = (-a)⁻¹

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -a⁻¹ = (-a)⁻¹

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_mem_Ico' (b : α) : toIcoMod hp 0 b ∈ Set.Ico 0 p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p

Tactic:
convert toIcoMod_mem_Ico hp 0 b

Result:
case h.e'_4.h.e'_4
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ p = 0 + p

Proof state:
case h.e'_4.h.e'_4
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ p = 0 + p

Tactic:
exact (zero_add p).symm

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem card_boundaries_eq_succ_length : c.boundaries.card = c.length + 1

Proof state:
n : ℕ
c : Composition n
⊢ c.boundaries.card = c.length + 1

Tactic:
simp [boundaries]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map_map₂ (f₁ : γ → ζ) (f₂ : α → β → γ) :
    map f₁ (map₂ f₂ xs ys) = map₂ (fun x y => f₁ <| f₂ x y) xs ys

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun x y => f₁ (f₂ x y)) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem hasPDF_of_map_eq_withDensity (hX : AEMeasurable X ℙ) (f : E → ℝ≥0∞) (hf : AEMeasurable f μ)
    (h : map X ℙ = μ.withDensity f) : HasPDF X ℙ μ

Proof state:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ

Tactic:
exact withDensity_absolutelyContinuous μ f

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ

Tactic:
exact haveLebesgueDecomposition_withDensity μ hf.measurable_mk

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ

Tactic:
rw [withDensity_congr_ae hf.ae_eq_mk]

Result:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ HasPDF X ℙ μ

Tactic:
refine ⟨hX, ?_, ?_⟩ <;> rw [h]

Result:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ

case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ
-- Mathlib/Data/Set/Image.lean
theorem preimage_eq_preimage' {s t : Set α} {f : β → α} (hs : s ⊆ range f) (ht : t ⊆ range f) :
    f ⁻¹' s = f ⁻¹' t ↔ s = t

Proof state:
case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s

Tactic:
rw [← preimage_subset_preimage_iff ht, h]

Result:
no goals

Proof state:
case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t

Tactic:
rw [← preimage_subset_preimage_iff hs, h]

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s

Proof state:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t

case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t

Proof state:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t

Tactic:
apply Subset.antisymm

Result:
case mp.h₁
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t

case mp.h₂
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem comap_map_eq (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ y⁻¹ * x ∈ f.ker

Tactic:
simp [mem_ker, hy']

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ x ∈ H ⊔ f.ker

Tactic:
rw [← mul_inv_cancel_left y x]

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ y * (y⁻¹ * x) ∈ H ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) = H ⊔ f.ker

Tactic:
refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ f.ker

Tactic:
intro x hx

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker

Tactic:
simp only [exists_prop, mem_map, mem_comap] at hx

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1 ∈ H, f x_1 = f x
⊢ x ∈ H ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1 ∈ H, f x_1 = f x
⊢ x ∈ H ⊔ f.ker

Tactic:
rcases hx with ⟨y, hy, hy'⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ x ∈ H ⊔ f.ker

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : f y = f x
⊢ y * (y⁻¹ * x) ∈ H ⊔ f.ker

Tactic:
exact mul_mem_sup hy (by simp [mem_ker, hy'])

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_singleton_iso (P : Cᵒᵖ ⥤ Type w) : IsSheafFor P (Presieve.singleton (𝟙 X))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
refine ⟨x _ (Presieve.singleton_self _), ?_, ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ (fun t => x.IsAmalgamation t) (x (𝟙 X) ⋯)

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t => x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
intro x _

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ t = x (𝟙 X) ⋯

Tactic:
simpa using ht _ (Presieve.singleton_self _)

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t => x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Tactic:
intro t ht

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ t = x (𝟙 X) ⋯

Proof state:
case refine_1.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
Y : C
⊢ P.map (𝟙 X).op (x (𝟙 X) ⋯) = x (𝟙 X) ⋯

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ (fun t => x.IsAmalgamation t) (x (𝟙 X) ⋯)

Tactic:
rintro _ _ ⟨rfl, rfl⟩

Result:
case refine_1.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
Y : C
⊢ P.map (𝟙 X).op (x (𝟙 X) ⋯) = x (𝟙 X) ⋯
-- Mathlib/Data/Pi/Interval.lean
theorem card_Ioc : #(Ioc a b) = ∏ i, #(Icc (a i) (b i)) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioc a b) = ∏ i : ι, #(Icc (a i) (b i)) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk0_surjective [IsDedekindDomain R] :
    Function.Surjective (ClassGroup.mk0 : (Ideal R)⁰ → ClassGroup R)

Proof state:
case mk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk0 ⟨integralRep ↑I, ⋯⟩ = Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I

Tactic:
rw [ClassGroup.mk0_integralRep, ClassGroup.Quot_mk_eq_mk]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ Function.Surjective ⇑mk0

Tactic:
rintro ⟨I⟩

Result:
case mk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ∃ a, mk0 a = Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I

Proof state:
case mk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ ∃ a, mk0 a = Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I

Tactic:
refine ⟨⟨ClassGroup.integralRep I.1, ClassGroup.integralRep_mem_nonZeroDivisors I.ne_zero⟩, ?_⟩

Result:
case mk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
b✝ : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk0 ⟨integralRep ↑I, ⋯⟩ = Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I
-- Mathlib/RingTheory/Invariant.lean
theorem eval_charpoly (b : B) : (charpoly G b).eval b = 0

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ ∏ j : G, eval b (X - C (j • b)) = 0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ (1 : G))

Result:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (X - C (1 • b)) = 0

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (X - C (1 • b)) = 0

Tactic:
rw [one_smul, eval_sub, eval_C, eval_X, sub_self]

Result:
no goals

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (charpoly G b) = 0

Tactic:
rw [charpoly_eq, eval_prod]

Result:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ ∏ j : G, eval b (X - C (j • b)) = 0
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_def_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
    x ^ y = if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs <;>
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
(Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
simp only [rpow_def, Complex.cpow_def]

Result:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem muld_val (x y : ℤ) : sqrtd (d := d) * ⟨x, y⟩ = ⟨d * y, x⟩

Proof state:
d x y : ℤ
⊢ sqrtd * { re := x, im := y } = { re := d * y, im := x }

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem intCast_inj {m n : ℤ} {R : Type*} [Ring R] [CharZero R] : (↑m : R[X]) = ↑n ↔ m = n

Proof state:
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
constructor

Result:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Proof state:
case mpr
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m

Tactic:
rfl

Result:
no goals

Proof state:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n

Tactic:
apply_fun fun p => p.coeff 0 at h

Result:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Proof state:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

Tactic:
intro h

Result:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n

Proof state:
case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl

Result:
case mpr
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LipschitzWith.mul (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (Kf + Kg) fun x ↦ f x * g x

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x => f x * g x

Tactic:
simpa [← lipschitzOnWith_univ] using hf.lipschitzOnWith.mul hg.lipschitzOnWith

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToFun_le_mul_norm' (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
    ‖setToFun μ T hT f‖ ≤ max C 0 * ‖f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ ‖setToFun μ T hT ↑↑f‖ ≤ (C ⊔ 0) * ‖f‖

Tactic:
rw [L1.setToFun_eq_setToL1]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ ‖(L1.setToL1 hT) f‖ ≤ (C ⊔ 0) * ‖f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : ↥(Lp E 1 μ)
⊢ ‖(L1.setToL1 hT) f‖ ≤ (C ⊔ 0) * ‖f‖

Tactic:
exact L1.norm_setToL1_le_mul_norm' hT f

Result:
no goals