harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/Ring/Basic.lean
theorem div_pf {R} [DivisionRing R] {a b c d : R} (_ : b⁻¹ = c) (_ : a * c = d) : a / b = d

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a b c d : R
x✝¹ : b⁻¹ = c
x✝ : a * c = d
⊢ a / b = d

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : DivisionRing R
a b : R
⊢ a / b = a * b⁻¹

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a b : R
⊢ a / b = a * b⁻¹

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
lemma IsAlgebraic.invOf {x : S} [Invertible x] (h : IsAlgebraic R x) : IsAlgebraic R (⅟ x)

Proof state:
case intro.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ (aeval ⅟x) p.reverse = 0

Tactic:
rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]

Result:
no goals

Proof state:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ p.reverse ≠ 0

Tactic:
simpa using hp

Result:
no goals

Proof state:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
h : IsAlgebraic R x
⊢ IsAlgebraic R ⅟x

Tactic:
obtain ⟨p, hp, hp'⟩ := h

Result:
case intro.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ IsAlgebraic R ⅟x

Proof state:
case intro.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ IsAlgebraic R ⅟x

Tactic:
refine ⟨p.reverse, by simpa using hp, ?_⟩

Result:
case intro.intro
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ (aeval ⅟x) p.reverse = 0
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem iterate_bijective (h : Bijective f') : ∀ n : ℕ, Bijective (f' ^ n)
  | 0 => bijective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_bijective h n).comp h

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑((f' ^ n) ∘ₗ f')

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑((f' ^ n) ∘ₗ f')

Tactic:
exact (iterate_bijective h n).comp h

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem left_cancel_inv (x : R) {y y' : R} : x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

Proof state:
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'

case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ y = y' → x ◃⁻¹ y = x ◃⁻¹ y'

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y

Proof state:
case mp
R : Type u_1
inst✝ : Rack R
x y y' : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y' → y = y'

Tactic:
apply (act' x).symm.injective

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ y = x ◃⁻¹ y

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_smul_right (x y : V) (r : ℝ) :
    (o.oangle x (y - r • x)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle x (y - r • x)).sign = (o.oangle x y).sign

Tactic:
rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval₂_comp {x : S} : eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))

Tactic:
simp [eval₂_finset_sum, eval₂_pow]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p

Tactic:
rw [comp, p.as_sum_range]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))
-- Mathlib/Data/List/Lattice.lean
theorem forall_mem_union : (∀ x ∈ l₁ ∪ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst✝ : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_union_iff, or_imp, forall_and]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem length_toList {xs : t α} : length xs = List.length (toList xs)

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length

Tactic:
rw [← Nat.add_zero ys.length]

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length + 0

Proof state:
case nil
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } []).down = [].length + n

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
head✝ : α
tail✝ : List α
ih : ∀ (n : ℕ), (List.foldl (fun l x => { down := l.down + 1 }) { down := n } tail✝).down = tail✝.length + n
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } (head✝ :: tail✝)).down = (head✝ :: tail✝).length + n

Tactic:
simp_arith [ih]

Result:
no goals

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length + 0

Tactic:
generalize 0 = n

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = ys.length + n

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = (toList xs).length

Tactic:
rw [foldl_toList]

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = (toList xs).length

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = (toList xs).length

Tactic:
generalize toList xs = ys

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x => { down := l.down + 1 }) { down := n } ys).down = ys.length + n

Tactic:
induction ys generalizing n with
| nil => simp
| cons _ _ ih => simp_arith [ih]

Result:
no goals

Proof state:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = (toList xs).length

Tactic:
unfold length

Result:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = (toList xs).length
-- Mathlib/SetTheory/Ordinal/Basic.lean
/--
A variation on `Cardinal.lt_ord` using `≤`: If `o` is no greater than the
initial ordinal of cardinality `c`, then its cardinal is no greater than `c`.

The converse, however, is false (for instance, `o = ω+1` and `c = ℵ₀`).
-/
lemma card_le_of_le_ord {o : Ordinal} {c : Cardinal} (ho : o ≤ c.ord) :
    o.card ≤ c

Proof state:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c

Tactic:
rw [← card_ord c]

Result:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Proof state:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
exact Ordinal.card_le_card ho

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma bind_toFinset [DecidableEq α] (s : Multiset α) (t : α → Multiset β) :
    (s.bind t).toFinset = s.toFinset.biUnion fun a ↦ (t a).toFinset :=
  ext fun x ↦ by simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ (s.bind t).toFinset ↔ x ∈ s.toFinset.biUnion fun a => (t a).toFinset

Tactic:
simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k

Proof state:
n m k : ℕ
⊢ n.dist k ≤ n.dist m + m.dist k

Tactic:
have : dist n m + dist m k = n - m + (m - k) + (k - m + (m - n)) := by
  simp [dist, add_comm, add_left_comm, add_assoc]

Result:
n m k : ℕ
this : n.dist m + m.dist k = n - m + (m - k) + (k - m + (m - n))
⊢ n.dist k ≤ n.dist m + m.dist k

Proof state:
n m k : ℕ
⊢ n.dist m + m.dist k = n - m + (m - k) + (k - m + (m - n))

Tactic:
simp [dist, add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
n m k : ℕ
this : n.dist m + m.dist k = n - m + (m - k) + (k - m + (m - n))
⊢ n.dist k ≤ n.dist m + m.dist k

Tactic:
rw [this, dist]

Result:
n m k : ℕ
this : n.dist m + m.dist k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))

Proof state:
n m k : ℕ
this : n.dist m + m.dist k = n - m + (m - k) + (k - m + (m - n))
⊢ n - k + (k - n) ≤ n - m + (m - k) + (k - m + (m - n))

Tactic:
exact add_le_add tsub_le_tsub_add_tsub tsub_le_tsub_add_tsub

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem repr_opow_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : Ordinal} (e0 : repr e ≠ 0)
    (h : a' < (ω : Ordinal.{0}) ^ repr e) (aa : repr a = a') (n : ℕ+) :
    ((ω : Ordinal.{0}) ^ repr e * (n : ℕ) + a') ^ (ω : Ordinal.{0}) =
      (ω ^ repr e) ^ (ω : Ordinal.{0})

Proof state:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
have No := Ne.oadd n (Na.below_of_lt' h)

Result:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Proof state:
case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ≤ e.repr * ω

Tactic:
simpa using mul_le_mul_right' (one_le_iff_ne_zero.2 e0) ω

Result:
no goals

Proof state:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ (e.oadd n a).repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
rw [repr] at this

Result:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Proof state:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ succ e.repr * b ≤ e.repr * ω

Tactic:
rcases le_or_lt ω (repr e) with h | h

Result:
case inl
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ succ e.repr * b ≤ e.repr * ω

case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ succ e.repr * b ≤ e.repr * ω
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfcHom_le_iff {a : A} (ha : p a) {f g : C(spectrum R a, R)} :
    cfcHom ha f ≤ cfcHom ha g ↔ f ≤ g

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.776006) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f g : C(↑(spectrum R a), R)
⊢ (cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g

Tactic:
rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem iota_eq_iotaTR : @iota = @iotaTR :=
  have aux (n : Nat) (r : List Nat) : iotaTR.go n r = r.reverse ++ iota n

Proof state:
case zero
r : List Nat
⊢ iotaTR.go 0 r = r.reverse ++ iota 0

Tactic:
simp [iota, iotaTR.go]

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ (r : List Nat), iotaTR.go n r = r.reverse ++ iota n
r : List Nat
⊢ iotaTR.go (n + 1) r = r.reverse ++ iota (n + 1)

Tactic:
simp [iota, iotaTR.go, ih, append_assoc]

Result:
no goals

Proof state:
n : Nat
r : List Nat
⊢ iotaTR.go n r = r.reverse ++ iota n

Tactic:
induction n generalizing r with
| zero => simp [iota, iotaTR.go]
| succ n ih => simp [iota, iotaTR.go, ih, append_assoc]

Result:
no goals

Proof state:
aux : ∀ (n : Nat) (r : List Nat), iotaTR.go n r = r.reverse ++ iota n
n : Nat
⊢ iota n = iotaTR n

Tactic:
simp [iotaTR, aux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem IsPrefix.eraseP (h : l₁ <+: l₂) : l₁.eraseP p <+: l₂.eraseP p

Proof state:
case intro
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
⊢ eraseP p l₁ <+: eraseP p (l₁ ++ t)

Tactic:
rw [eraseP_append]

Result:
case intro
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
⊢ eraseP p l₁ <+: if l₁.any p = true then eraseP p l₁ ++ t else l₁ ++ eraseP p t

Proof state:
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : ¬l₁.any p = true
⊢ ∀ (a : α✝), a ∈ l₁ → ¬p a = true

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.isFalse
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : ¬l₁.any p = true
⊢ eraseP p l₁ <+: l₁ ++ eraseP p t

Tactic:
rw [eraseP_of_forall_not (by simp_all)]

Result:
case intro.isFalse
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : ¬l₁.any p = true
⊢ l₁ <+: l₁ ++ eraseP p t

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : l₁ <+: l₂
⊢ eraseP p l₁ <+: eraseP p l₂

Tactic:
rw [IsPrefix] at h

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ eraseP p l₁ <+: eraseP p l₂

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ eraseP p l₁ <+: eraseP p l₂

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
⊢ eraseP p l₁ <+: eraseP p (l₁ ++ t)

Proof state:
case intro
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
⊢ eraseP p l₁ <+: if l₁.any p = true then eraseP p l₁ ++ t else l₁ ++ eraseP p t

Tactic:
split

Result:
case intro.isTrue
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : l₁.any p = true
⊢ eraseP p l₁ <+: eraseP p l₁ ++ t

case intro.isFalse
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : ¬l₁.any p = true
⊢ eraseP p l₁ <+: l₁ ++ eraseP p t

Proof state:
case intro.isFalse
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : ¬l₁.any p = true
⊢ l₁ <+: l₁ ++ eraseP p t

Tactic:
exact prefix_append l₁ (eraseP p t)

Result:
no goals

Proof state:
case intro.isTrue
α✝ : Type u_1
l₁ : List α✝
p : α✝ → Bool
t : List α✝
h✝ : l₁.any p = true
⊢ eraseP p l₁ <+: eraseP p l₁ ++ t

Tactic:
exact prefix_append (eraseP p l₁) t

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma isFlat_iff_isClosed : M.IsFlat F ↔ ∃ h : F ⊆ M.E, M.subtypeClosure.IsClosed ⟨F, h⟩

Proof state:
α : Type u_2
M : Matroid α
F : Set α
⊢ M.IsFlat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩

Tactic:
simpa [subtypeClosure] using IsFlat.subset_ground

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem option_map {f : α → Option β} {g : α → β → σ} (hf : Computable f) (hg : Computable₂ g) :
    Computable fun a => (f a).map (g a)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
⊢ Computable fun a => Option.map (g a) (f a)

Tactic:
convert option_bind hf (option_some.comp₂ hg)

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
x✝ : α
⊢ Option.map (g x✝) (f x✝) = (f x✝).bind fun b => Option.some (g x✝ b)

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
x✝ : α
⊢ Option.map (g x✝) (f x✝) = (f x✝).bind fun b => Option.some (g x✝ b)

Tactic:
apply Option.map_eq_bind

Result:
no goals
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Ioo : #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem bot : Ideal.IsHomogeneous 𝒜 ⊥ := fun i r hr => by
  simp only [Ideal.mem_bot] at hr
  rw [hr, decompose_zero, zero_apply]
  apply Ideal.zero_mem

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑0 ∈ ⊥

Tactic:
apply Ideal.zero_mem

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r ∈ ⊥
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Tactic:
simp only [Ideal.mem_bot] at hr

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑(((decompose 𝒜) r) i) ∈ ⊥

Tactic:
rw [hr, decompose_zero, zero_apply]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : r = 0
⊢ ↑0 ∈ ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_none_iff_findIdx_eq {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = none ↔ xs.findIdx p = xs.size

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = none ↔ findIdx p { toList := xs } = { toList := xs }.size

Tactic:
simp [List.findIdx?_eq_none_iff_findIdx_eq]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ findIdx? p xs = none ↔ findIdx p xs = xs.size

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ findIdx? p { toList := xs } = none ↔ findIdx p { toList := xs } = { toList := xs }.size
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma eq_one_iff {χ : MulChar R R'} : χ = 1 ↔ ∀ a : Rˣ, χ a = 1

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ = 1 ↔ ∀ (a : Rˣ), χ ↑a = 1

Tactic:
simp only [MulChar.ext_iff, one_apply_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem image_mul_right : image (· * b) t = preimage t (· * b⁻¹) (mul_left_injective _).injOn :=
  coe_injective <| by simp

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

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) {hc : k ∈ m.alter k f} : (m.alter k f).getKey k hc = k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k ∈ m.alter k f
⊢ (m.alter k f).getKey k hc = k

Tactic:
simp [getKey_alter h]

Result:
no goals