harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma snd_of_toSubgraph_adj {u v v'} {p : G.Walk u v} (hp : p.IsPath)
    (hadj : p.toSubgraph.Adj u v') : p.snd = v'

Proof state:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u, v') ∧ i < p.length
⊢ p.snd = v'

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at hi

Result:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
⊢ p.snd = v'

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ p.getVert i = p.getVert 0

Tactic:
rw [p.getVert_zero, hl1]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
⊢ p.snd = v'

Tactic:
have ⟨i, hi⟩ := p.toSubgraph_adj_iff.mp hadj

Result:
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u, v') ∧ i < p.length
⊢ p.snd = v'

Proof state:
case inl.intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ p.snd = p.getVert (i + 1)

Tactic:
have : i = 0 := by
  apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
  rw [p.getVert_zero, hl1]

Result:
case inl.intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
this : i = 0
⊢ p.snd = p.getVert (i + 1)

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_setOf]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
i : ℕ
hl1 : p.getVert i = u
hadj : p.toSubgraph.Adj u (p.getVert (i + 1))
hi :
  (p.getVert i = u ∧ p.getVert (i + 1) = p.getVert (i + 1) ∨ p.getVert i = p.getVert (i + 1) ∧ p.getVert (i + 1) = u) ∧
    i < p.length
⊢ 0 ≤ p.length
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)]
lemma univ_div_univ : (univ / univ : Set α) = univ

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
⊢ univ / univ = univ

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem castHom_bijective [Fintype R] (h : Fintype.card R = n) :
    Function.Bijective (ZMod.castHom (dvd_refl n) R)

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
apply ZMod.castHom_injective

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective ⇑(castHom ⋯ R)

Tactic:
rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]

Result:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R)

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False

Tactic:
exact (Fintype.card_eq_zero_iff.mp h).elim' 0

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ Bijective ⇑(castHom ⋯ R)

Tactic:
haveI : NeZero n :=
  ⟨by
    intro hn
    rw [hn] at h
    exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩

Result:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective ⇑(castHom ⋯ R)

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ n ≠ 0

Tactic:
intro hn

Result:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False

Proof state:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False

Tactic:
rw [hn] at h

Result:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False
-- Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
/-- A global integral curve is injective xor periodic with positive period. -/
lemma IsIntegralCurve.periodic_xor_injective [BoundarylessManifold I M]
    (hγ : IsIntegralCurve γ v)
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M))) :
    Xor' (∃ T > 0, Periodic γ T) (Injective γ)

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
h : ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂
⊢ ∃ T > 0, Periodic γ T

Tactic:
push_neg at h

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
h : ∃ a₁ a₂, γ a₁ = γ a₂ ∧ a₁ ≠ a₂
⊢ ∃ T > 0, Periodic γ T

Proof state:
case neg
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ (a - b)

Tactic:
exact hγ.periodic_of_eq hv heq

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma four_mul_le_sq_add [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddLeftReflectLE α] [AddLeftMono α]
    (a b : α) : 4 * a * b ≤ (a + b) ^ 2

Proof state:
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 4 * a * b = 2 * a * b + 2 * a * b

Tactic:
rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 4 * a * b ≤ (a + b) ^ 2

Tactic:
calc 4 * a * b
  _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
  _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
  _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
  _ = (a + b) ^ 2 := (add_sq a b).symm

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 2 * a * b + 2 * a * b ≤ a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
gcongr

Result:
case bc
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2

Proof state:
case bc
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ 2 * a * b ≤ a ^ 2 + b ^ 2

Tactic:
exact two_mul_le_add_sq _ _

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : CommSemiring α
inst✝⁴ : LinearOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLE α
inst✝ : AddLeftMono α
a b : α
⊢ a ^ 2 + b ^ 2 + 2 * a * b = a ^ 2 + 2 * a * b + b ^ 2

Tactic:
rw [add_right_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_eq_top_iff (s : Set R) :
    zeroLocus s = ⊤ ↔ s ⊆ nilradical R

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) → zeroLocus s = ⊤

Tactic:
rw [eq_top_iff]

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) → ⊤ ≤ zeroLocus s

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) → ⊤ ≤ zeroLocus s

Tactic:
intro h p _

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
h : s ⊆ ↑(nilradical R)
p : PrimeSpectrum R
a✝ : p ∈ ⊤
⊢ p ∈ zeroLocus s

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s = ⊤ → s ⊆ ↑(nilradical R)

Tactic:
intro h x hx

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
⊢ x ∈ ↑(nilradical R)

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
⊢ { asIdeal := J, isPrime := hJ } ∈ zeroLocus s

Tactic:
rw [h]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
⊢ { asIdeal := J, isPrime := hJ } ∈ ⊤

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
hJz : { asIdeal := J, isPrime := hJ } ∈ zeroLocus s
⊢ x ∈ J

Tactic:
exact (mem_zeroLocus _ _).mpr hJz hx

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
h : s ⊆ ↑(nilradical R)
p : PrimeSpectrum R
a✝ : p ∈ ⊤
⊢ p ∈ zeroLocus s

Tactic:
apply Set.Subset.trans h (nilradical_le_prime p.asIdeal)

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
⊢ x ∈ J

Tactic:
have hJz : ⟨J, hJ⟩ ∈ zeroLocus s := by
  rw [h]
  trivial

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
hJz : { asIdeal := J, isPrime := hJ } ∈ zeroLocus s
⊢ x ∈ J

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
⊢ { asIdeal := J, isPrime := hJ } ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
⊢ x ∈ ↑(nilradical R)

Tactic:
refine nilpotent_iff_mem_prime.mpr (fun J hJ ↦ ?_)

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
h : zeroLocus s = ⊤
x : R
hx : x ∈ s
J : Ideal R
hJ : J.IsPrime
⊢ x ∈ J

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical R)

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus s = ⊤ → s ⊆ ↑(nilradical R)

case mpr
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ s ⊆ ↑(nilradical R) → zeroLocus s = ⊤
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_mono_fun {f g : α →ₛ ℝ≥0∞} (h : f ≤ g) : f.lintegral μ ≤ g.lintegral μ

Proof state:
case h.bc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
i✝ : ℝ≥0∞ × ℝ≥0∞
a✝ : i✝ ∈ (f.pair g).range
⊢ i✝.1 ≤ i✝.1 ⊔ i✝.2

Tactic:
exact le_sup_left

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ (map Prod.fst (f.pair g)).lintegral μ ≤ (map (fun p => p.1 ⊔ p.2) (f.pair g)).lintegral μ

Tactic:
simp only [map_lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) ≤ ∑ x ∈ (f.pair g).range, (x.1 ⊔ x.2) * μ (⇑(f.pair g) ⁻¹' {x})

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range, x.1 * μ (⇑(f.pair g) ⁻¹' {x}) ≤ ∑ x ∈ (f.pair g).range, (x.1 ⊔ x.2) * μ (⇑(f.pair g) ⁻¹' {x})

Tactic:
gcongr

Result:
case h.bc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
i✝ : ℝ≥0∞ × ℝ≥0∞
a✝ : i✝ ∈ (f.pair g).range
⊢ i✝.1 ≤ i✝.1 ⊔ i✝.2

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ (fun x => x.lintegral μ) f ≤ (fun x => x.lintegral μ) (f ⊔ g)

Tactic:
calc
  f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
  _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
    simp only [map_lintegral]
    gcongr
    exact le_sup_left

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₛ ℝ≥0∞
h : f✝ ≤ g✝
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ

Tactic:
rw [map_fst_pair]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem lookupAll_nodup (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : (lookupAll a l).Nodup

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).Nodup

Tactic:
rw [lookupAll_eq_dlookup a h]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).Nodup

Tactic:
(rw [lookupAll_eq_dlookup a h]; apply Option.toList_nodup)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup

Tactic:
apply Option.toList_nodup

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
lemma shiftIso_add_inv_app (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).inv.app X =
      (F.shiftIso n a a' ha').inv.app X ≫
      ((F.shiftIso m a' a'' ha'').inv.app X)⟦n⟧' ≫
      (shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso (m + n) a a'' ⋯).inv.app X =
    (F.shiftIso n a a' ha').inv.app X ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫
        (shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{?u.9398, u_1} C
inst✝⁶ : Category.{?u.9402, u_2} D
inst✝⁵ : Category.{?u.9406, u_3} E
inst✝⁴ : Category.{?u.9410, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem qRight_one_left (θ : I) : qRight (1, θ) = 1 :=
  Set.projIcc_of_right_le _ <|
    (le_div_iff₀ <| add_pos zero_lt_one).2 <| by
      dsimp only
      rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]
      simp only [add_le_add_iff_right]
      exact le_one _

Proof state:
θ : ↑I
⊢ 1 * (1 + ↑(1, θ).2) ≤ 2 * ↑(1, θ).1

Tactic:
dsimp only

Result:
θ : ↑I
⊢ 1 * (1 + ↑θ) ≤ 2 * ↑1

Proof state:
θ : ↑I
⊢ 1 * (1 + ↑θ) ≤ 2 * ↑1

Tactic:
rw [coe_one, one_mul, mul_one, add_comm, ← one_add_one_eq_two]

Result:
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1

Proof state:
θ : ↑I
⊢ ↑θ ≤ 1

Tactic:
exact le_one _

Result:
no goals

Proof state:
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1

Tactic:
simp only [add_le_add_iff_right]

Result:
θ : ↑I
⊢ ↑θ ≤ 1
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma not_even_and_odd [NeZero (2 : S)] : ¬(ψ.Even ∧ ψ.Odd)

Proof state:
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NeZero 2
⊢ ¬(ψ.Even ∧ ψ.Odd)

Tactic:
rintro ⟨(h : _ = 1), (h' : _ = -1)⟩

Result:
case intro
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NeZero 2
h : ψ (-1) = 1
h' : ψ (-1) = -1
⊢ False

Proof state:
case intro
S : Type u_2
inst✝¹ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
inst✝ : NeZero 2
h : ψ (-1) = 1
h' : ψ (-1) = -1
⊢ False

Tactic:
simp only [h', neg_eq_iff_add_eq_zero, one_add_one_eq_two, two_ne_zero] at h

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_zero_of_frequently_zero (hf : GrowsPolynomially f) (hf' : ∃ᶠ x in atTop, f x = 0) :
    ∀ᶠ x in atTop, f x = 0

Proof state:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ x ⊔ 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ 2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1) ≤ x / x₀

Tactic:
refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
  (by positivity)).mp ?_

Result:
f : ℝ → ℝ
hf✝ : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ x ⊔ 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z → z ∈ Set.Icc (2 ^ (-↑m - 1) * x₀) (2 ^ (-↑m) * x₀) → f z = 0
⊢ logb 2 (2 ^ (-↑⌊-logb 2 (x / x₀)⌋₊ - 1)) ≤ logb 2 (x / x₀)
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem irreducible_of_mirror (h1 : ¬IsUnit f)
    (h2 : ∀ k, f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror)
    (h3 : IsRelPrime f f.mirror) : Irreducible f

Proof state:
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h

Tactic:
let k := g * h.mirror

Result:
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ IsUnit g ∨ IsUnit h

Proof state:
case isUnit_or_isUnit'.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inr (h3 h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))

Result:
no goals

Proof state:
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
have hk := h2 k key

Result:
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
⊢ IsUnit g ∨ IsUnit h

Proof state:
case isUnit_or_isUnit'.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inl (h3 g_dvd_f (by rwa [← hk]))

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem hasDerivAt_resolvent {a : A} {k : 𝕜} (hk : k ∈ ρ a) :
    HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Tactic:
have H₁ : HasFDerivAt Ring.inverse _ (↑ₐ k - a) := hasFDerivAt_ring_inverse (𝕜 := 𝕜) hk.unit

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    (↑ₐ k - a)
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    (↑ₐ k - a)
⊢ HasDerivAt (fun k => ↑ₐ k - a) 1 k

Tactic:
simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    (↑ₐ k - a)
H₂ : HasDerivAt (fun k => ↑ₐ k - a) 1 k
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Tactic:
simpa [resolvent, sq, hk.unit_spec, ← Ring.inverse_unit hk.unit] using H₁.comp_hasDerivAt k H₂

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    (↑ₐ k - a)
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

Tactic:
have H₂ : HasDerivAt (fun k => ↑ₐ k - a) 1 k := by
  simpa using (Algebra.linearMap 𝕜 A).hasDerivAt.sub_const a

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
k : 𝕜
hk : k ∈ ρ a
H₁ :
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹)
    (↑ₐ k - a)
H₂ : HasDerivAt (fun k => ↑ₐ k - a) 1 k
⊢ HasDerivAt (resolvent a) (-resolvent a k ^ 2) k