harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
theorem Subgraph.spanningCoe_sup_edge_le {H : Subgraph (G ⊔ edge s t)} (h : ¬ H.Adj s t) :
    H.spanningCoe ≤ G

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
⊢ G.Adj v w

Tactic:
have := hvw.adj_sub

Result:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
this : (G ⊔ edge s t).Adj v w
⊢ G.Adj v w

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
this : (G ⊔ edge s t).Adj v w
⊢ G.Adj v w

Tactic:
simp only [Subgraph.spanningCoe_adj, SimpleGraph.sup_adj, SimpleGraph.edge_adj] at *

Result:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ G.Adj v w

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : s(v, w) = s(s, t)
⊢ G.Adj v w

Tactic:
exact (h ((Subgraph.adj_congr_of_sym2 hs).mp hvw)).elim

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
⊢ G.Adj v w

Tactic:
by_cases hs : s(v, w) = s(s, t)

Result:
case pos
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : s(v, w) = s(s, t)
⊢ G.Adj v w

case neg
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : ¬s(v, w) = s(s, t)
⊢ G.Adj v w

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.Adj v w
this : G.Adj v w ∨ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
hs : ¬s(v, w) = s(s, t)
⊢ G.Adj v w

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
⊢ H.spanningCoe ≤ G

Tactic:
intro v w hvw

Result:
V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
v w : V
hvw : H.spanningCoe.Adj v w
⊢ G.Adj v w
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_transpose : trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose = trace R M

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Tactic:
refine (cancel_right h).1 ?_

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
⊢ (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e = trace R M ∘ₗ ↑e

Proof state:
case a.h.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
f : Dual R M
m : M
⊢ ((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e)) f) m =
    ((AlgebraTensorModule.curry (trace R M ∘ₗ ↑e)) f) m

Tactic:
simp [e]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Tactic:
let e := dualTensorHomEquiv R M M

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
⊢ (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e = trace R M ∘ₗ ↑e

Tactic:
ext f m

Result:
case a.h.h
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
f : Dual R M
m : M
⊢ ((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ ↑e)) f) m =
    ((AlgebraTensorModule.curry (trace R M ∘ₗ ↑e)) f) m
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_inv_cancel (h0 : a ≠ 0) (ht : a ≠ ∞) : a * a⁻¹ = 1

Proof state:
a : ℝ≥0∞
h0 : a ≠ 0
ht : a ≠ ⊤
⊢ a * a⁻¹ = 1

Tactic:
lift a to ℝ≥0 using ht

Result:
case intro
a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1

Proof state:
case intro
a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1

Tactic:
norm_cast at h0

Result:
case intro
a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1

Proof state:
case intro
a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ h0

Result:
no goals

Proof state:
case intro
a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1

Tactic:
norm_cast

Result:
case intro
a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_self (P : Fin 3 → R) : W'.addX P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addX P P = 0

Tactic:
rw [addX]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * P y ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * P y * P z + 2 * P x * P y * P y * P z -
                            W'.a₁ * P x ^ 2 * P y * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * P y * P z ^ 2 -
                2 * W'.a₃ * P x * P y * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * P y ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * P y * P z + 2 * P x * P y * P y * P z -
                            W'.a₁ * P x ^ 2 * P y * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * P y * P z ^ 2 -
                2 * W'.a₃ * P x * P y * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem valuation_unit (a : Aˣ) : A.valuation a = 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a

Tactic:
use a

Result:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ↑↑a * 1 = ↑↑a

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ A.valuation ↑↑a = 1

Tactic:
rw [← A.valuation.map_one, valuation_eq_iff]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a

Proof state:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ↑↑a * 1 = ↑↑a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_monomial {i : σ} :
    pderiv i (monomial s a) = monomial (s - single i 1) (a * s i)

Proof state:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (s.sum fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) =
    (monomial (s - single i 1)) (a * ↑(s i))

Tactic:
refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_

Result:
case refine_1
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
x✝ : j ∈ s.support
hne : j ≠ i
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) j (s j) = 0

case refine_2
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : i ∉ s.support
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) = 0

case refine_3
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) =
    (monomial (s - single i 1)) (a * ↑(s i))

Proof state:
case refine_2
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : i ∉ s.support
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) = 0

Tactic:
rw [Finsupp.not_mem_support_iff] at hi

Result:
case refine_2
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : s i = 0
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) = 0

Proof state:
case refine_1
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i j : σ
x✝ : j ∈ s.support
hne : j ≠ i
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) j (s j) = 0

Tactic:
simp [Pi.single_eq_of_ne hne]

Result:
no goals

Proof state:
case refine_3
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) =
    (monomial (s - single i 1)) (a * ↑(s i))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (pderiv i) ((monomial s) a) = (monomial (s - single i 1)) (a * ↑(s i))

Tactic:
simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
  ← (monomial _).map_smul]

Result:
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
⊢ (s.sum fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) =
    (monomial (s - single i 1)) (a * ↑(s i))

Proof state:
case refine_2
R : Type u
σ : Type v
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : σ
hi : s i = 0
⊢ (fun a_1 b => (monomial (s - single a_1 1)) (a * ↑b) * Pi.single i 1 a_1) i (s i) = 0

Tactic:
simp [hi]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- A uniform upper bound for `jacobiTheta₂_term` on compact subsets. -/
lemma norm_jacobiTheta₂_term_le {S T : ℝ} (hT : 0 < T) {z τ : ℂ}
    (hz : |im z| ≤ S) (hτ : T ≤ im τ) (n : ℤ) :
    ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * n ^ 2 - 2 * S * |n|))

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑n ^ 2 * T + -(2 * S * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im

Tactic:
refine add_le_add (mul_le_mul le_rfl hτ hT.le (sq_nonneg _)) ?_

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ -(2 * S * ↑|n|) ≤ 2 * ↑n * z.im

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ |↑n| * |z.im| ≤ |↑n| * S

Tactic:
exact mul_le_mul_of_nonneg_left hz (abs_nonneg _)

Result:
no goals

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ -(2 * S * ↑|n|) ≤ 2 * ↑n * z.im

Tactic:
rw [← mul_neg, mul_assoc, mul_assoc, mul_le_mul_left two_pos, mul_comm, neg_mul, ← mul_neg]

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑|n| * -S ≤ ↑n * z.im

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
simp_rw [norm_jacobiTheta₂_term, Real.exp_le_exp, sub_eq_add_neg, neg_mul, ← neg_add,
  neg_le_neg_iff, mul_comm (2 : ℝ), mul_assoc π, ← mul_add, mul_le_mul_left pi_pos,
  mul_comm T, mul_comm S]

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑n ^ 2 * T + -(2 * S * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑|n| * -S ≤ -|↑n * z.im|

Tactic:
rw [mul_neg, neg_le_neg_iff, abs_mul, Int.cast_abs]

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ |↑n| * |z.im| ≤ |↑n| * S

Proof state:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑|n| * -S ≤ ↑n * z.im

Tactic:
refine le_trans ?_ (neg_abs_le _)

Result:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑|n| * -S ≤ -|↑n * z.im|
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem back_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : a = b

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : [a] = [b]
⊢ a = b

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
a b : α
ys : Array α
toList✝ : List α
h : { toList := toList✝ }.push a = ys.push b
⊢ a = b

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.push a = { toList := toList✝ }.push b
⊢ a = b

Proof state:
α : Type u_1
a b : α
xs ys : Array α
h : xs.push a = ys.push b
⊢ a = b

Tactic:
cases xs

Result:
case mk
α : Type u_1
a b : α
ys : Array α
toList✝ : List α
h : { toList := toList✝ }.push a = ys.push b
⊢ a = b

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.push a = { toList := toList✝ }.push b
⊢ a = b

Tactic:
simp only [List.push_toArray, mk.injEq] at h

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ a = b

Proof state:
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ [a].length = [b].length

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ a = b

Tactic:
replace h := List.append_inj_right' h (by simp)

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : [a] = [b]
⊢ a = b
-- Mathlib/GroupTheory/Perm/Support.lean
theorem set_support_inv_eq : { x | p⁻¹ x ≠ x } = { x | p x ≠ x }

Proof state:
α : Type u_1
p : Perm α
⊢ {x | p⁻¹ x ≠ x} = {x | p x ≠ x}

Tactic:
ext x

Result:
case h
α : Type u_1
p : Perm α
x : α
⊢ x ∈ {x | p⁻¹ x ≠ x} ↔ x ∈ {x | p x ≠ x}

Proof state:
case h
α : Type u_1
p : Perm α
x : α
⊢ x ∈ {x | p⁻¹ x ≠ x} ↔ x ∈ {x | p x ≠ x}

Tactic:
simp only [Set.mem_setOf_eq, Ne]

Result:
case h
α : Type u_1
p : Perm α
x : α
⊢ ¬p⁻¹ x = x ↔ ¬p x = x

Proof state:
case h
α : Type u_1
p : Perm α
x : α
⊢ ¬p⁻¹ x = x ↔ ¬p x = x

Tactic:
rw [inv_def, symm_apply_eq, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map'_comp_map {f : α → C} {g h : β → C} [HasProduct f] [HasProduct g] [HasProduct h]
    (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b) (q' : ∀ (b : β), g b ⟶ h b) :
    Pi.map' p q ≫ Pi.map q' = Pi.map' p (fun b => q b ≫ q' b)

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun b => q b ≫ q' b

Tactic:
ext

Result:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
b✝ : β
⊢ (map' p q ≫ map q') ≫ π h b✝ = (map' p fun b => q b ≫ q' b) ≫ π h b✝

Proof state:
case h
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
b✝ : β
⊢ (map' p q ≫ map q') ≫ π h b✝ = (map' p fun b => q b ≫ q' b) ≫ π h b✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem toReal_add {x y : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) (hy : y ≠ ⊤) (h'y : y ≠ ⊥) :
    toReal (x + y) = toReal x + toReal y

Proof state:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x + y).toReal = x.toReal + y.toReal

Tactic:
lift x to ℝ using ⟨hx, h'x⟩

Result:
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x + y).toReal = (↑x).toReal + y.toReal

Proof state:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x + ↑y).toReal = (↑x).toReal + (↑y).toReal

Tactic:
rfl

Result:
no goals

Proof state:
case intro
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x + y).toReal = (↑x).toReal + y.toReal

Tactic:
lift y to ℝ using ⟨hy, h'y⟩

Result:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h'y : ↑y ≠ ⊥
⊢ (↑x + ↑y).toReal = (↑x).toReal + (↑y).toReal
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem δ_comp_σ_succ {n} {i : Fin (n + 1)} : δ i.succ ≫ σ i = 𝟙 (mk n)

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 (mk n)

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (Paths.of.map (FreeSimplexQuiver.Hom.δ i.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i))
    (𝟙 (mk n).as)

Proof state:
case h
n : ℕ
i : Fin (n + 1)
⊢ FreeSimplexQuiver.homRel (Paths.of.map (FreeSimplexQuiver.Hom.δ i.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i))
    (𝟙 (mk n).as)

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_succ

Result:
no goals
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
lemma doubleFactorial_le_factorial : ∀ n, n‼ ≤ n !
  | 0 => le_rfl
  | n + 1 => by
    rw [factorial_eq_mul_doubleFactorial]; exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos

Proof state:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)!

Tactic:
rw [factorial_eq_mul_doubleFactorial]

Result:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)‼ * n‼

Proof state:
n : ℕ
⊢ (n + 1)‼ ≤ (n + 1)‼ * n‼

Tactic:
exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The L-function of an even Dirichlet character vanishes at strictly negative even integers. -/
@[simp]
lemma Even.LFunction_neg_two_mul_nat {χ : DirichletCharacter ℂ N} (hχ : Even χ) (n : ℕ) [NeZero n] :
    LFunction χ (-(2 * n)) = 0

Proof state:
N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst✝ : NeZero n
⊢ LFunction χ (-(2 * ↑n)) = 0

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)

Result:
case intro
N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
m : ℕ
inst✝ : NeZero m.succ
⊢ LFunction χ (-(2 * ↑m.succ)) = 0

Proof state:
case intro
N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
m : ℕ
inst✝ : NeZero m.succ
⊢ LFunction χ (-(2 * ↑m.succ)) = 0

Tactic:
exact_mod_cast hχ.LFunction_neg_two_mul_nat_add_one m

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_norm_sub_rev {S : AddSubgroup M} (x y : M ⧸ S) : ‖x - y‖ = ‖y - x‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x - y‖ = ‖y - x‖

Tactic:
rw [← neg_sub, quotient_norm_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
lemma integral_congr_ae₂ {β : Type*} {_ : MeasurableSpace β} {ν : Measure β} {f g : α → β → G}
    (h : ∀ᵐ a ∂μ, f a =ᵐ[ν] g a) :
    ∫ a, ∫ b, f a b ∂ν ∂μ = ∫ a, ∫ b, g a b ∂ν ∂μ

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
⊢ ∫ (a : α), ∫ (b : β), f a b ∂ν ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂ν ∂μ

Tactic:
apply integral_congr_ae

Result:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
⊢ (fun a => ∫ (b : β), f a b ∂ν) =ᶠ[ae μ] fun a => ∫ (b : β), g a b ∂ν

Proof state:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a✝ : α
ha : f a✝ =ᶠ[ae ν] g a✝
⊢ ∫ (b : β), f a✝ b ∂ν = ∫ (b : β), g a✝ b ∂ν

Tactic:
apply integral_congr_ae

Result:
case h.h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a✝ : α
ha : f a✝ =ᶠ[ae ν] g a✝
⊢ f a✝ =ᶠ[ae ν] g a✝

Proof state:
case h.h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a✝ : α
ha : f a✝ =ᶠ[ae ν] g a✝
⊢ f a✝ =ᶠ[ae ν] g a✝

Tactic:
filter_upwards [ha] with _ hb using hb

Result:
no goals

Proof state:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
⊢ (fun a => ∫ (b : β), f a b ∂ν) =ᶠ[ae μ] fun a => ∫ (b : β), g a b ∂ν

Tactic:
filter_upwards [h] with _ ha

Result:
case h
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a✝ : α
ha : f a✝ =ᶠ[ae ν] g a✝
⊢ ∫ (b : β), f a✝ b ∂ν = ∫ (b : β), g a✝ b ∂ν