harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Monotone/Basic.lean
theorem antitoneOn_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ AntitoneOn f s

Tactic:
rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_mul [Mul α] [Small α] (x y : α) :
    equivShrink α (x * y) = equivShrink α x * equivShrink α y

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y

Tactic:
rw [Equiv.mul_def]

Result:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x * y) =
    (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) * (equivShrink α).symm ((equivShrink α) y))

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ (equivShrink α) (x * y) =
    (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) * (equivShrink α).symm ((equivShrink α) y))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_eq_empty_iff {f : ι → α} : range f = ∅ ↔ IsEmpty ι

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι

Tactic:
rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
lemma ofSubtype_support_disjoint {σ : Perm α} (x : Perm (Function.fixedPoints σ)) :
    _root_.Disjoint x.ofSubtype.support σ.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ ∀ a ∈ (ofSubtype x).support, ∀ b ∈ σ.support, a ≠ b

Tactic:
rintro a ha b hb rfl

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : a ∈ (ofSubtype x).support
hb : a ∈ σ.support
⊢ False

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ _root_.Disjoint (ofSubtype x).support σ.support

Tactic:
rw [Finset.disjoint_iff_ne]

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
⊢ ∀ a ∈ (ofSubtype x).support, ∀ b ∈ σ.support, a ≠ b

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : a ∈ (ofSubtype x).support
hb : a ∈ σ.support
⊢ False

Tactic:
rw [mem_support] at ha hb

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : (ofSubtype x) a ≠ a
hb : σ a ≠ a
⊢ False

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
x : Perm ↑(fixedPoints ⇑σ)
a : α
ha : (ofSubtype x) a ≠ a
hb : σ a ≠ a
⊢ False

Tactic:
exact ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : getEntry? a (insertEntryIfNew k v l) =
      if k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getEntry? a (insertEntryIfNew k v l) = if (k == a && !false) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [insertEntryIfNew_of_containsKey_eq_false h, getEntry?_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getEntry? a (insertEntryIfNew k v l) = if (k == a && !containsKey k l) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getEntry? a (insertEntryIfNew k v l) = if (k == a && !false) = true then some ⟨k, v⟩ else getEntry? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getEntry? a (insertEntryIfNew k v l) = if (k == a && !true) = true then some ⟨k, v⟩ else getEntry? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getEntry? a (insertEntryIfNew k v l) = if (k == a && !true) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [insertEntryIfNew_of_containsKey h]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem covBy_iff_le_iff_lt_right {x y : α} : x ⋖ y ↔ ∀ {z}, y ≤ z ↔ x < z

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ x ⋖ y ↔ ∀ {z : α}, y ≤ z ↔ x < z

Tactic:
simp_rw [covBy_iff_lt_iff_le_right, iff_comm]

Result:
no goals
-- Mathlib/Analysis/Complex/RemovableSingularity.lean
theorem tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO {f : ℂ → E} {c : ℂ}
    (hd : ∀ᶠ z in 𝓝[≠] c, DifferentiableAt ℂ f z)
    (ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹) :
    Tendsto f (𝓝[≠] c) (𝓝 <| limUnder (𝓝[≠] c) f)

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Tactic:
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
  (hz.1 hz.2).differentiableWithinAt

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Tactic:
rw [eventually_nhdsWithin_iff] at hd

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Tactic:
have H := differentiableOn_update_limUnder_of_isLittleO hd this ho

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H : DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H : DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))

Tactic:
exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prevn : ∀ {s}, Valid s → s.toString.1 = m₁.reverse ++ m₂ →
    ∀ n, s.prevn n ⟨utf8Len m₁⟩ = ⟨utf8Len (m₁.drop n)⟩
  | _, h, e => by
    let ⟨l, m, r, h⟩ := h.validFor
    simp only [h.toString] at e; subst e; simp [h.prevn]

Proof state:
m₂ m₁ : List Char
x✝ : Substring
h : x✝.Valid
e : x✝.toString.data = m₁.reverse ++ m₂
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Tactic:
let ⟨l, m, r, h⟩ := h.validFor

Result:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁.reverse ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Proof state:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁.reverse ++ m₂) r x✝
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Tactic:
simp [h.prevn]

Result:
no goals

Proof state:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁.reverse ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Tactic:
simp only [h.toString] at e

Result:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁.reverse ++ m₂
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Proof state:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁.reverse ++ m₂
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }

Tactic:
subst e

Result:
m₂ m₁ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁.reverse ++ m₂) r x✝
⊢ ∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_prime (R : Type*) [Ring R] (p : ℕ) [hp : Fact p.Prime] :
    cyclotomic p R = ∑ i ∈ Finset.range p, X ^ i

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p R = ∑ i ∈ range p, X ^ i

Tactic:
suffices cyclotomic p ℤ = ∑ i ∈ range p, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    congr_arg (map (Int.castRingHom R)) this

Result:
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i ∈ range p, X ^ i

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
this : cyclotomic p ℤ = ∑ i ∈ range p, X ^ i
⊢ cyclotomic p R = ∑ i ∈ range p, X ^ i

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  congr_arg (map (Int.castRingHom R)) this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i ∈ range p, X ^ i

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
  erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem coe_toDual_self (i : ι) : b.toDual (b i) = b.coord i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
⊢ b.toDual (b i) = b.coord i

Tactic:
ext

Result:
case h
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
x✝ : M
⊢ (b.toDual (b i)) x✝ = (b.coord i) x✝

Proof state:
case h
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
x✝ : M
⊢ (b.toDual (b i)) x✝ = (b.coord i) x✝

Tactic:
apply toDual_apply_right

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_norm_eq_zero_iff (S : AddSubgroup M) (m : M) :
    ‖mk' S m‖ = 0 ↔ m ∈ closure (S : Set M)

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ (↑S).Nonempty

Tactic:
exact ⟨0, S.zero_mem⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ‖(mk' S) m‖ = 0 ↔ m ∈ closure ↑S

Tactic:
rw [mk'_apply, norm_mk, ← mem_closure_iff_infDist_zero]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ (↑S).Nonempty
-- Mathlib/ModelTheory/Graph.lean
theorem _root_.SimpleGraph.simpleGraphOfStructure (G : SimpleGraph V) :
    @simpleGraphOfStructure V G.structure _ = G

Proof state:
V : Type u
G : SimpleGraph V
⊢ FirstOrder.Language.simpleGraphOfStructure V = G

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (FirstOrder.Language.simpleGraphOfStructure V).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (FirstOrder.Language.simpleGraphOfStructure V).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_true_subtype {x : Subtype P} : Minimal (fun _ ↦ True) x ↔ Minimal P x

Proof state:
case mk
α : Type u_1
P : α → Prop
inst✝ : LE α
x : α
hx : P x
⊢ Minimal (fun x => True) ⟨x, hx⟩ ↔ Minimal P ↑⟨x, hx⟩

Tactic:
simp [Minimal, hx]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
inst✝ : LE α
x : Subtype P
⊢ Minimal (fun x => True) x ↔ Minimal P ↑x

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
α : Type u_1
P : α → Prop
inst✝ : LE α
x : α
hx : P x
⊢ Minimal (fun x => True) ⟨x, hx⟩ ↔ Minimal P ↑⟨x, hx⟩
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem to_global_factors :
    toOpen R ⊤ =
      CommRingCat.ofHom (algebraMap R (Localization.Away (1 : R))) ≫
        CommRingCat.ofHom (toBasicOpen R (1 : R)) ≫
        (structureSheaf R).1.map (eqToHom PrimeSpectrum.basicOpen_one.symm).op

Proof state:
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    (CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ CommRingCat.ofHom (toBasicOpen R 1)) ≫
      (structureSheaf R).val.map (eqToHom ⋯).op

Tactic:
change toOpen R ⊤ =
  (CommRingCat.ofHom <| (toBasicOpen R 1).comp (algebraMap R (Localization.Away 1))) ≫
  (structureSheaf R).1.map (eqToHom _).op

Result:
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom ((toBasicOpen R 1).comp (algebraMap R (Localization.Away 1))) ≫
      (structureSheaf R).val.map (eqToHom ⋯).op

Proof state:
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom ((toBasicOpen R 1).comp (algebraMap R (Localization.Away 1))) ≫
      (structureSheaf R).val.map (eqToHom ⋯).op

Tactic:
rw [localization_toBasicOpen R, CommRingCat.ofHom_hom, toOpen_res]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫
      CommRingCat.ofHom (toBasicOpen R 1) ≫ (structureSheaf R).val.map (eqToHom ⋯).op

Tactic:
rw [← Category.assoc]

Result:
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    (CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ CommRingCat.ofHom (toBasicOpen R 1)) ≫
      (structureSheaf R).val.map (eqToHom ⋯).op
-- Mathlib/Control/Traversable/Basic.lean
theorem preserves_map {α β} (x : α → β) (y : F α) : η (x <$> y) = x <$> η y

Proof state:
F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y

Tactic:
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.inter {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁)
    (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∩ s₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∩ s₂)

Tactic:
rw [inter_eq_compl_compl_union_compl]

Result:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ

Tactic:
exact (h₁.compl.union h₂.compl).compl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modifyHead_zero {l : List α} {f : α → α} {h} :
    (l.modifyHead f)[0] = f (l[0]'(by simpa using h))

Proof state:
α : Type ?u.2789
l : List α
f : α → α
h : 0 < (modifyHead f l).length
⊢ 0 < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
f : α → α
h : 0 < (modifyHead f l).length
⊢ (modifyHead f l)[0] = f l[0]

Tactic:
simp [getElem_modifyHead]

Result:
no goals
-- Mathlib/Order/PartialSups.lean
theorem iSup_eq_iSup_of_partialSups_eq_partialSups {f g : ι → α}
    (h : partialSups f = partialSups g) : ⨆ i, f i = ⨆ i, g i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f = partialSups g
⊢ ⨆ i, f i = ⨆ i, g i

Tactic:
simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_drop_append_take {l : List α} {n : ℕ} :
    n ≤ l.length → l.rotate n = l.drop n ++ l.take n

Proof state:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l

Tactic:
exact rotate'_eq_drop_append_take

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate n = drop n l ++ take n l

Tactic:
rw [rotate_eq_rotate']

Result:
α : Type u
l : List α
n : ℕ
⊢ n ≤ l.length → l.rotate' n = drop n l ++ take n l
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Path u v) :
    p.cast hu hv = _root_.cast (by rw [hu, hv]) p

Proof state:
U : Type u_1
inst✝ : Quiver U
u' v' : U
p : Path u' v'
⊢ cast ⋯ ⋯ p = _root_.cast ⋯ p

Tactic:
rfl

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'

Tactic:
rw [hu, hv]

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p = _root_.cast ⋯ p

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u' v' : U
p : Path u' v'
⊢ cast ⋯ ⋯ p = _root_.cast ⋯ p
-- Mathlib/Data/ZMod/Basic.lean
theorem val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n

Proof state:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

Tactic:
rw [Nat.mod_zero]

Result:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val

Proof state:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
apply Fin.val_mul

Result:
no goals

Proof state:
n : ℕ
a b : ZMod n
⊢ (a * b).val = a.val * b.val % n

Tactic:
cases n

Result:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Proof state:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val

Tactic:
apply Int.natAbs_mul

Result:
no goals
-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem matrixEquivTensor_apply_stdBasisMatrix (i j : n) (x : A) :
    matrixEquivTensor n R A (stdBasisMatrix i j x) = x ⊗ₜ stdBasisMatrix i j 1

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)

Tactic:
aesop

Result:
no goals

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ (matrixEquivTensor n R A) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1

Tactic:
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop

Result:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)
⊢ (matrixEquivTensor n R A) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)
⊢ (matrixEquivTensor n R A) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1

Tactic:
simp [ite_tmul, t, stdBasisMatrix]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem compl₂_id : f.compl₂ LinearMap.id = f

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
R₂ : Type u_2
inst✝⁷ : CommSemiring R₂
R₃ : Type u_3
inst✝⁶ : CommSemiring R₃
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R₂ N
inst✝ : Module R₃ P
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
⊢ f.compl₂ id = f

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝⁸ : CommSemiring R
R₂ : Type u_2
inst✝⁷ : CommSemiring R₂
R₃ : Type u_3
inst✝⁶ : CommSemiring R₃
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R₂ N
inst✝ : Module R₃ P
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ((f.compl₂ id) x✝¹) x✝ = (f x✝¹) x✝

Proof state:
case h.h
R : Type u_1
inst✝⁸ : CommSemiring R
R₂ : Type u_2
inst✝⁷ : CommSemiring R₂
R₃ : Type u_3
inst✝⁶ : CommSemiring R₃
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R₂ N
inst✝ : Module R₃ P
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ((f.compl₂ id) x✝¹) x✝ = (f x✝¹) x✝

Tactic:
rw [compl₂_apply, id_coe, _root_.id]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem comp_left_bot (r : Rel α β) : (⊥ : Rel γ α) • r = ⊥

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
⊢ ⊥ • r = ⊥

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : γ
y : β
⊢ (⊥ • r) x y ↔ ⊥ x y

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
x : γ
y : β
⊢ (⊥ • r) x y ↔ ⊥ x y

Tactic:
simp [comp, Bot.bot]

Result:
no goals