harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem reduce_to_polynomial_of_mul_T (f : R[T;T⁻¹]) {Q : R[T;T⁻¹] → Prop}
    (Qf : ∀ f : R[X], Q (toLaurent f)) (QT : ∀ f, Q (f * T 1) → Q f) : Q f

Proof state:
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)) * T 1)

Tactic:
simpa using hn

Result:
no goals

Proof state:
case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))

Tactic:
induction n with
| zero => simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
| succ n hn => convert QT _ _; simpa using hn

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f

Tactic:
induction' f using LaurentPolynomial.induction_on_mul_T with f n

Result:
case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))

Proof state:
case Qf.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)))

Tactic:
convert QT _ _

Result:
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)) * T 1)

Proof state:
case Qf.zero
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
⊢ Q (toLaurent f * T (-↑0))

Tactic:
simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.tail? (hwf : (s : Heap α).WF le n) : s.tail? le = some tl → tl.WF le 0

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl : Heap α
hwf : WF le n s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le 0 tl

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact hwf.deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl✝ : Heap α
hwf : WF le n s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl✝
a : α
tl : Heap α
eq₂ : Heap.deleteMin le s = some (a, tl)
⊢ WF le 0 ((fun x => x.snd) (a, tl))

Tactic:
exact hwf.deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl : Heap α
hwf : WF le n s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le 0 tl

Tactic:
intro eq

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl : Heap α
hwf : WF le n s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le 0 tl

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl : Heap α
hwf : WF le n s
⊢ Heap.tail? le s = some tl → WF le 0 tl

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
n : Nat
tl : Heap α
hwf : WF le n s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le 0 tl
-- Mathlib/Order/ScottContinuity.lean
theorem ScottContinuousOn.monotone (D : Set (Set α)) (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D)
    (h : ScottContinuousOn D f) : Monotone f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
⊢ Monotone f

Tactic:
refine fun a b hab =>
  (h (hD a b hab) (insert_nonempty _ _) (directedOn_pair le_refl hab) ?_).1
    (mem_image_of_mem _ <| mem_insert _ _)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b

Tactic:
exact isLeast_Ici

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b

Tactic:
rw [IsLUB, upperBounds_insert, upperBounds_singleton,
  inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem hasMFDerivAt_const (c : M') (x : M) :
    HasMFDerivAt I I' (fun _ : M => c) x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
c : M'
x : M
⊢ HasMFDerivAt I I' (fun x => c) x 0

Tactic:
refine ⟨continuous_const.continuousAt, ?_⟩

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
c : M'
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x fun x => c) 0 (range ↑I) (↑(extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
c : M'
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x fun x => c) 0 (range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [writtenInExtChartAt, Function.comp_def, hasFDerivWithinAt_const]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma meas_le_lintegral₀ {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    {s : Set α} (hs : ∀ x ∈ s, 1 ≤ f x) : μ s ≤ ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ 1 * μ {x | 1 ≤ f x}

Tactic:
rw [one_mul]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ μ {x | 1 ≤ f x}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
apply le_trans _ (mul_meas_ge_le_lintegral₀ hf 1)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ 1 * μ {x | 1 ≤ f x}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ μ s ≤ μ {x | 1 ≤ f x}

Tactic:
exact measure_mono hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_ofList [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (ofList l).size = l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (ofList l).size = l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertMany_empty_list

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem blocksFun_le {n} (c : Composition n) (i : Fin c.length) :
    c.blocksFun i ≤ n

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
this : c.blocks.sum = n
⊢ c.blocksFun i ≤ n

Tactic:
have := List.le_sum_of_mem (c.blocksFun_mem_blocks i)

Result:
n : ℕ
c : Composition n
i : Fin c.length
this✝ : c.blocks.sum = n
this : c.blocksFun i ≤ c.blocks.sum
⊢ c.blocksFun i ≤ n

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
this✝ : c.blocks.sum = n
this : c.blocksFun i ≤ c.blocks.sum
⊢ c.blocksFun i ≤ n

Tactic:
simp_all

Result:
no goals

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
⊢ c.blocksFun i ≤ n

Tactic:
have := c.blocks_sum

Result:
n : ℕ
c : Composition n
i : Fin c.length
this : c.blocks.sum = n
⊢ c.blocksFun i ≤ n
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_left`. -/
lemma mul_div_mul_left_le (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
⊢ c * a / (c * b) ≤ a / b

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : 0 ≤ a / b
⊢ 0 * a / (0 * b) ≤ a / b

case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
hc : c ≠ 0
⊢ c * a / (c * b) ≤ a / b

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : 0 ≤ a / b
hc : c ≠ 0
⊢ c * a / (c * b) ≤ a / b

Tactic:
rw [mul_div_mul_left _ _ hc]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : 0 ≤ a / b
⊢ 0 * a / (0 * b) ≤ a / b

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem exists_sup_ge [SemilatticeSup β] [OrderBot β] [WellFoundedGT β] (f : α → β) :
    ∃ t : Finset α, ∀ a, f a ≤ t.sup f

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : IsEmpty α
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
exact ⟨⊥, isEmptyElim⟩

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
⊢ f a ≤ t.sup f

Tactic:
classical
have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
rwa [GT.gt, right_lt_sup, not_not] at this

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
⊢ (fun x => x.sup f) (insert a t) = f a ⊔ t.sup f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : IsEmpty α
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
⊢ f a ≤ t.sup f

Tactic:
have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
this : ¬f a ⊔ t.sup f > (fun x => x.sup f) t
⊢ f a ≤ t.sup f

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
this : ¬f a ⊔ t.sup f > (fun x => x.sup f) t
⊢ f a ≤ t.sup f

Tactic:
rwa [GT.gt, right_lt_sup, not_not] at this

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
refine ⟨t, fun a ↦ ?_⟩

Result:
case inr.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x => x.sup f, ¬x > (fun x => x.sup f) t
a : α
⊢ f a ≤ t.sup f
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
rw [Finset.prod_eq_mul_prod_diff_singleton ha]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
classical
  rw [Finset.prod_eq_mul_prod_diff_singleton ha]
  exact dvd_mul_right _ _

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem _root_.IsIdempotentElem.coe_powers {a : M} (ha : IsIdempotentElem a) :
    (Submonoid.powers a : Set M) = {1, a} :=
  let S : Submonoid M :=
  { carrier := {1, a},
    mul_mem'

Proof state:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

Tactic:
rw [mul_one]

Result:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ ∈ {1, a✝}

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ S ≤ powers a

Tactic:
rintro _ (rfl|rfl)

Result:
case inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ 1 ∈ powers a

case inr
M : Type u_1
inst✝ : Monoid M
x✝ : M
ha : IsIdempotentElem x✝
S : Submonoid M := { carrier := {1, x✝}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ x✝ ∈ powers x✝

Proof state:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

Tactic:
rw [one_mul]

Result:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 ∈ {1, a}

Proof state:
case inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
S : Submonoid M := { carrier := {1, a}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ 1 ∈ powers a

case inr
M : Type u_1
inst✝ : Monoid M
x✝ : M
ha : IsIdempotentElem x✝
S : Submonoid M := { carrier := {1, x✝}, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ x✝ ∈ powers x✝

Tactic:
exacts [one_mem _, Submonoid.mem_powers _]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ ∀ {a_1 b : M}, a_1 ∈ {1, a} → b ∈ {1, a} → a_1 * b ∈ {1, a}

Tactic:
rintro _ _ (rfl|rfl) (rfl|rfl)

Result:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Proof state:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 ∈ {1, a}

Tactic:
exact .inl rfl

Result:
no goals

Proof state:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ ∈ {1, a✝}

Tactic:
exact .inr rfl

Result:
no goals

Proof state:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Tactic:
rw [ha]

Result:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}

Proof state:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}

Tactic:
exact .inr rfl

Result:
no goals

Proof state:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

Tactic:
rw [one_mul]

Result:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}

Proof state:
case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ ∈ {1, b✝}

Tactic:
exact .inr rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_ofBoolListBE (h : i < bs.length) :
    (ofBoolListBE bs)[i] = bs[bs.length - 1 - i]

Proof state:
i : Nat
bs : List Bool
h : i < bs.length
⊢ (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) = bs[bs.length - 1 - i]

Tactic:
simp only [h, decide_true, List.getD_eq_getElem?_getD, Bool.true_and]

Result:
i : Nat
bs : List Bool
h : i < bs.length
⊢ bs[bs.length - 1 - i]?.getD false = bs[bs.length - 1 - i]

Proof state:
i : Nat
bs : List Bool
h : i < bs.length
⊢ bs.length - 1 - i < bs.length

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
bs : List Bool
h : i < bs.length
⊢ bs[bs.length - 1 - i]?.getD false = bs[bs.length - 1 - i]

Tactic:
rw [List.getElem?_eq_getElem (by omega)]

Result:
i : Nat
bs : List Bool
h : i < bs.length
⊢ (some bs[bs.length - 1 - i]).getD false = bs[bs.length - 1 - i]

Proof state:
i : Nat
bs : List Bool
h : i < bs.length
⊢ (ofBoolListBE bs)[i] = bs[bs.length - 1 - i]

Tactic:
rw [← getLsbD_eq_getElem, getLsbD_ofBoolListBE]

Result:
i : Nat
bs : List Bool
h : i < bs.length
⊢ (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) = bs[bs.length - 1 - i]

Proof state:
i : Nat
bs : List Bool
h : i < bs.length
⊢ (some bs[bs.length - 1 - i]).getD false = bs[bs.length - 1 - i]

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cone.ofFork_π {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) (j) :
    (Cone.ofFork t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Nat.lean
theorem natSumNatEquivNat_apply : ⇑natSumNatEquivNat = Sum.elim (2 * ·) (2 * · + 1)

Proof state:
⊢ ⇑natSumNatEquivNat = Sum.elim (fun x => 2 * x) fun x => 2 * x + 1

Tactic:
ext (x | x) <;> rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Lex.lean
theorem Lex.single_strictAnti : StrictAnti (fun (a : α) ↦ toLex (single a 1))

Proof state:
case h.right
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (single b 1) a < (single a 1) a

Tactic:
simp only [single_eq_same, single_eq_of_ne (ne_of_lt h).symm, zero_lt_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a => toLex (single a 1)

Tactic:
intro a b h

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (fun a => toLex (single a 1)) b < (fun a => toLex (single a 1)) a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (fun a => toLex (single a 1)) b < (fun a => toLex (single a 1)) a

Tactic:
simp only [LT.lt, Finsupp.lex_def]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j,
    (∀ d < j, (ofLex (toLex (single b 1))) d = (ofLex (toLex (single a 1))) d) ∧
      ((ofLex (toLex (single b 1))) j).lt ((ofLex (toLex (single a 1))) j)

Proof state:
case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∀ d < a, (single b 1) d = (single a 1) d

Tactic:
intro d hd

Result:
case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
d : α
hd : d < a
⊢ (single b 1) d = (single a 1) d

Proof state:
case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
d : α
hd : d < a
⊢ (single b 1) d = (single a 1) d

Tactic:
simp only [Finsupp.single_eq_of_ne hd.ne', Finsupp.single_eq_of_ne (hd.trans h).ne']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j,
    (∀ d < j, (ofLex (toLex (single b 1))) d = (ofLex (toLex (single a 1))) d) ∧
      ((ofLex (toLex (single b 1))) j).lt ((ofLex (toLex (single a 1))) j)

Tactic:
simp only [ofLex_toLex, Nat.lt_eq]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j, (∀ d < j, (single b 1) d = (single a 1) d) ∧ (single b 1) j < (single a 1) j

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ j, (∀ d < j, (single b 1) d = (single a 1) d) ∧ (single b 1) j < (single a 1) j

Tactic:
use a

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (∀ d < a, (single b 1) d = (single a 1) d) ∧ (single b 1) a < (single a 1) a

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (∀ d < a, (single b 1) d = (single a 1) d) ∧ (single b 1) a < (single a 1) a

Tactic:
constructor

Result:
case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∀ d < a, (single b 1) d = (single a 1) d

case h.right
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (single b 1) a < (single a 1) a
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_naturality_right (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
    (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ X ◁ Y ◁ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (X ⊗ Y) ◁ f ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ X ◁ Y ◁ f

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_adj_penultimate {u v} (w : G.Walk u v) (h : ¬ w.Nil) :
    w.toSubgraph.Adj w.penultimate v

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 < w.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
rw [not_nil_iff_lt_length] at h

Result:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 + 1 = w.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.toSubgraph.Adj w.penultimate v

Tactic:
simpa [show w.length - 1 + 1 = w.length from by omega]
  using w.toSubgraph_adj_getVert (by omega : w.length - 1 < w.length)

Result:
no goals