harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@[simp] lemma arg_toCircle (θ : Real.Angle) : (arg θ.toCircle : Angle) = θ

Proof state:
case h
x✝ : ℝ
⊢ ↑(↑(↑x✝).toCircle).arg = ↑x✝

Tactic:
rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
  Real.Angle.cos_coe, ← Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]

Result:
no goals

Proof state:
θ : Angle
⊢ ↑(↑θ.toCircle).arg = θ

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ ↑(↑(↑x✝).toCircle).arg = ↑x✝
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n

Proof state:
case succ
n : ℕ
ih : sign (finRotate (n + 1)) = (-1) ^ n
⊢ sign (decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ (n + 1)

Tactic:
simp [ih, pow_succ]

Result:
no goals

Proof state:
n : ℕ
⊢ sign (finRotate (n + 1)) = (-1) ^ n

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [finRotate_succ_eq_decomposeFin]
  simp [ih, pow_succ]

Result:
no goals

Proof state:
case zero

⊢ sign (finRotate (0 + 1)) = (-1) ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
ih : sign (finRotate (n + 1)) = (-1) ^ n
⊢ sign (finRotate (n + 1 + 1)) = (-1) ^ (n + 1)

Tactic:
rw [finRotate_succ_eq_decomposeFin]

Result:
case succ
n : ℕ
ih : sign (finRotate (n + 1)) = (-1) ^ n
⊢ sign (decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ (n + 1)
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
    riemannZeta k = ∑' n : ℕ, 1 / (n : ℂ) ^ k

Proof state:
k : ℕ
hk : 1 < k
⊢ riemannZeta ↑k = ∑' (n : ℕ), 1 / ↑n ^ k

Tactic:
simp only [zeta_eq_tsum_one_div_nat_cpow
    (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
  cpow_natCast]

Result:
no goals

Proof state:
k : ℕ
hk : 1 < k
⊢ 1 < (↑k).re

Tactic:
rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Iic_mul_Iio_subset' (a b : α) : Iic a * Iio b ⊆ Iio (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Iic a * Iio b ⊆ Iio (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iio b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iio (a * b)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
⊢ Iic a * Iio b ⊆ Iio (a * b)

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
⊢ Iic a * Iio b ⊆ Iio (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b : α
this : MulRightMono α
y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iio b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iio (a * b)

Tactic:
exact mul_lt_mul_of_le_of_lt hya hzb

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_iSup_Iio_le_card_mul_iSup {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
    (⨆ a : Iio o, f a).card ≤ Cardinal.lift.{v} o.card * ⨆ a : Iio o, (f a).card

Proof state:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Tactic:
apply (card_iSup_Iio_le_sum_card f).trans

Result:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (sum fun i => (f (o.enumIsoToType.symm i)).card) ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Proof state:
case h.e'_4.h.e'_6
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, (f (o.enumIsoToType.symm i)).card = ⨆ a, (f a).card

Tactic:
exact (enumIsoToType o).symm.iSup_comp (g := fun x ↦ (f x).card)

Result:
no goals

Proof state:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (sum fun i => (f (o.enumIsoToType.symm i)).card) ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Tactic:
convert ← sum_le_iSup_lift _

Result:
case h.e'_4.h.e'_5.h.e'_1
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ #o.toType = o.card

case h.e'_4.h.e'_6
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, (f (o.enumIsoToType.symm i)).card = ⨆ a, (f a).card

Proof state:
case h.e'_4.h.e'_5.h.e'_1
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ #o.toType = o.card

Tactic:
exact mk_toType o

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂ [DivisionRing α] {x y : α} (h' : Commute x y) (h : x ≠ y)
    (n : ℕ) : ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0

Tactic:
simp_all [sub_eq_iff_eq_add]

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)

Tactic:
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]

Result:
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_mul_expand {p : ℕ} (hp : p ≠ 0) (f g : R[X]) :
    contract p (f * expand R p g) = contract p f * g

Proof state:
case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n * p → (¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
intro ⟨x, y⟩ eq nex

Result:
case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem mk' (Hnt : fixedPoints G X ≠ ⊤)
    (H : ∀ {B : Set X} (_ : IsBlock G B), IsTrivialBlock B) :
    IsPreprimitive G X

Proof state:
case intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w✝ : X
ha : w✝ ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
exact .of_isTrivialBlock_of_not_mem_fixedPoints ha fun {B} _ ↦ H

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
obtain ⟨_, ha⟩ := Hnt

Result:
case intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w✝ : X
ha : w✝ ∉ fixedPoints G X
⊢ IsPreprimitive G X

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X

Tactic:
simp only [Set.top_eq_univ, Set.ne_univ_iff_exists_not_mem] at Hnt

Result:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[gcongr] lemma map_mono {H₁ H₂ : G.Subgraph} (hH : H₁ ≤ H₂) : H₁.map f ≤ H₂.map f

Proof state:
case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w

Tactic:
rintro _ _ ⟨u, v, ha, rfl, rfl⟩

Result:
case right.intro.intro.intro.intro
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
u v : V
ha : H₁.Adj u v
⊢ (Subgraph.map f H₂).Adj (f u) (f v)

Proof state:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a✝ : W
⊢ ∀ x ∈ H₁.verts, f x = a✝ → ∃ x ∈ H₂.verts, f x = a✝

Tactic:
rintro v hv rfl

Result:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
v : V
hv : v ∈ H₁.verts
⊢ ∃ x ∈ H₂.verts, f x = f v

Proof state:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a✝ : W
⊢ a✝ ∈ (Subgraph.map f H₁).verts → a✝ ∈ (Subgraph.map f H₂).verts

Tactic:
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]

Result:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a✝ : W
⊢ ∀ x ∈ H₁.verts, f x = a✝ → ∃ x ∈ H₂.verts, f x = a✝

Proof state:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
v : V
hv : v ∈ H₁.verts
⊢ ∃ x ∈ H₂.verts, f x = f v

Tactic:
exact ⟨_, hH.1 hv, rfl⟩

Result:
no goals

Proof state:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts

Tactic:
intro

Result:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a✝ : W
⊢ a✝ ∈ (Subgraph.map f H₁).verts → a✝ ∈ (Subgraph.map f H₂).verts

Proof state:
case right.intro.intro.intro.intro
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
u v : V
ha : H₁.Adj u v
⊢ (Subgraph.map f H₂).Adj (f u) (f v)

Tactic:
exact ⟨_, _, hH.2 ha, rfl, rfl⟩

Result:
no goals

Proof state:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ Subgraph.map f H₁ ≤ Subgraph.map f H₂

Tactic:
constructor

Result:
case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts

case right
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
⊢ ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem measurable_kernel_prod_mk_left_of_finite {t : Set (α × β)} (ht : MeasurableSet t)
    (hκs : ∀ a, IsFiniteMeasure (κ a)) : Measurable fun a => κ a (Prod.mk a ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ (fun a => (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a => (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)

Tactic:
ext1 a

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (univ \ Prod.mk a ⁻¹' t) = (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
a : α
b : β
⊢ b ∈ Prod.mk a ⁻¹' tᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t

Tactic:
simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : a ∈ t₁
⊢ (κ a) t₂ = (κ a) t₂

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : a ∉ t₁
⊢ (κ a) ∅ = 0

Tactic:
exacts [rfl, measure_empty]

Result:
no goals

Proof state:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a => (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a => (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a => (κ a) (univ \ Prod.mk a ⁻¹' t)

Tactic:
rw [this]

Result:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this : (fun a => (κ a) (univ \ Prod.mk a ⁻¹' t)) = fun a => (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
⊢ Measurable fun a => (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_coe (n : Nat) : withTopEquiv.symm n = n

Proof state:
n : ℕ
⊢ withTopEquiv.symm ↑n = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Conj.lean
theorem refl_conj (f : End X) : (Iso.refl X).conj f = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
⊢ (refl X).conj f = f

Tactic:
rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem sym2_eq_sym_two : xs.sym2.map (Sym2.equivSym α) = xs.sym 2

Proof state:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α)) (x :: xs).sym2 = List.sym 2 (x :: xs)

Tactic:
rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]

Result:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y => s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p => x ::ₛ p) ∘ fun x => x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2

Proof state:
α : Type u_1
xs : List α
⊢ map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs

Tactic:
induction xs with
| nil => simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]
| cons x xs ih =>
  rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]
  rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
⊢ map (⇑(Sym2.equivSym α) ∘ fun y => s(x, y)) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2 =
    map ((fun p => x ::ₛ p) ∘ fun x => x ::ₛ Sym.nil) (x :: xs) ++ map (⇑(Sym2.equivSym α)) xs.sym2

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u_1
xs : List α
⊢ map ⇑(Sym2.equivSym α) [].sym2 = List.sym 2 []

Tactic:
simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[reassoc (attr := simp)]
lemma residueFieldCongr_trans_hom (X : Scheme) {x y z : X} (e : x = y) (e' : y = z) :
    (X.residueFieldCongr e).hom ≫ (X.residueFieldCongr e').hom =
      (X.residueFieldCongr (e.trans e')).hom

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ (residueFieldCongr ⋯).hom ≫ (residueFieldCongr ⋯).hom = (residueFieldCongr ⋯).hom

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
x y z : ↑↑X.toPresheafedSpace
e : x = y
e' : y = z
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom

Tactic:
subst e e'

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ (residueFieldCongr ⋯).hom ≫ (residueFieldCongr ⋯).hom = (residueFieldCongr ⋯).hom
-- Mathlib/Topology/Perfect.lean
lemma IsPreconnected.preperfect_of_nontrivial [T1Space α] {U : Set α} (hu : U.Nontrivial)
    (h : IsPreconnected U) : Preperfect U

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)

Tactic:
specialize h {x} (closure (U \ {x})) isClosed_singleton isClosed_closure ?_ ?_ ?_

Result:
case specialize_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ closure (U \ {x})

case specialize_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ {x}).Nonempty

case specialize_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ (U ∩ closure (U \ {x})).Nonempty

α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : (U ∩ ({x} ∩ closure (U \ {x}))).Nonempty
⊢ AccPt x (𝓟 U)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty
x : α
hx : x ∈ U
⊢ U ⊆ {x} ∪ U \ {x}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
⊢ Preperfect U

Tactic:
intro x hx

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
h : IsPreconnected U
x : α
hx : x ∈ U
⊢ AccPt x (𝓟 U)
-- Mathlib/Data/Real/ConjExponents.lean
theorem inv_add_inv_conj_ennreal : (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ (ENNReal.ofReal p)⁻¹ + (ENNReal.ofReal q)⁻¹ = 1

Tactic:
rw [← ENNReal.ofReal_one, ← ENNReal.ofReal_inv_of_pos h.pos,
  ← ENNReal.ofReal_inv_of_pos h.symm.pos, ← ENNReal.ofReal_add h.inv_nonneg h.symm.inv_nonneg,
  h.inv_add_inv_conj]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem BlankExtends.above_of_le {Γ} [Inhabited Γ] {l l₁ l₂ : List Γ} :
    BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ j ≤ i

Tactic:
rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l l₁ l₂ : List Γ
⊢ BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

Tactic:
rintro ⟨i, rfl⟩ ⟨j, e⟩ h

Result:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default

Tactic:
rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ j ≤ i

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ j ≤ i

Tactic:
apply_fun List.length at e

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length
⊢ j ≤ i

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length
⊢ j ≤ i

Tactic:
simp only [List.length_append, List.length_replicate] at e

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
⊢ j ≤ i

Proof state:
case intro.intro
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ BlankExtends l₁ l₂

Tactic:
use i - j

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (i - j) default

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (i - j) default

Tactic:
refine List.append_cancel_right (e.symm.trans ?_)

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netMaxcard_le_coverMincard (T : X → X) (F : Set X) {U : Set (X × X)} (U_symm : SymmetricRel U)
    (n : ℕ) :
    netMaxcard T F U n ≤ coverMincard T F U n

Proof state:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ ↑t.card

Tactic:
exact iSup₂_le (fun s s_net ↦ Nat.cast_le.2 (s_net.card_le_card_of_isDynCoverOf U_symm t_cover))

Result:
no goals

Proof state:
case inr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rcases ((coverMincard_finite_iff T F U n).1 h) with ⟨t, t_cover, t_mincard⟩

Result:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Proof state:
case inl
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
exact h ▸ le_top

Result:
no goals

Proof state:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rw [← t_mincard]

Result:
case inr.intro.intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
t : Finset X
t_cover : IsDynCoverOf T F U n ↑t
t_mincard : ↑t.card = coverMincard T F U n
⊢ netMaxcard T F U n ≤ ↑t.card

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
⊢ netMaxcard T F U n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h | h

Result:
case inl
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n = ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n

case inr
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
h : coverMincard T F U n < ⊤
⊢ netMaxcard T F U n ≤ coverMincard T F U n