harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Monotone.lean
theorem Monotone.ae_hasDerivAt {f : ℝ → ℝ} (hf : Monotone f) :
    ∀ᵐ x, HasDerivAt f (rnDeriv hf.stieltjesFunction.measure volume x).toReal x

Proof state:
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y ∈ Ioo (x - 1) x
⊢ y + -1 * (y - x) ^ 2 ∈ Iio x

Tactic:
rw [mem_Ioo] at hy

Result:
case h
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b => (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : x - 1 < y ∧ y < x
⊢ y + -1 * (y - x) ^ 2 ∈ Iio x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equiv_iff_eq_of_Z_eq' {P Q : Fin 3 → R} (hz : P z = Q z) (mem : Q z ∈ nonZeroDivisors R) :
    P ≈ Q ↔ P = Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = 1 * Q z
⊢ (fun m => m • Q) u = Q

Tactic:
simp_rw [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors mem).mp hz, one_smul]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
P : Fin 3 → R
hz : P z = P z
mem : P z ∈ nonZeroDivisors R
⊢ P ≈ P

Tactic:
exact Setoid.refl _

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = Q z
⊢ (fun m => m • Q) u = Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = Q z
⊢ (fun m => m • Q) u = Q

Tactic:
rw [← one_mul (Q z)] at hz

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = 1 * Q z
⊢ (fun m => m • Q) u = Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P = Q → P ≈ Q

Tactic:
rintro rfl

Result:
R : Type r
inst✝ : CommRing R
P : Fin 3 → R
hz : P z = P z
mem : P z ∈ nonZeroDivisors R
⊢ P ≈ P

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, by rintro rfl; exact Setoid.refl _⟩

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[ext 900]
lemma ext_dual [H : SeparatingDual 𝕜 F] {A B : E →WOT[𝕜] F}
    (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
H : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)
⊢ A = B

Tactic:
simp_rw [ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff, LinearMap.ext_iff]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
H : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)
⊢ ∀ (x : E) (x_1 : F →L[𝕜] 𝕜),
    ((ContinuousLinearMap.coeLM 𝕜).flip (A x)) x_1 = ((ContinuousLinearMap.coeLM 𝕜).flip (B x)) x_1

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
H : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)
⊢ ∀ (x : E) (x_1 : F →L[𝕜] 𝕜),
    ((ContinuousLinearMap.coeLM 𝕜).flip (A x)) x_1 = ((ContinuousLinearMap.coeLM 𝕜).flip (B x)) x_1

Tactic:
exact h

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_to_generateFrom_iff {β : Type*} {T : Set (Set β)} {f : α → β} :
    @ContinuousOn α β _ (.generateFrom T) f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x :=
  forall₂_congr fun x _ => by
    delta ContinuousWithinAt
    simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
      and_imp]
    exact forall_congr' fun t => forall_swap

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_setOf_eq,
  and_imp]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
exact forall_congr' fun t => forall_swap

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
delta ContinuousWithinAt

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected. -/
lemma IsSelfAdjoint.isConnected_spectrum_compl {a : A} (ha : IsSelfAdjoint a) :
    IsConnected (σ ℂ a)ᶜ

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ {z | 0 < z.im} ⊆ (σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}

Tactic:
refine Set.subset_inter (fun z hz hz' ↦ ?_) (fun _ ↦ by simpa using le_of_lt)

Result:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ {z | 0 < z.im}
hz' : z ∈ σ ℂ a
⊢ False

Proof state:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
rw [← Set.inter_univ (σ ℂ a)ᶜ]

Result:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)

Proof state:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ {z | 0 < z.im}
hz' : z ∈ σ ℂ a
⊢ False

Tactic:
rw [Set.mem_setOf_eq, ha.im_eq_zero_of_mem_spectrum hz'] at hz

Result:
case upper
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : 0 < 0
hz' : z ∈ σ ℂ a
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem extract_empty (start stop : Nat) :
    (#v[] : Vector α 0).extract start stop = #v[].cast (by simp)

Proof state:
α : Type u_1
start stop : Nat
⊢ { toArray := #[], size_toArray := ⋯ }.extract start stop = Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.410308
start stop : Nat
⊢ 0 = min stop 0 - start

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_le_mul_norm_add (u v : E) : ‖u‖ ≤ ‖u * v‖ + ‖v‖ :=
  calc
    ‖u‖ = ‖u * v / v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ = ‖u * v / v‖

Tactic:
rw [mul_div_cancel_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
private lemma tendsto_deriv_mul_log_nhdsWithin_zero :
    Tendsto (deriv (fun x ↦ x * log x)) (𝓝[>] 0) atBot

Proof state:
⊢ Tendsto (deriv fun x => x * log x) (𝓝[>] 0) atBot

Tactic:
have : (deriv (fun x ↦ x * log x)) =ᶠ[𝓝[>] 0] (fun x ↦ log x + 1) := by
  apply eventuallyEq_nhdsWithin_of_eqOn
  intro x hx
  rw [Set.mem_Ioi] at hx
  exact deriv_mul_log hx.ne'

Result:
this : (deriv fun x => x * log x) =ᶠ[𝓝[>] 0] fun x => log x + 1
⊢ Tendsto (deriv fun x => x * log x) (𝓝[>] 0) atBot

Proof state:
case h

⊢ Set.EqOn (deriv fun x => x * log x) (fun x => log x + 1) (Set.Ioi 0)

Tactic:
intro x hx

Result:
case h
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ deriv (fun x => x * log x) x = (fun x => log x + 1) x

Proof state:
case h
x : ℝ
hx : 0 < x
⊢ deriv (fun x => x * log x) x = (fun x => log x + 1) x

Tactic:
exact deriv_mul_log hx.ne'

Result:
no goals

Proof state:
case h
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ deriv (fun x => x * log x) x = (fun x => log x + 1) x

Tactic:
rw [Set.mem_Ioi] at hx

Result:
case h
x : ℝ
hx : 0 < x
⊢ deriv (fun x => x * log x) x = (fun x => log x + 1) x

Proof state:
this : (deriv fun x => x * log x) =ᶠ[𝓝[>] 0] fun x => log x + 1
⊢ Tendsto (deriv fun x => x * log x) (𝓝[>] 0) atBot

Tactic:
simp only [tendsto_congr' this, tendsto_atBot_add_const_right, tendsto_log_nhdsWithin_zero_right]

Result:
no goals

Proof state:
⊢ (deriv fun x => x * log x) =ᶠ[𝓝[>] 0] fun x => log x + 1

Tactic:
apply eventuallyEq_nhdsWithin_of_eqOn

Result:
case h

⊢ Set.EqOn (deriv fun x => x * log x) (fun x => log x + 1) (Set.Ioi 0)
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsNilpotent.isUnit_sub_one [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r - 1)

Proof state:
case intro.refine_2
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1

Tactic:
simp [geom_sum_mul, hn]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)

Tactic:
refine ⟨⟨r - 1, -∑ i ∈ Finset.range n, r ^ i, ?_, ?_⟩, rfl⟩

Result:
case intro.refine_1
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1

case intro.refine_2
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (-∑ i ∈ Finset.range n, r ^ i) * (r - 1) = 1

Proof state:
case intro.refine_1
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (r - 1) * -∑ i ∈ Finset.range n, r ^ i = 1

Tactic:
simp [mul_geom_sum, hn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
obtain ⟨n, hn⟩ := hnil

Result:
case intro
R : Type u_1
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)
-- Mathlib/Algebra/GroupWithZero/NeZero.lean
theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
  have := mul_inv_cancel₀ h
  simp only [a_eq_0, mul_zero, zero_ne_one] at this

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
⊢ False

Tactic:
have := mul_inv_cancel₀ h

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
this : a * a⁻¹ = 1
⊢ False

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
a_eq_0 : a⁻¹ = 0
this : a * a⁻¹ = 1
⊢ False

Tactic:
simp only [a_eq_0, mul_zero, zero_ne_one] at this

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem sum_mul_smul (n : ℕ) :
    (∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν) =
      (n * (n - 1)) • X ^ 2

Proof state:
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ ↑((k + 1 + 1) * (k + 1)) * (↑(n.choose (k + 1 + 1)) * (X ^ k * X * X) * (1 - X) ^ (n - (k + 1 + 1))) =
    ↑(n.choose (k + 1 + 1)) * ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1) * X ^ k))) * (X ^ 0 * X * X)

Tactic:
push_cast

Result:
case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
k : ℕ
⊢ (↑k + 1 + 1) * (↑k + 1) * (↑(n.choose (k + 1 + 1)) * (X ^ k * X * X) * (1 - X) ^ (n - (k + 1 + 1))) =
    ↑(n.choose (k + 1 + 1)) * ((1 - X) ^ (n - (k + 1 + 1)) * ((↑k + 1 + 1) * ((↑k + 1) * X ^ k))) * (X ^ 0 * X * X)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i => bif i then X else 1 - X
w :
  ∀ (k : ℕ),
    (k * (k - 1)) • bernsteinPolynomial R n k =
      ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2
k : ℕ
x✝ : k ∈ Finset.range (n + 1)
⊢ ↑(n.choose k) * ((1 - X) ^ (n - k) * (↑k * (↑(k - 1) * X ^ (k - 1 - 1)))) * X ^ 2 =
    (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) (x ^ k * y ^ (n - k) * ↑(n.choose k)))) * X ^ 2

Tactic:
simp only [x, y, e, pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul,
  Bool.cond_true, Bool.cond_false, add_zero, zero_add, mul_zero, smul_zero, mul_one,
  MvPolynomial.aeval_X, MvPolynomial.pderiv_X_self, MvPolynomial.pderiv_X_of_ne,
  Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow,
  map_mul, map_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
⊢ (pderiv true) y = 0

Tactic:
rw [pderiv_X]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
⊢ Pi.single true 1 false = 0
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_right_one : (· * b) ⁻¹' 1 = {b⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x => x * b) ⁻¹' 1 = {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem injective : Function.Injective a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬(↑c).Disjoint ↑d

Tactic:
simp only [Disjoint, not_forall, not_or]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ∃ x, ¬↑c x = x ∧ ¬↑d x = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ↑c = ↑d

Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint.eq c.prop d.prop

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬(↑c).Disjoint ↑d

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ c = d

Tactic:
rw [← Subtype.coe_inj]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ↑c = ↑d

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
⊢ Function.Injective ⇑a

Tactic:
intro c d h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ c = d

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ∃ x, ¬↑c x = x ∧ ¬↑d x = x

Tactic:
use a c

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a c) = a c

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a d) = a d

Tactic:
simp only [← Perm.mem_support, a.mem_support_self c, a.mem_support_self d, and_self]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a c) = a c

Tactic:
conv_rhs => rw [h]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : { x // x ∈ g.cycleFactorsFinset }
h : a c = a d
⊢ ¬↑c (a c) = a c ∧ ¬↑d (a d) = a d
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem eq_top_iff {S : StarSubalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
  ⟨fun h x => by rw [h]; exact mem_top,
  fun h => by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x

Result:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Result:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Submonoid M} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Submonoid M) : Set M) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma quasiIsoAt_πTruncGE {j : ι} {j' : ι'} (hj' : e.f j = j') :
    QuasiIsoAt (K.πTruncGE e) j'

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))

Tactic:
rw [(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff]

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ IsIso (truncGE.rightHomologyMapData K e hj' ⋯ ⋯ hj).φH
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem isBounded_image_iff {f : β → α} {s : Set β} :
    IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_image]

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
s : Set β
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ f '' s → ∀ ⦃y : α⦄, y ∈ f '' s → dist x y ≤ C) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

Tactic:
simp only [forall_mem_image]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem iSup_adj {f : ι → G.Subgraph} : (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
f : ι → G.Subgraph
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
lemma isIso_unit_app_iff_mem_essImage [R.Faithful] [R.Full] {Y : C} :
    IsIso (h.unit.app Y) ↔ R.essImage Y

Proof state:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)

Tactic:
rintro ⟨_, ⟨i⟩⟩

Result:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app Y)

Proof state:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app Y)

Tactic:
rw [NatTrans.isIso_app_iff_of_iso _ i.symm]

Result:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app (R.obj w✝))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) → R.essImage Y

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)

Proof state:
case mpr.intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app (R.obj w✝))

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
a✝ : IsIso (h.unit.app Y)
⊢ R.essImage Y

Tactic:
exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) → R.essImage Y

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
a✝ : IsIso (h.unit.app Y)
⊢ R.essImage Y