harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_sub_self_eq (ha : fract a ≠ 0) : (⌈a⌉ : α) - a = 1 - fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - fract a

Tactic:
rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : fract a ≠ 0
⊢ ↑⌈a⌉ - a = 1 - (a + 1 - ↑⌈a⌉)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_map_complex (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x : V) :
    f (o.rotation θ x) = θ.toCircle * f x

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = ↑θ.toCircle * f x

Tactic:
rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKeyD k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany empty l).val.getKeyD k' fallback = k

Tactic:
rw [getKeyD_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma one_le_toNNReal {r : ℝ} : 1 ≤ r.toNNReal ↔ 1 ≤ r

Proof state:
r : ℝ
⊢ 1 ≤ r.toNNReal ↔ 1 ≤ r

Tactic:
simpa using toNNReal_le_toNNReal_iff_of_pos one_pos

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_of_equiv {I : Ideal R} (f : R ≃+* S) :
    (I.comap (f.symm : S →+* R)).comap (f : R →+* S) = I

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (↑f) (comap (↑f.symm) I) = I

Tactic:
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
  RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_cons (a : α) {l₁ l₂ : List α} : a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
x✝ : a :: l₁ <+~ a :: l₂
l : List α
s : l <+ a :: l₂
l₁✝ : List α
s' : l₁✝ <+ l₂
p : a :: l₁✝ ~ a :: l₁
⊢ l₁ <+~ l₂

Tactic:
exact ⟨_, p.cons_inv, s'⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
⊢ a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂

Tactic:
refine ⟨fun ⟨l, p, s⟩ => ?_, fun ⟨l, p, s⟩ => ⟨a :: l, p.cons a, s.cons₂ _⟩⟩

Result:
α : Type u_1
a : α
l₁ l₂ : List α
x✝ : a :: l₁ <+~ a :: l₂
l : List α
p : l ~ a :: l₁
s : l <+ a :: l₂
⊢ l₁ <+~ l₂

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
x✝ : a :: l₁ <+~ a :: l₂
l : List α
p : l ~ a :: l₁
s : l <+ a :: l₂
⊢ l₁ <+~ l₂

Tactic:
match s with
| .cons _ s' => exact (p.subperm_left.2 <| (sublist_cons_self _ _).subperm).trans s'.subperm
| .cons₂ _ s' => exact ⟨_, p.cons_inv, s'⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
x✝ : a :: l₁ <+~ a :: l₂
l✝ : List α
s : l✝ <+ a :: l₂
l : List α
s' : l <+ l₂
p : l ~ a :: l₁
⊢ l₁ <+~ l₂

Tactic:
exact (p.subperm_left.2 <| (sublist_cons_self _ _).subperm).trans s'.subperm

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem elementarilyEquivalent_iff : M ≅[L] N ↔ ∀ φ : L.Sentence, M ⊨ φ ↔ N ⊨ φ

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ M ≅[L] N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ

Tactic:
simp only [ElementarilyEquivalent, Set.ext_iff, completeTheory, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem refl (φ : L.BoundedFormula α n) : φ ⇔[T] φ :=
  fun M v xs => by rw [BoundedFormula.realize_iff]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ φ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
  | m, [] => by simp
  | 0, l => by simp
  | m + 1, a :: l =>
    calc
      drop n (drop (m + 1) (a :: l)) = drop n (drop m l) := rfl
      _ = drop (m + n) l := drop_drop n m l
      _ = drop ((m + 1) + n) (a :: l)

Proof state:
α : Type u_1
n m : Nat
⊢ drop n (drop m []) = drop (m + n) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
a : α
l : List α
⊢ drop (m + n) l = drop (m + 1 + n) (a :: l)

Tactic:
rw [Nat.add_right_comm]

Result:
α : Type u_1
n m : Nat
a : α
l : List α
⊢ drop (m + n) l = drop (m + n + 1) (a :: l)

Proof state:
α : Type u_1
n m : Nat
a : α
l : List α
⊢ drop (m + n) l = drop (m + n + 1) (a :: l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ drop n (drop 0 l) = drop (0 + n) l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_mkVector_of_mem {a : α} {l : Vector α n} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkVector n a

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l → b = a
⊢ l.toArray = (mkVector n a).toArray

Tactic:
simpa using Array.eq_mkArray_of_mem (l := l.toArray) (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l → b = a
⊢ ∀ (b : α), b ∈ l.toArray → b = a

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l → b = a
⊢ l = mkVector n a

Tactic:
rw [← toArray_inj]

Result:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : ∀ (b : α), b ∈ l → b = a
⊢ l.toArray = (mkVector n a).toArray
-- Mathlib/Probability/ConditionalProbability.lean
lemma absolutelyContinuous_cond_univ [IsFiniteMeasure μ] : μ ≪ μ[|univ]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (μ univ)⁻¹ ≠ 0

Tactic:
simp [measure_ne_top]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ μ[|univ]

Tactic:
rw [cond, restrict_univ]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ (μ univ)⁻¹ • μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ (μ univ)⁻¹ • μ

Tactic:
refine absolutelyContinuous_smul ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (μ univ)⁻¹ ≠ 0
-- Mathlib/Data/ENNReal/Real.lean
@[simp]
lemma one_le_ofReal {p : ℝ} : 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

Proof state:
p : ℝ
⊢ 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

Tactic:
exact mod_cast natCast_le_ofReal one_ne_zero

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem eqRec_heq' {α : Sort*} {a' : α} {motive : (a : α) → a' = a → Sort*}
    (p : motive a' (rfl : a' = a')) {a : α} (t : a' = a) :
    HEq (@Eq.rec α a' motive p a t) p

Proof state:
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u_2
p : motive a' ⋯
⊢ HEq (⋯ ▸ p) p

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u_2
p : motive a' ⋯
a : α
t : a' = a
⊢ HEq (t ▸ p) p

Tactic:
subst t

Result:
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u_2
p : motive a' ⋯
⊢ HEq (⋯ ▸ p) p
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem image_mul_left :
    image (fun b => a * b) t = preimage t (fun b => a⁻¹ * b) (mul_right_injective _).injOn :=
  coe_injective <| by simp

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
a : α
⊢ ↑(image (fun b => a * b) t) = ↑(t.preimage (fun b => a⁻¹ * b) ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_zero {x : BitVec w} : x * 0#w = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ x * 0#w = 0#w

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
⊢ (x * 0#w).toNat = (0#w).toNat

Proof state:
case a
w : Nat
x : BitVec w
⊢ (x * 0#w).toNat = (0#w).toNat

Tactic:
simp [toNat_mul]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_nonpos_iff {a b : EReal} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Proof state:
a b : EReal
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

Result:
no goals

Proof state:
a b : EReal
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
nth_rw 1 [← neg_zero]

Result:
a b : EReal
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a

Proof state:
a b : Int
⊢ ↑(a.gcd b) ∣ a

Tactic:
have := Nat.gcd_dvd_left a.natAbs b.natAbs

Result:
a b : Int
this : a.natAbs.gcd b.natAbs ∣ a.natAbs
⊢ ↑(a.gcd b) ∣ a

Proof state:
a b : Int
this : ↑(a.natAbs.gcd b.natAbs) ∣ ↑a.natAbs
⊢ ↑(a.gcd b) ∣ a

Tactic:
exact Int.dvd_trans this natAbs_dvd_self

Result:
no goals

Proof state:
a b : Int
this : a.natAbs.gcd b.natAbs ∣ a.natAbs
⊢ ↑(a.gcd b) ∣ a

Tactic:
rw [← Int.ofNat_dvd] at this

Result:
a b : Int
this : ↑(a.natAbs.gcd b.natAbs) ∣ ↑a.natAbs
⊢ ↑(a.gcd b) ∣ a
-- Mathlib/Data/Set/Function.lean
theorem image_restrict (f : α → β) (s t : Set α) :
    s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)

Tactic:
rw [restrict_eq, image_comp, image_preimage_eq_inter_range, Subtype.range_coe]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mem_support_toFun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ 0

Proof state:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ ↑s ∧ f i ≠ 0 ↔ f i ≠ 0

Tactic:
exact and_iff_right_of_imp (s.prop i).resolve_right

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ f.support ↔ f i ≠ 0

Tactic:
obtain ⟨f, s⟩ := f

Result:
case mk'
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := s }.support ↔ { toFun := f, support' := s } i ≠ 0

Proof state:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ Finset.filter (fun i => { toFun := f, support' := Trunc.mk s } i ≠ 0) (↑s).toFinset ↔
    { toFun := f, support' := Trunc.mk s } i ≠ 0

Tactic:
rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']

Result:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ ↑s ∧ f i ≠ 0 ↔ f i ≠ 0

Proof state:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := Trunc.mk s }.support ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0

Tactic:
dsimp only [support, Trunc.lift_mk]

Result:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ Finset.filter (fun i => { toFun := f, support' := Trunc.mk s } i ≠ 0) (↑s).toFinset ↔
    { toFun := f, support' := Trunc.mk s } i ≠ 0

Proof state:
case mk'
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := s }.support ↔ { toFun := f, support' := s } i ≠ 0

Tactic:
induction' s using Trunc.induction_on with s

Result:
case mk'.h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := Trunc.mk s }.support ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fdiv_self {a : Int} (H : a ≠ 0) : a.fdiv a = 1

Proof state:
a : Int
H : a ≠ 0
this : (1 * a).fdiv a = 1
⊢ a.fdiv a = 1

Tactic:
rwa [Int.one_mul] at this

Result:
no goals

Proof state:
a : Int
H : a ≠ 0
⊢ a.fdiv a = 1

Tactic:
have := Int.mul_fdiv_cancel 1 H

Result:
a : Int
H : a ≠ 0
this : (1 * a).fdiv a = 1
⊢ a.fdiv a = 1
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem baseChange_neg : (-f).baseChange A = -f.baseChange A

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ baseChange A (-f) = -baseChange A f

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (-f))) 1) x✝ = ((AlgebraTensorModule.curry (-baseChange A f)) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (-f))) 1) x✝ = ((AlgebraTensorModule.curry (-baseChange A f)) 1) x✝

Tactic:
simp [baseChange_eq_ltensor, tmul_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem tail_modifyHead {f : α → α} {l : List α} :
    (l.modifyHead f).tail = l.tail

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ (modifyHead f l).tail = l.tail

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
lemma edgeFinset_subset_sym2_of_support_subset (h : G.support ⊆ s) :
    G.edgeFinset ⊆ s.toFinset.sym2

Proof state:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
x✝ y✝ : V
hadj : G.Adj x✝ y✝
⊢ x✝ ∈ s ∧ y✝ ∈ s

Tactic:
exact ⟨h ⟨_, hadj⟩, h ⟨_, hadj.symm⟩⟩

Result:
no goals

Proof state:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeFinset ⊆ s.toFinset.sym2

Tactic:
simp_rw [subset_iff, Sym2.forall,
  mem_edgeFinset, mem_edgeSet, mk_mem_sym2_iff, Set.mem_toFinset]

Result:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ ∀ (x y : V), G.Adj x y → x ∈ s ∧ y ∈ s

Proof state:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ ∀ (x y : V), G.Adj x y → x ∈ s ∧ y ∈ s

Tactic:
intro _ _ hadj

Result:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x => x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
x✝ y✝ : V
hadj : G.Adj x✝ y✝
⊢ x✝ ∈ s ∧ y✝ ∈ s
-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- A proper map is closed. -/
lemma IsProperMap.isClosedMap (h : IsProperMap f) : IsClosedMap f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)

Tactic:
exact fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f

Tactic:
rw [isClosedMap_iff_clusterPt]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ ∀ (s : Set X) (y : Y), MapClusterPt y (𝓟 s) f → ∃ x, f x = y ∧ ClusterPt x (𝓟 s)
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem of_discreteTopology [DiscreteTopology M] [Unique E] :
    IsManifold (modelWithCornersSelf 𝕜 E) n M

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
n : WithTop ℕ∞
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : DiscreteTopology M
inst✝ : Unique E
⊢ IsManifold 𝓘(𝕜, E) n M

Tactic:
apply isManifold_of_contDiffOn _ _ _ (fun _ _ _ _ ↦ contDiff_of_subsingleton.contDiffOn)

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem conj (w : W) : cs.IsReflection (w * t * w⁻¹)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection (w * t * w⁻¹)

Tactic:
obtain ⟨u, i, rfl⟩ := ht

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)

Proof state:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹

Tactic:
group

Result:
no goals

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)

Tactic:
use w * u, i

Result:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toGame_natCast : ∀ n : ℕ, toGame n = n
  | 0 => Quot.sound (zeroToPGameRelabelling).equiv
  | n + 1 => by
    have : toGame 1 = 1 := Quot.sound oneToPGameRelabelling.equiv
    rw [Nat.cast_add, ← nadd_nat, toGame_nadd, toGame_natCast, Nat.cast_one, this]
    rfl

Proof state:
n : ℕ
this : toGame 1 = 1
⊢ ↑n + 1 = ↑(n + 1)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ toGame ↑(n + 1) = ↑(n + 1)

Tactic:
have : toGame 1 = 1 := Quot.sound oneToPGameRelabelling.equiv

Result:
n : ℕ
this : toGame 1 = 1
⊢ toGame ↑(n + 1) = ↑(n + 1)

Proof state:
n : ℕ
this : toGame 1 = 1
⊢ toGame ↑(n + 1) = ↑(n + 1)

Tactic:
rw [Nat.cast_add, ← nadd_nat, toGame_nadd, toGame_natCast, Nat.cast_one, this]

Result:
n : ℕ
this : toGame 1 = 1
⊢ ↑n + 1 = ↑(n + 1)
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_top_right : relrank A ⊤ = Module.rank A E

Proof state:
E : Type v
inst✝ : Field E
A : Subfield E
x✝ : AddCommMonoid ↥⊤ := inferInstance
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
  IntermediateField.topEquiv.toLinearEquiv.rank_eq]

Result:
no goals

Proof state:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
let _ : AddCommMonoid (⊤ : IntermediateField A E) := inferInstance

Result:
E : Type v
inst✝ : Field E
A : Subfield E
x✝ : AddCommMonoid ↥⊤ := inferInstance
⊢ A.relrank ⊤ = Module.rank (↥A) E
-- Mathlib/RingTheory/Artinian/Module.lean
theorem set_has_minimal_iff_artinian :
    (∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M

Tactic:
rw [isArtinian_iff, WellFounded.wellFounded_iff_has_min]

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_hom {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β}
    (hm : ∀ x y, m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) :
    (s.map m).fold op' (m b) = m (s.fold op b) :=
  Multiset.induction_on s (by simp) (by simp +contextual [hm])

Proof state:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ fold op' (m b) (map m 0) = m (fold op b 0)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
op' : β → β → β
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : α → β
hm : ∀ (x y : α), m (op x y) = op' (m x) (m y)
b : α
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α),
    fold op' (m b) (map m s) = m (fold op b s) → fold op' (m b) (map m (a ::ₘ s)) = m (fold op b (a ::ₘ s))

Tactic:
simp +contextual [hm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eq_some_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
    (h : containsKey a l = true) :
    getKey? a l = some (getKeyD a l fallback)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
a fallback : α
h : containsKey a l = true
⊢ getKey? a l = some (getKeyD a l fallback)

Tactic:
rw [getKey?_eq_some_getKey h, getKey_eq_getKeyD]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem chineseRemainder_modEq_unique (co : n.Coprime m) {a b z}
    (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) : z ≡ chineseRemainder co a b [MOD n*m]

Proof state:
m n : ℕ
co : n.Coprime m
a b z : ℕ
hzan : z ≡ a [MOD n]
hzbm : z ≡ b [MOD m]
⊢ z ≡ ↑(chineseRemainder co a b) [MOD n * m]

Tactic:
simpa [Nat.Coprime.lcm_eq_mul co] using
  mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm)
    (hzbm.trans ((chineseRemainder co a b).prop.2).symm)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma not_dvd_of_natDegree_lt (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) :
    ¬p ∣ q

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
hcontra : p ∣ q
⊢ False

Tactic:
exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
⊢ ¬p ∣ q

Tactic:
by_contra hcontra

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
hcontra : p ∣ q
⊢ False
-- Mathlib/Topology/Category/Compactum.lean
theorem join_distrib (X : Compactum) (uux : Ultrafilter (Ultrafilter X)) :
    X.str (X.join uux) = X.str (map X.str uux)

Proof state:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.μ.app X.A ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)

Tactic:
rw [Monad.Algebra.assoc]

Result:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.map X.a ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)

Proof state:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)

Tactic:
change ((β ).μ.app _ ≫ X.a) _ = _

Result:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.μ.app X.A ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)

Proof state:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (β.map X.a ≫ X.a) uux = X.str (Ultrafilter.map X.str uux)

Tactic:
rfl

Result:
no goals