harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Sober.lean
lemma closure [QuasiSober α] : closure (genericPoints α) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
⊢ _root_.closure (genericPoints α) = univ

Tactic:
refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.subset_def.mp ?_ x mem_irreducibleComponent

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
x : α
⊢ irreducibleComponent x ⊆ _root_.closure (genericPoints α)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
x : α
⊢ {↑(ofComponent ⟨irreducibleComponent x, ⋯⟩)} ⊆ genericPoints α

Tactic:
exact Set.singleton_subset_iff.mpr (ofComponent _).2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
x : α
⊢ irreducibleComponent x ⊆ _root_.closure (genericPoints α)

Tactic:
refine (isGenericPoint_ofComponent
  ⟨_, irreducibleComponent_mem_irreducibleComponents x⟩).symm.trans_subset (closure_mono ?_)

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
x : α
⊢ {↑(ofComponent ⟨irreducibleComponent x, ⋯⟩)} ⊆ genericPoints α
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem exp_half_dist (z w : ℍ) :
    exp (dist z w / 2) = (dist (z : ℂ) w + dist (z : ℂ) (conj ↑w)) / (2 * √(z.im * w.im))

Proof state:
z w : ℍ
⊢ rexp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))

Tactic:
rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_mem_support (hD : D.Injective) (hp : p ≠ 0) :
    D.invFun (p.supDegree D) ∈ p.support

Proof state:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
rwa [he, Function.leftInverse_invFun hD]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp

Result:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ Function.invFun D (supDegree D p) ∈ p.support
-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem P_le (f : ℕ → ℂ[X]) (s : ℂ) (c : ℝ)
    (hc : ∀ p : ℕ, ∀ x ∈ Set.Ioc (0 : ℝ) 1, ‖(f p).eval (x • s)‖ ≤ c ^ p) :
    ∃ c' ≥ 0, ∀ p ≠ 0, ‖P (f p) s‖ ≤ c' ^ p

Proof state:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p

Tactic:
let c₂ := max (Real.exp ‖s‖) 1

Result:
case intro.intro
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖LindemannWeierstrass.P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := Real.exp s.re ⊔ 1
c₂ : ℝ := Real.exp ‖s‖ ⊔ 1
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (f p) s‖ ≤ c' ^ p
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem Submodule.exists_add_mem_mem_orthogonal [HasOrthogonalProjection K] (v : E) :
    ∃ y ∈ K, ∃ z ∈ Kᗮ, v = y + z :=
  ⟨orthogonalProjection K v, Subtype.coe_prop _, v - orthogonalProjection K v,
    sub_orthogonalProjection_mem_orthogonal _, by simp⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : E
⊢ v = ↑((orthogonalProjection K) v) + (v - ↑((orthogonalProjection K) v))

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma SubRootedTree.bot_mem_iff {t : RootedTree} (r : SubRootedTree t) :
    ⊥ ∈ r ↔ r.root = ⊥

Proof state:
t : RootedTree
r : SubRootedTree t
⊢ ⊥ ∈ r ↔ r.root = ⊥

Tactic:
simp [mem_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma op_commShiftIso_inv_app (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0):
    (F.op.commShiftIso n).inv.app X =
      (shiftFunctorOpIso D n m h).hom.app (op (F.obj X.unop)) ≫
        ((F.commShiftIso m).hom.app X.unop).op ≫
          (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((F.commShiftIso m).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X))) ≫
          (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
            ((F.commShiftIso m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Tactic:
simp [← op_comp, ← F.map_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ (F.op.commShiftIso n).inv.app X =
    (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
      ((F.commShiftIso m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Tactic:
rw [← cancel_epi ((F.op.commShiftIso n).hom.app X), Iso.hom_inv_id_app,
  op_commShiftIso_hom_app _ X n m h, assoc, assoc]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((F.commShiftIso m).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X))) ≫
          (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
            ((F.commShiftIso m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftRight_neg (m n : ℤ) : m >>> (-n) = m <<< n

Proof state:
m n : ℤ
⊢ m >>> (-n) = m <<< n

Tactic:
rw [← shiftLeft_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
    n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
  have h : 0 < (n - k)! * (k - s)! * s !

Proof state:
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
⊢ 0 < (n - k)! * (k - s)! * s !

Tactic:
apply_rules [factorial_pos, Nat.mul_pos]

Result:
no goals

Proof state:
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) = n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)!

Tactic:
rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc _ s !, Nat.mul_assoc,
  Nat.mul_comm (n - k)!, Nat.mul_comm s !]

Result:
no goals

Proof state:
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : 0 < (n - k)! * (k - s)! * s !
⊢ n ! = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!)

Tactic:
rw [choose_mul_factorial_mul_factorial (Nat.sub_le_sub_right hkn _),
  choose_mul_factorial_mul_factorial (hsk.trans hkn)]

Result:
no goals

Proof state:
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)! = n !

Tactic:
rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]

Result:
no goals

Proof state:
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) =
    n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !)

Tactic:
rw [Nat.sub_sub_sub_cancel_right hsk, Nat.mul_assoc, Nat.mul_left_comm s !, Nat.mul_assoc,
  Nat.mul_comm (k - s)!, Nat.mul_comm s !, Nat.mul_right_comm, ← Nat.mul_assoc]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem inter_cons_of_mem (l₁ : List α) (h : a ∈ l₂) : (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Proof state:
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
simp [Inter.inter, List.inter, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma coeff_divByMonic_X_sub_C_rec (p : R[X]) (a : R) (n : ℕ) :
    (p /ₘ (X - C a)).coeff n = coeff p (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
rw [← p.modByMonic_add_div this]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Tactic:
have := monic_X_sub_C a

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Tactic:
set q := p /ₘ (X - C a)

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this✝ : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
this : (p %ₘ (X - C a)).degree < ↑(n + 1)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
  |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this✝ : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
this : (p %ₘ (X - C a)).degree < ↑(n + 1)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_thickening_subset (ε δ : ℝ) (s : Set α) :
    thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
obtain hδ | hδ := le_total δ 0

Result:
case inr.inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : δ ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
obtain hε | hε := le_total ε 0

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Proof state:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add hε hδ]

Result:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hε, empty_subset]

Result:
no goals

Proof state:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ z, (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun ⟨y, ⟨z, hz, hy⟩, hx⟩ =>
  ⟨z, hz, (edist_triangle _ _ _).trans_lt <| ENNReal.add_lt_add hx hy⟩

Result:
no goals

Proof state:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
intro x

Result:
case inr.inr
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s

Proof state:
case inr.inl
α : Type u
inst✝ : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : δ ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hδ, thickening_empty, empty_subset]

Result:
no goals
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
lemma ruzsaSzemerediNumber_mono (f : α ↪ β) : ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ G_1 x, #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear

Tactic:
refine ⟨G.map f, inferInstance, ?_, hG.map _⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #((SimpleGraph.map f G).cliqueFinset 3) = #(G.cliqueFinset 3)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ∀ (n : ℕ), (∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) → ∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ∀ (n : ℕ), (∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) → ∃ G x, #(G.cliqueFinset 3) = n ∧ G.LocallyLinear

Tactic:
rintro n ⟨G, _, rfl, hG⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ G_1 x, #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #((SimpleGraph.map f G).cliqueFinset 3) = #(G.cliqueFinset 3)

Tactic:
rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ 3 ≠ 1

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ 3 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β

Tactic:
classical
refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
rintro n ⟨G, _, rfl, hG⟩
refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_insert_swap (x y : α) (l : List α) :
    List.insert x (List.insert y l) ~ List.insert y (List.insert x l)

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)

Tactic:
if xy : x = y then simp [xy] else
simp [List.insert, xl, yl, xy, Ne.symm xy]
constructor

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)

Tactic:
simp [List.insert, xl, yl, xy, Ne.symm xy]

Result:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ x :: y :: l ~ y :: x :: l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : x = y
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)

Tactic:
simp [xy]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
xy : ¬x = y
⊢ x :: y :: l ~ y :: x :: l

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
⊢ List.insert x (List.insert y l) ~ List.insert y (List.insert x l)

Tactic:
by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
xl : ¬x ∈ l
yl : ¬y ∈ l
⊢ List.insert x (y :: l) ~ List.insert y (x :: l)
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem exists_eq_add_translationNumber (hf : Continuous f) : ∃ x, f x = x + τ f

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
⊢ ∃ x, f x = x + τ f

Tactic:
obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
  by_contra! H
  exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Result:
case intro
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
⊢ ∃ x, f x = x + τ f

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
H : ∀ (x : ℝ), x + τ f < f x
⊢ False

Tactic:
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Result:
no goals

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
⊢ ∃ x, f x ≤ x + τ f

Tactic:
by_contra! H

Result:
f : CircleDeg1Lift
hf : Continuous ⇑f
H : ∀ (x : ℝ), x + τ f < f x
⊢ False

Proof state:
case intro
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
⊢ ∃ x, f x = x + τ f

Tactic:
obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
  by_contra! H
  exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

Result:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ f b
⊢ ∃ x, f x = x + τ f

Proof state:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ f b
⊢ ∃ x, f x = x + τ f

Tactic:
exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb

Result:
no goals

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
⊢ ∃ x, x + τ f ≤ f x

Tactic:
by_contra! H

Result:
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
H : ∀ (x : ℝ), f x < x + τ f
⊢ False

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
a : ℝ
ha : f a ≤ a + τ f
H : ∀ (x : ℝ), f x < x + τ f
⊢ False

Tactic:
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem ppow_apply {f : ArithmeticFunction R} {k x : ℕ} (kpos : 0 < k) : f.ppow k x = f x ^ k

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ (f.ppow k) x = f x ^ k

Tactic:
rw [ppow, dif_neg (Nat.ne_of_gt kpos)]

Result:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ { toFun := fun x => f x ^ k, map_zero' := ⋯ } x = f x ^ k

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ { toFun := fun x => f x ^ k, map_zero' := ⋯ } x = f x ^ k

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem contMDiffVectorBundle : @ContMDiffVectorBundle n
    _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle a.toVectorBundle :=
  letI := a.totalSpaceTopology; letI := a.toFiberBundle; letI := a.toVectorBundle
  { contMDiffOn_coordChangeL

Proof state:
n : WithTop ℕ∞
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩

Result:
case mk.intro.intro.mk.intro.intro
n : WithTop ℕ∞
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
⊢ ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n
    (fun b =>
      ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b))
    ((a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩
      (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet)