harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem mem_attach : ∀ (o : Option α) (x : {x // x ∈ o}), x ∈ o.attach
  | none, ⟨x, h⟩ => by simp at h
  | some a, ⟨x, h⟩ => by simpa using h

Proof state:
α : Type u_1
a x : α
h : x ∈ some a
⊢ ⟨x, h⟩ ∈ (some a).attach

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
x : α
h : x ∈ none
⊢ ⟨x, h⟩ ∈ none.attach

Tactic:
simp at h

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Icc_pred_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (pred b) = Ico a b :=
  coe_injective <| by simpa using Set.Icc_pred_right_eq_Ico_of_not_isMin hb _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ ↑(Icc a (pred b)) = ↑(Ico a b)

Tactic:
simpa using Set.Icc_pred_right_eq_Ico_of_not_isMin hb _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_replicate_ne {a b : α} (h : !b == a) :
    (replicate n a).insert b = b :: replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
h : (!b == a) = true
⊢ List.insert b (replicate n a) = b :: replicate n a

Tactic:
rw [insert_of_not_mem]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
h : (!b == a) = true
⊢ ¬b ∈ replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
h : (!b == a) = true
⊢ ¬b ∈ replicate n a

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem le_of_succ_get?_den {b : K}
    (nth_partDenom_eq : (of v).partDens.get? n = some b) :
    b * (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDenom_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ (of v).dens (n + 1)

Tactic:
exact le_of_succ_succ_get?_contsAux_b nth_partDenom_eq

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDenom_eq : (of v).partDens.get? n = some b
⊢ b * (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDenom_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ (of v).dens (n + 1)
-- Mathlib/Order/WithBot.lean
theorem monotone_map_iff {f : α → β} : Monotone (WithBot.map f) ↔ Monotone f :=
  monotone_iff.trans <| by simp [Monotone]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((Monotone fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ ≤ map f ↑x) ↔ Monotone f

Tactic:
simp [Monotone]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem ext' : ∀ {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ h₁ h₂, o.get h₁ = p.get h₂) → o = p
  | ⟨od, o⟩, ⟨pd, p⟩, H1, H2 => by
    have t : od = pd := propext H1
    cases t; rw [show o = p from funext fun p => H2 p p]

Proof state:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := pd, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := pd, get := p }

Tactic:
have t : od = pd := propext H1

Result:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := pd, get := p }.get h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }

Proof state:
case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }

Tactic:
rw [show o = p from funext fun p => H2 p p]

Result:
no goals

Proof state:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := pd, get := p }.get h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }

Tactic:
cases t

Result:
case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_denom_mul (x y : RatFunc K) :
    (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom :=
  (num_mul_eq_mul_denom_iff (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))).mpr <| by
    conv_lhs =>
      rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← RingHom.map_mul, ←
        RingHom.map_mul]

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
conv_lhs =>
  rw [← num_div_denom x, ← num_div_denom y, div_mul_div_comm, ← RingHom.map_mul, ←
    RingHom.map_mul]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.mem_closure_iff_ball {s : Set α} {x} :
    x ∈ closure s ↔ ∀ {V}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_map_measure {f : α → δ} {g : δ → β}
    (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
exact memLp_map_measure_iff hg hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
g : δ → β
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_push_some {f : α → Option β} {a : α} {l : Array α} {b : β}
    (h : f a = some b) (w : stop = l.size + 1) :
    filterMap f (l.push a) 0 stop = (filterMap f l).push b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : Array α
b : β
h : f a = some b
⊢ filterMap f (l.push a) 0 (l.size + 1) = (filterMap f l).push b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
a : α
b : β
h : f a = some b
l : List α
⊢ filterMap f ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = (filterMap f { toList := l }).push b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
a : α
b : β
h : f a = some b
l : List α
⊢ filterMap f ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = (filterMap f { toList := l }).push b

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
a : α
l : Array α
b : β
h : f a = some b
w : stop = l.size + 1
⊢ filterMap f (l.push a) 0 stop = (filterMap f l).push b

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : Array α
b : β
h : f a = some b
⊢ filterMap f (l.push a) 0 (l.size + 1) = (filterMap f l).push b
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bddAbove_of_small (s : Set Ordinal.{u}) [h : Small.{u} s] : BddAbove s

Proof state:
case intro
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
⊢ BddAbove s

Tactic:
use a

Result:
case h
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
⊢ a ∈ upperBounds s

Proof state:
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
⊢ BddAbove s

Tactic:
obtain ⟨a, ha⟩ := bddAbove_range (fun x => ((@equivShrink s h).symm x).val)

Result:
case intro
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
⊢ BddAbove s

Proof state:
case h
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
⊢ a ∈ upperBounds s

Tactic:
intro b hb

Result:
case h
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
b : Ordinal.{u}
hb : b ∈ s
⊢ b ≤ a

Proof state:
case h
s : Set Ordinal.{u}
h : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ upperBounds (range fun x => ↑((equivShrink ↑s).symm x))
b : Ordinal.{u}
hb : b ∈ s
⊢ b ≤ a

Tactic:
simpa using ha (mem_range_self (equivShrink s ⟨b, hb⟩))

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma precomp_surjective (F : ComposableArrows C (n + 1)) :
    ∃ (F₀ : ComposableArrows C n) (X₀ : C) (f₀ : X₀ ⟶ F₀.left), F = F₀.precomp f₀ :=
  ⟨F.δ₀, _, F.map' 0 1, ext_succ rfl (by simp) (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C (n + 1)
⊢ F.map' 0 1 ⋯ ⋯ = eqToHom ⋯ ≫ (F.δ₀.precomp (F.map' 0 1 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F : ComposableArrows C (n + 1)
⊢ F.δ₀ = (F.δ₀.precomp (F.map' 0 1 ⋯ ⋯)).δ₀

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_coe_apply' {n : ℤ} {x : ℝ} :
    toCircle (n • (x : AddCircle T) :) = Complex.exp (2 * π * Complex.I * n * x / T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ ↑(toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
rw [← fourier_apply]

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
exact fourier_coe_apply

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_neg : sinh (-x) = -sinh x

Proof state:
x : ℂ
⊢ sinh (-x) = -sinh x

Tactic:
simp [sinh, exp_neg, (neg_div _ _).symm, add_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
    xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : ¬findIdx p xs ≤ i
⊢ False

Tactic:
simp at h3

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : i < findIdx p xs
⊢ False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : i < findIdx p xs
⊢ False

Tactic:
simp_all [not_of_lt_findIdx h3]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs = i

Tactic:
apply Nat.le_antisymm _ (le_findIdx_of_not h h2)

Result:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs ≤ i

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs ≤ i

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬findIdx p xs ≤ i → False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬findIdx p xs ≤ i → False

Tactic:
intro h3

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : ¬findIdx p xs ≤ i
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
⊢ findIdx p xs = i ↔ p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false

Tactic:
refine ⟨fun f ↦ ⟨f ▸ (@findIdx_getElem _ p xs (f ▸ h)), fun _ hji ↦ not_of_lt_findIdx (f ▸ hji)⟩,
  fun ⟨_, h2⟩ ↦ ?_⟩

Result:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs = i
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrictDvd_surjective (hpq : p ∣ q) (hq : q ≠ 0) :
    Function.Surjective (restrictDvd hpq)

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective ⇑(restrictDvd hpq)

Tactic:
classical
haveI := Fact.mk <|
  splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq
simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
this : Fact (Splits (algebraMap F q.SplittingField) p)
⊢ Function.Surjective ⇑(restrictDvd hpq)

Tactic:
simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
⊢ Function.Surjective ⇑(restrictDvd hpq)

Tactic:
haveI := Fact.mk <|
  splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p ∣ q
hq : q ≠ 0
this : Fact (Splits (algebraMap F q.SplittingField) p)
⊢ Function.Surjective ⇑(restrictDvd hpq)
-- Mathlib/Data/List/Lattice.lean
theorem sublist_suffix_of_union : ∀ l₁ l₂ : List α, ∃ t, t <+ l₁ ∧ t ++ l₂ = l₁ ∪ l₂
  | [], _ => ⟨[], by rfl, rfl⟩
  | a :: l₁, l₂ =>
    let ⟨t, s, e⟩ := sublist_suffix_of_union l₁ l₂
    if h : a ∈ l₁ ∪ l₂ then
      ⟨t, sublist_cons_of_sublist _ s, by
        simp only [e, cons_union, insert_of_mem h]⟩
    else
      ⟨a :: t, s.cons_cons _, by
        simp only [cons_append, cons_union, e, insert_of_not_mem h]⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x✝ : List α
⊢ [] <+ []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ l₁ ∪ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
simp only [cons_append, cons_union, e, insert_of_not_mem h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
simp only [e, cons_union, insert_of_mem h]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem _root_.ZFSet.isOrdinal_iff_isWellOrder : x.IsOrdinal ↔
    x.IsTransitive ∧ IsWellOrder _ (Subrel (· ∈ ·) (· ∈ x))

Proof state:
case mpr
x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsOrdinal

Proof state:
case mpr.intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ IsTrans { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)

Tactic:
infer_instance

Result:
no goals

Proof state:
x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)

Tactic:
use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩

Result:
case mpr
x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x) → x.IsOrdinal

Proof state:
case mpr.intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩

Result:
case mpr.intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ IsTrans { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i

Proof state:
w✝ : Nat
x : BitVec w✝
b : Bool
i : Nat
⊢ (x.concat b).getLsbD (i + 1) = x.getLsbD i

Tactic:
simp [getLsbD_concat]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- The L-series of `δ` is the constant function `1`. -/
lemma LSeries_delta : LSeries δ = 1

Proof state:
case h
x✝ : ℂ
⊢ L δ x✝ = 1 x✝

Tactic:
simp [LSeries, LSeries.term_delta]

Result:
no goals

Proof state:
⊢ L δ = 1

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ L δ x✝ = 1 x✝
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem isSymmetric {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) : (A : E →ₗ[𝕜] E).IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x y : E
⊢ ⟪↑A x, y⟫_𝕜 = ⟪x, ↑A y⟫_𝕜

Tactic:
rw_mod_cast [← A.adjoint_inner_right, hA.adjoint_eq]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : IsSelfAdjoint A
⊢ (↑A).IsSymmetric

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x y : E
⊢ ⟪↑A x, y⟫_𝕜 = ⟪x, ↑A y⟫_𝕜
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem map_ite_zero_one {F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F)
    (p : Prop) [Decidable p] :
    f (ite p 0 1) = ite p 0 1

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
F : Type u_5
inst✝² : FunLike F α β
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 0 else 1) = if p then 0 else 1

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.union (hs : s.Finite) (ht : t.Finite) : (s ∪ t).Finite

Proof state:
α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite

Tactic:
rw [Set.Finite] at hs ht

Result:
α : Type u
s t : Set α
hs : Finite ↑s
ht : Finite ↑t
⊢ (s ∪ t).Finite

Proof state:
α : Type u
s t : Set α
hs : Finite ↑s
ht : Finite ↑t
⊢ (s ∪ t).Finite

Tactic:
apply toFinite

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem equiv_trans {ι'' : Type*} (b'' : Basis ι'' R M'') (e : ι ≃ ι') (e' : ι' ≃ ι'') :
    (b.equiv b' e).trans (b'.equiv b'' e') = b.equiv b'' (e.trans e') :=
  b.ext' fun i => by simp

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
M'' : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
ι'' : Type u_10
b'' : Basis ι'' R M''
e : ι ≃ ι'
e' : ι' ≃ ι''
i : ι
⊢ (b.equiv b' e ≪≫ₗ b'.equiv b'' e') (b i) = (b.equiv b'' (e.trans e')) (b i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_singleton' (l : Vector α n) : (l.flatMap fun x => #v[x]) = l.cast (by simp)

Proof state:
α : Type ?u.328317
n : Nat
l : Vector α n
⊢ n = n * 1

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => { toArray := #[x], size_toArray := ⋯ }) =
    Vector.cast ⋯ { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ (l.flatMap fun x => { toArray := #[x], size_toArray := ⋯ }) = Vector.cast ⋯ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap fun x => { toArray := #[x], size_toArray := ⋯ }) =
    Vector.cast ⋯ { toArray := l, size_toArray := ⋯ }
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma prodMkRight_add (κ η : Kernel α β) :
    prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkRight γ (κ + η)) a✝¹) s✝ = ((prodMkRight γ κ + prodMkRight γ η) a✝¹) s✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
⊢ prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkRight γ (κ + η)) a✝¹) s✝ = ((prodMkRight γ κ + prodMkRight γ η) a✝¹) s✝
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalComp_cons {f g h i j : C} (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i} {θ : i ⟶ j} {ι : h ⟶ j}
    (e_ι : ηs ≫ θ = ι)  :
    (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
simp [e_ι]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
theorem IsInitial.hom_ext {X Y : C} (t : IsInitial X) (f g : X ⟶ Y) : f = g :=
  IsColimit.hom_ext t (by simp)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f g : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone X).ι.app j ≫ f = (asEmptyCocone X).ι.app j ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma Γevaluation_ne_zero_iff_mem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
    X.Γevaluation x f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f :=
  evaluation_ne_zero_iff_mem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
f : ↑(X.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals