harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
/-- If `A` is a finite free `R`-algebra, then `f : A` is nilpotent on `κ(𝔭) ⊗ A` for some
prime `𝔭 ◃ R` if and only if every non-leading coefficient of `charpoly(f)` is in `𝔭`. -/
lemma isNilpotent_tensor_residueField_iff
    [Module.Free R A] [Module.Finite R A] (f : A) (I : Ideal R) [I.IsPrime] :
    IsNilpotent (algebraMap A (A ⊗[R] I.ResidueField) f) ↔
      ∀ i < Module.finrank R A, (Algebra.lmul R A f).charpoly.coeff i ∈ I

Proof state:
case inr.mpr.a.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Tactic:
obtain (hi | hi) := lt_or_gt_of_ne hi

Result:
case inr.mpr.a.inr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

case inr.mpr.a.inr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i > ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Proof state:
case inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Subsingleton R
this : Subsingleton (A ⊗[R] I.ResidueField)
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

Tactic:
simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem exists_dual_map_eq_bot_of_nmem {x : M} (hx : x ∉ p) (hp' : Free R (M ⧸ p)) :
    ∃ f : Dual R M, f x ≠ 0 ∧ p.map f = ⊥

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
f : Dual R (M ⧸ p)
hf : f (p.mkQ x) ≠ 0
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
f : Dual R (M ⧸ p)
hf : f (p.mkQ x) ≠ 0
⊢ map (f ∘ₗ p.mkQ) p = ⊥

Tactic:
simp [Submodule.map_comp]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
  obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
⊢ ∃ f, f (p.mkQ x) ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
this : ∃ f, f (p.mkQ x) ≠ 0
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
obtain ⟨f, hf⟩ := this

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
f : Dual R (M ⧸ p)
hf : f (p.mkQ x) ≠ 0
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Free R (M ⧸ p)
⊢ ∃ f, f (p.mkQ x) ≠ 0

Tactic:
rwa [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
  ← forall_dual_apply_eq_zero_iff (K := R), not_forall] at hx

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_eq_linear_proj [HasOrthogonalProjection K] (x : E) :
    orthogonalProjection K x =
      K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_completeSpace x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ (orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x

Tactic:
have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_completeSpace

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
this : IsCompl K Kᗮ
⊢ (orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
this : IsCompl K Kᗮ
⊢ (orthogonalProjection K) (↑((K.linearProjOfIsCompl Kᗮ this) x) + ↑((Kᗮ.linearProjOfIsCompl K ⋯) x)) =
    (K.linearProjOfIsCompl Kᗮ ⋯) x

Tactic:
rw [map_add, orthogonalProjection_mem_subspace_eq_self,
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
this : IsCompl K Kᗮ
⊢ (orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x

Tactic:
conv_lhs => rw [← Submodule.linear_proj_add_linearProjOfIsCompl_eq_self this x]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
this : IsCompl K Kᗮ
⊢ (orthogonalProjection K) (↑((K.linearProjOfIsCompl Kᗮ this) x) + ↑((Kᗮ.linearProjOfIsCompl K ⋯) x)) =
    (K.linearProjOfIsCompl Kᗮ ⋯) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (v : Vector α n) :
    v.toList.findM? p = v.findM? p

Proof state:
m : Type → Type
α : Type
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
v : Vector α n
⊢ List.findM? p v.toList = findM? p v

Tactic:
cases v

Result:
case mk
m : Type → Type
α : Type
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
m : Type → Type
α : Type
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
lemma factors_eq : ∀ n : ℕ, normalizedFactors n = n.primeFactorsList
  | 0 => by simp
  | n + 1 => by
    rw [← Multiset.rel_eq, ← associated_eq_eq]
    apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _
    · rw [Multiset.prod_coe, Nat.prod_primeFactorsList n.succ_ne_zero]
      exact prod_normalizedFactors n.succ_ne_zero
    · intro x hx
      rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]
      exact Nat.prime_of_mem_primeFactorsList hx

Proof state:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

Tactic:
rw [Multiset.prod_coe, Nat.prod_primeFactorsList n.succ_ne_zero]

Result:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod n.succ

Proof state:
n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ Prime x

Tactic:
exact Nat.prime_of_mem_primeFactorsList hx

Result:
no goals

Proof state:
⊢ normalizedFactors 0 = ↑(primeFactorsList 0)

Tactic:
simp

Result:
no goals

Proof state:
n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ Irreducible x

Tactic:
rw [Nat.irreducible_iff_prime, ← Nat.prime_iff]

Result:
n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ Prime x

Proof state:
n : ℕ
⊢ normalizedFactors (n + 1) = ↑(n + 1).primeFactorsList

Tactic:
rw [← Multiset.rel_eq, ← associated_eq_eq]

Result:
n : ℕ
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList

Proof state:
n : ℕ
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList

Tactic:
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _

Result:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x

Proof state:
n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x

Tactic:
intro x hx

Result:
n x : ℕ
hx : x ∈ ↑(n + 1).primeFactorsList
⊢ Irreducible x

Proof state:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod n.succ

Tactic:
exact prod_normalizedFactors n.succ_ne_zero

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_const (c : ℝ≥0∞) : μ.withDensity (fun _ ↦ c) = c • μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ (μ.withDensity fun x => c) = c • μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity fun x => c) s = (c • μ) s

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity fun x => c) s = (c • μ) s

Tactic:
simp [withDensity_apply _ hs]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_eq_zero_of_ae_eq_zero (ht_eq : ∀ᵐ x ∂μ, x ∈ t → f x = 0) :
    ∫ x in t, f x ∂μ = 0

Proof state:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0
⊢ ∫ (x : X) in t, f x ∂μ = 0

Tactic:
rw [← this]

Result:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem coeff_of_lt_order (n : ℕ) (h : ↑n < order φ) : coeff R n φ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ φ.order ≤ ↑n

Tactic:
exact order_le _ h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ↑n < φ.order
⊢ (coeff R n) φ = 0

Tactic:
contrapose! h

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ φ.order ≤ ↑n
-- Mathlib/Data/Set/Prod.lean
theorem prod_diff_prod : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
x : α × β
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Proof state:
case h
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
x : α × β
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Tactic:
by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem fixedPoints_of_subsingleton [Subsingleton α] :
    fixedPoints G α = .univ

Proof state:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α) (m : G), m • x = x

Tactic:
intro x hx

Result:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
x : α
hx : G
⊢ hx • x = x

Proof state:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α), x ∈ fixedPoints G α

Tactic:
simp only [mem_fixedPoints]

Result:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α) (m : G), m • x = x

Proof state:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
x : α
hx : G
⊢ hx • x = x

Tactic:
apply Subsingleton.elim ..

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ fixedPoints G α = Set.univ

Tactic:
apply Set.eq_univ_of_forall

Result:
case a
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α), x ∈ fixedPoints G α
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma IsPullback.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPullback)
    (e : sq₁ ≅ sq₂) : sq₂.IsPullback

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
all_goals simp

Result:
no goals

Proof state:
case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₂.IsPullback

Tactic:
refine CategoryTheory.IsPullback.of_iso h
  (evaluation₁.mapIso e) (evaluation₂.mapIso e)
  (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPullback
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
theorem exists_separating_of_ne {x y : V} (h : x ≠ y) :
    ∃ f : V →L[R] R, f x ≠ f y

Proof state:
case intro
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : V →L[R] R
hf : f (x - y) ≠ 0
⊢ ∃ f, f x ≠ f y

Tactic:
exact ⟨f, by simpa [sub_ne_zero] using hf⟩

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : V →L[R] R
hf : f (x - y) ≠ 0
⊢ f x ≠ f y

Tactic:
simpa [sub_ne_zero] using hf

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
⊢ ∃ f, f x ≠ f y

Tactic:
rcases exists_ne_zero (R := R) (sub_ne_zero_of_ne h) with ⟨f, hf⟩

Result:
case intro
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
h : x ≠ y
f : V →L[R] R
hf : f (x - y) ≠ 0
⊢ ∃ f, f x ≠ f y
-- Mathlib/GroupTheory/Perm/Support.lean
theorem not_mem_support {x : α} : x ∉ f.support ↔ f x = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∉ f.support ↔ f x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem expNear_sub (n x r₁ r₂) : expNear n x r₁ -
    expNear n x r₂ = x ^ n / n.factorial * (r₁ - r₂)

Proof state:
n : ℕ
x r₁ r₂ : ℝ
⊢ expNear n x r₁ - expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)

Tactic:
simp [expNear, mul_sub]

Result:
no goals
-- Mathlib/NumberTheory/Bertrand.lean
theorem exists_prime_lt_and_le_two_mul_succ {n} (q) {p : ℕ} (prime_p : Nat.Prime p)
    (covering : p ≤ 2 * q) (H : n < q → ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) (hn : n < p) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n

Proof state:
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
by_cases h : p ≤ 2 * n

Result:
case pos
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

case neg
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Proof state:
case pos
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact ⟨p, prime_p, hn, h⟩

Result:
no goals

Proof state:
case neg
n q p : ℕ
prime_p : Prime p
covering : p ≤ 2 * q
H : n < q → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact H (lt_of_mul_lt_mul_left' (lt_of_lt_of_le (not_le.1 h) covering))

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.IsAmalgamation.compPresheafMap {x : FamilyOfElements P R} {t} (f : P ⟶ Q)
    (h : x.IsAmalgamation t) : (x.compPresheafMap f).IsAmalgamation (f.app (op X) t)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (f.app (op X) ≫ Q.map g.op) t = f.app (op Y) (x g hg)

Tactic:
rw [← f.naturality, types_comp_apply, h g hg]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app (op X) t) = FamilyOfElements.compPresheafMap f x g hg

Tactic:
dsimp [FamilyOfElements.compPresheafMap]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app (op X) t) = f.app (op Y) (x g hg)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
⊢ (FamilyOfElements.compPresheafMap f x).IsAmalgamation (f.app (op X) t)

Tactic:
intro Y g hg

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app (op X) t) = FamilyOfElements.compPresheafMap f x g hg

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ Q.map g.op (f.app (op X) t) = f.app (op Y) (x g hg)

Tactic:
change (f.app _ ≫ Q.map _) _ = _

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (f.app (op X) ≫ Q.map g.op) t = f.app (op Y) (x g hg)
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem EuclideanHalfSpace.convex [NeZero n] :
    Convex ℝ { x : EuclideanSpace ℝ (Fin n) | 0 ≤ x 0 } :=
  fun _ hx _ hy _ _ _ _ _ ↦ by dsimp at hx hy ⊢; positivity

Proof state:
n : ℕ
inst✝ : NeZero n
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : x✝⁶ ∈ {x | 0 ≤ x 0}
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : x✝⁵ ∈ {x | 0 ≤ x 0}
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ x✝⁴ • x✝⁶ + x✝³ • x✝⁵ ∈ {x | 0 ≤ x 0}

Tactic:
dsimp at hx hy ⊢

Result:
n : ℕ
inst✝ : NeZero n
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : 0 ≤ x✝⁶ 0
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : 0 ≤ x✝⁵ 0
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ 0 ≤ x✝⁴ * x✝⁶ 0 + x✝³ * x✝⁵ 0

Proof state:
n : ℕ
inst✝ : NeZero n
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : 0 ≤ x✝⁶ 0
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : 0 ≤ x✝⁵ 0
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ 0 ≤ x✝⁴ * x✝⁶ 0 + x✝³ * x✝⁵ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/Equiv/TransferInstance.lean
theorem algEquiv_symm_apply (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) : by
    letI := Equiv.semiring e
    letI := Equiv.algebra R e
    exact (algEquiv R e).symm b = e.symm b := rfl

Proof state:
α : Type u
β : Type v
e✝ : α ≃ β
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this : Semiring α := e.semiring
⊢ Sort ?u.100528

Tactic:
letI := Equiv.algebra R e

Result:
α : Type u
β : Type v
e✝ : α ≃ β
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this✝ : Semiring α := e.semiring
this : Algebra R α := Equiv.algebra R e
⊢ Sort ?u.100528

Proof state:
α : Type u
β : Type v
e✝ : α ≃ β
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
⊢ Sort ?u.100528

Tactic:
letI := Equiv.semiring e

Result:
α : Type u
β : Type v
e✝ : α ≃ β
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this : Semiring α := e.semiring
⊢ Sort ?u.100528

Proof state:
α : Type u
β : Type v
e✝ : α ≃ β
R : Type u_1
inst✝² : CommSemiring R
e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this✝ : Semiring α := e.semiring
this : Algebra R α := Equiv.algebra R e
⊢ Sort ?u.100528

Tactic:
exact (algEquiv R e).symm b = e.symm b

Result:
no goals