harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Permutation.lean
theorem map_map_permutations'Aux (f : α → β) (t : α) (ts : List α) :
    map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
t : α
⊢ map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)

Tactic:
induction' ts with a ts ih

Result:
case nil
α : Type u_1
β : Type u_2
f : α → β
t : α
⊢ map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])

case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f) (permutations'Aux t (a :: ts)) = permutations'Aux (f t) (map f (a :: ts))

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f) (permutations'Aux t (a :: ts)) = permutations'Aux (f t) (map f (a :: ts))

Tactic:
simp only [permutations'Aux, map_cons, map_map, ← ih, cons.injEq, true_and, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Convex/KreinMilman.lean
theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex ℝ s) :
    closure (convexHull ℝ <| s.extremePoints ℝ) = s

Proof state:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r
hrx : r < l x
⊢ False

Tactic:
have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩

Result:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r
hrx : r < l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}
⊢ False
-- Mathlib/CategoryTheory/Sites/Coverage.lean
lemma saturate_of_superset (K : Coverage C) {X : C} {S T : Sieve X} (h : S ≤ T)
    (hS : Saturate K X S) : Saturate K X T

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤

Tactic:
apply Saturate.top

Result:
no goals

Proof state:
case hf
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Tactic:
assumption

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
⊢ K.Saturate X T

Tactic:
apply Saturate.transitive _ _ _ hS

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f T)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y (Sieve.pullback g T)

Tactic:
rw [eq_top_pullback (h := h)]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y ⊤

case hf
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f T)

Tactic:
intro Y g hg

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y (Sieve.pullback g T)
-- Mathlib/Data/ENNReal/Inv.lean
@[simp] protected lemma inv_mul_le_one (a : ℝ≥0∞) : a⁻¹ * a ≤ 1

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ * a ≤ 1

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem ConvolutionExists.distrib_add (hfg : ConvolutionExists f g L μ)
    (hfg' : ConvolutionExists f g' L μ) : f ⋆[L, μ] (g + g') = f ⋆[L, μ] g + f ⋆[L, μ] g'

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g g' : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
x : G
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x

Tactic:
exact (hfg x).distrib_add (hfg' x)

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g g' : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
⊢ f ⋆[L, μ] (g + g') = f ⋆[L, μ] g + f ⋆[L, μ] g'

Tactic:
ext x

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g g' : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f g' L μ
x : G
⊢ (f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
/-- Also see `PrimeSpectrum.isClosed_singleton_iff_isMaximal` -/
lemma isMax_iff {x : PrimeSpectrum R} :
    IsMax x ↔ x.asIdeal.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := Ideal.exists_le_maximal I e

Result:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
m : Ideal R
hm : m.IsMaximal
hm' : I ≤ m
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
⊢ I = ⊤

Tactic:
by_contra e

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMax x ↔ x.asIdeal.IsMaximal

Tactic:
refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
⊢ I = ⊤

Proof state:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
hx : IsMax x
I : Ideal R
hI : x.asIdeal < I
e : ¬I = ⊤
m : Ideal R
hm : m.IsMaximal
hm' : I ≤ m
⊢ False

Tactic:
exact hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mul_div_assoc (x : R) {y z : R} (h : z ∣ y) : x * y / z = x * (y / z)

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)

Tactic:
subst hz

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ x * y / 0 = x * (y / 0)

Proof state:
case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)

Tactic:
rcases h with ⟨p, rfl⟩

Result:
case neg.intro
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * (z * p / z)

Proof state:
case neg.intro
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * (z * p / z)

Tactic:
rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ x * y / 0 = x * (y / 0)

Tactic:
rw [div_zero, div_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
⊢ x * y / z = x * (y / z)

Tactic:
by_cases hz : z = 0

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)

case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)
-- Mathlib/Data/Matroid/Closure.lean
lemma spanning_iff_exists_isBase_subset (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
rw [spanning_iff_exists_isBase_subset', and_iff_left hS]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_eq_one_iff_right₀ (ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a ^ n = 1 ↔ n = 0

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
⊢ a ^ n = 1 ↔ n = 0

Tactic:
obtain rfl | ha₀ := ha₀.eq_or_lt

Result:
case inl
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 ≤ 0
ha₁ : 0 ≠ 1
⊢ 0 ^ n = 1 ↔ n = 0

case inr
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0

Proof state:
case inl
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 ≤ 0
ha₁ : 0 ≠ 1
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
exact zero_zpow_eq_one₀

Result:
no goals

Proof state:
case inr
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀✝ : 0 ≤ a
ha₁ : a ≠ 1
n : ℤ
ha₀ : 0 < a
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simpa using zpow_right_inj₀ ha₀ ha₁ (n := 0)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval_eq_sum_range {p : R[X]} (x : R) :
    p.eval x = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

Tactic:
rw [eval_eq_sum, sum_over_range]

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
we are on the slitPlane. -/
lemma Complex.deriv_log_comp_eq_logDeriv {f : ℂ → ℂ} {x : ℂ} (h₁ : DifferentiableAt ℂ f x)
    (h₂ : f x ∈ Complex.slitPlane) : deriv (Complex.log ∘ f) x = logDeriv f x

Proof state:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv

Result:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun t => log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x

Proof state:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun t => log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
simp only [logDeriv, Pi.div_apply, ← A, Function.comp_def]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem isMax_iterate_succ_of_eq_of_lt {n m : ℕ} (h_eq : succ^[n] a = succ^[m] a)
    (h_lt : n < m) : IsMax (succ^[n] a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a

Tactic:
rw [← iterate_succ_apply' succ]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ^[n.succ] a ≤ succ^[m] a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ IsMax (succ^[n] a)

Tactic:
refine max_of_succ_le (le_trans ?_ h_eq.symm.le)

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem mem_sSup_of_mem {S : Set (Subsemigroup M)} {s : Subsemigroup M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
have : s ≤ sSup S := le_sSup hs

Result:
M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
tauto

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem maximal_false : ¬ Maximal (fun _ ↦ False) x

Proof state:
α : Type u_1
x : α
inst✝ : LE α
⊢ ¬Maximal (fun x => False) x

Tactic:
simp [Maximal]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem disconnect_isTotallyDisconnected : S.disconnect.IsTotallyDisconnected

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d

Tactic:
exact fun c d ⟨_, h, _⟩ => h

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect.IsTotallyDisconnected

Tactic:
rw [isTotallyDisconnected_iff]

Result:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma corootForm_apply_apply (x y : N) : P.CorootForm x y =
    ∑ i, P.root' i x * P.root' i y

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x y : N
⊢ (P.CorootForm x) y = ∑ i : ι, (P.root' i) x * (P.root' i) y

Tactic:
simp [CorootForm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem slope_vadd_const (f : k → E) (c : PE) : (slope fun x => f x +ᵥ c) = slope f

Proof state:
case h.h
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
c : PE
a b : k
⊢ slope (fun x => f x +ᵥ c) a b = slope f a b

Tactic:
simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub]

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
c : PE
⊢ (slope fun x => f x +ᵥ c) = slope f

Tactic:
ext a b

Result:
case h.h
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
c : PE
a b : k
⊢ slope (fun x => f x +ᵥ c) a b = slope f a b
-- Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean
@[simp]
lemma toSet_map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) :
    (s.map f).toSet = comap f ⁻¹' s.toSet

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq S
f : R →+* S
s : ConstructibleSetData R
⊢ (map f s).toSet = ⇑(comap f) ⁻¹' s.toSet

Tactic:
unfold toSet map

Result:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃
      x ∈
        image
          (fun x =>
            match x with
            | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩))
          s,
      zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1} =
    ⇑(comap f) ⁻¹' ⋃ x ∈ s, zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1}

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃
      x ∈
        image
          (fun x =>
            match x with
            | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩))
          s,
      zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1} =
    ⇑(comap f) ⁻¹' ⋃ x ∈ s, zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1}

Tactic:
rw [set_biUnion_finset_image]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ y ∈ s,
      zeroLocus
          (Set.range
            (match y with
                | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩)).2.snd) \
        zeroLocus
          {(match y with
              | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩)).1} =
    ⇑(comap f) ⁻¹' ⋃ x ∈ s, zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1}

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : DecidableEq S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ y ∈ s,
      zeroLocus
          (Set.range
            (match y with
                | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩)).2.snd) \
        zeroLocus
          {(match y with
              | (r, ⟨n, g⟩) => (f r, ⟨n, ⇑f ∘ g⟩)).1} =
    ⇑(comap f) ⁻¹' ⋃ x ∈ s, zeroLocus (Set.range x.2.snd) \ zeroLocus {x.1}

Tactic:
simp [← Set.range_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.integrable_of_lintegral_enorm_tendsto' [l.NeBot] [l.IsCountablyGenerated]
    {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → E} (I : ℝ≥0) (hfm : AEStronglyMeasurable f μ)
    (htendsto : Tendsto (fun i => ∫⁻ x in φ i, ‖f x‖ₑ ∂μ) l (𝓝 I)) : Integrable f μ :=
  hφ.integrable_of_lintegral_enorm_tendsto I hfm
    (by simpa only [ENNReal.ofReal_coe_nnreal] using htendsto)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 ↑I)
⊢ Tendsto (fun i => ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal ↑I))

Tactic:
simpa only [ENNReal.ofReal_coe_nnreal] using htendsto

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem tendsto_dist_right_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x => dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_nat_mul_pi_sub (x : ℝ) (n : ℕ) : sin (n * π - x) = -((-1) ^ n * sin x)

Proof state:
x : ℝ
n : ℕ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)

Tactic:
simpa only [sin_neg, mul_neg] using sin_antiperiodic.nat_mul_sub_eq n

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem comm_sq₂ (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :
    (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

Proof state:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

Tactic:
rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem cast_pos {n : ℕ} : IsNat (a : R) n → a = n.rawCast + 0
  | ⟨e⟩ => by simp [e]

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
n : ℕ
e : a = ↑n
⊢ a = n.rawCast + 0

Tactic:
simp [e]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- A version of `Matroid.indep_iff_forall_subset_not_isCircuit` that has the supportedness
hypothesis as part of the equivalence, rather than a hypothesis. -/
lemma indep_iff_forall_subset_not_isCircuit' :
    M.Indep I ↔ (∀ C, C ⊆ I → ¬M.IsCircuit C) ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
simp_rw [indep_iff_not_dep, dep_iff_superset_isCircuit']

Result:
α : Type u_1
M : Matroid α
I : Set α
⊢ ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ ¬((∃ C ⊆ I, M.IsCircuit C) ∧ I ⊆ M.E) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiff_of_subsingleton [Subsingleton F] : ContDiff 𝕜 n f

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiff 𝕜 n f

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiff 𝕜 n fun x => 0

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiff 𝕜 n fun x => 0

Tactic:
exact contDiff_const

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) :
    getKey? k (modifyKey k f l) = if containsKey k l then some k else none

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey? k (modifyKey k f l) = if containsKey k l = true then some k else none

Tactic:
simp [getKey?_modifyKey, hl]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem one_add_mul [RightDistribClass α] (a b : α) : (1 + a) * b = b + a * b

Proof state:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b

Tactic:
rw [add_mul, one_mul]

Result:
no goals