harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Stream/Init.lean
theorem get_interleave_right : ∀ (n : ℕ) (s₁ s₂ : Stream' α),
    get (s₁ ⋈ s₂) (2 * n + 1) = get s₂ n
  | 0, _, _ => rfl
  | n + 1, s₁, s₂ => by
    change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)
    rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
      get_interleave_right n (tail s₁) (tail s₂)]
    rfl

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ

Tactic:
rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
  get_interleave_right n (tail s₁) (tail s₂)]

Result:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)

Tactic:
change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)

Result:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_vecAlt0 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
    vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (by omega) u)

Proof state:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

Result:
case h.mk.zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

case h.mk.succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Proof state:
α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)

Tactic:
ext i

Result:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Proof state:
case h.mk.succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
  cons_vecAppend, Nat.add_eq, vecAlt0]

Result:
no goals

Proof state:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt0 h (vecCons x (vecCons y u)) i = vecCons x (vecAlt0 ⋯ u) i

Tactic:
simp_rw [vecAlt0]

Result:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) i

Proof state:
case h.mk.zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem add {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x + y)

Proof state:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)

Tactic:
simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem eventuallyEq_one : f =ᶠ[𝓝 c] 1 :=
  f.eventuallyEq_one_of_dist_lt (mem_chart_source _ _) <| by rw [dist_self]; exact f.rIn_pos

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ dist (↑(extChartAt I c) c) (↑(extChartAt I c) c) < f.rIn

Tactic:
rw [dist_self]

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ 0 < f.rIn

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ 0 < f.rIn

Tactic:
exact f.rIn_pos

Result:
no goals
-- Mathlib/Logic/Encodable/Basic.lean
theorem up_down {a : α} : (down a).up = a

Proof state:
α : Type u_1
inst✝ : Encodable α
a : α
⊢ (down a).up = a

Tactic:
simp [up, down,Equiv.left_inv _ _, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers [Infinite α] {g : α}
    (h : ∀ x, x ∈ zpowers g) : orderOf g = 0

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0

Tactic:
rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem size_zero_iff_forall_not_mem {l : Vector α n} : n = 0 ↔ ∀ a, a ∉ l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ n = 0 ↔ ∀ (a : α), ¬a ∈ l

Tactic:
simpa using List.eq_nil_iff_forall_not_mem (l := l.toList)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem cosh_arsinh (x : ℝ) : cosh (arsinh x) = √(1 + x ^ 2)

Proof state:
x : ℝ
⊢ cosh (arsinh x) = √(1 + x ^ 2)

Tactic:
rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem frontier_prod_eq (s : Set X) (t : Set Y) :
    frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
⊢ frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t

Tactic:
simp only [frontier, closure_prod_eq, interior_prod_eq, prod_diff_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_le_ne {x y : BitVec n} : x ≤ y → ¬ x = y → x < y

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat → ¬x.toNat = y.toNat → x.toNat < y.toNat

Tactic:
apply Nat.lt_of_le_of_ne

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x ≤ y → ¬x = y → x < y

Tactic:
simp only [lt_def, le_def, BitVec.toNat_eq]

Result:
n : Nat
x y : BitVec n
⊢ x.toNat ≤ y.toNat → ¬x.toNat = y.toNat → x.toNat < y.toNat
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem invEmbedding_comp (i : Fin c.length) (j : Fin (c.blocksFun i)) :
    (c.invEmbedding (c.embedding i j) : ℕ) = j

Proof state:
n : ℕ
c : Composition n
i : Fin c.length
j : Fin (c.blocksFun i)
⊢ ↑(c.invEmbedding ((c.embedding i) j)) = ↑j

Tactic:
simp_rw [coe_invEmbedding, index_embedding, coe_embedding, add_tsub_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Vector α n)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldr f' (g a) = g (l.foldr f a)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Vector α n
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldr f' (g a) (map g l) = g (foldr f a l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ foldr f' (g a) (map g { toArray := l, size_toArray := ⋯ }) = g (foldr f a { toArray := l, size_toArray := ⋯ })

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ Array.foldr f' (g a) (Array.map g l) l.size = g (Array.foldr f a l)

Tactic:
rw [Array.foldr_map_hom' _ _ _ _ _ h rfl]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ foldr f' (g a) (map g { toArray := l, size_toArray := ⋯ }) = g (foldr f a { toArray := l, size_toArray := ⋯ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
l : Array α
⊢ Array.foldr f' (g a) (Array.map g l) l.size = g (Array.foldr f a l)
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem mk_coord_apply_ne {i j : ι} (h : j ≠ i) : (Basis.mk hli hsp).coord i (v j) = 0 :=
  show hli.repr ⟨v j, Submodule.subset_span (mem_range_self j)⟩ i = 0 by
    simp [hli.repr_eq_single j, h]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
i j : ι
h : j ≠ i
⊢ (hli.repr ⟨v j, ⋯⟩) i = 0

Tactic:
simp [hli.repr_eq_single j, h]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[simp, reassoc]
lemma map_comp : map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂

Proof state:
case a
C : Type u_1
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (φ ≫ ψ) c₁₂) =
    (HomologicalComplex.forget C c₁₂).map (map φ c₁₂ ≫ map ψ c₁₂)

Tactic:
exact GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ map (φ ≫ ψ) c₁₂ = map φ c₁₂ ≫ map ψ c₁₂

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Result:
case a
C : Type u_1
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (φ ≫ ψ) c₁₂) =
    (HomologicalComplex.forget C c₁₂).map (map φ c₁₂ ≫ map ψ c₁₂)
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive]
lemma HasCompactMulSupport.exists_pos_le_norm [One E] (hf : HasCompactMulSupport f) :
    ∃ R : ℝ, 0 < R ∧ ∀ x : α, R ≤ ‖x‖ → f x = 1

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩⟩ := exists_compact_iff_hasCompactMulSupport.mpr hf

Result:
case intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ 0 < S + 1

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : S + 1 ≤ ‖x‖
⊢ ¬‖x‖ ≤ S

Tactic:
contrapose! hx

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : ‖x‖ ≤ S
⊢ ‖x‖ < S + 1

Tactic:
exact lt_add_of_le_of_pos hx zero_lt_one

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
refine ⟨S + 1, by positivity, fun x hx => hK2 x ((mt <| hS' x) ?_)⟩

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
x : α
hx : S + 1 ≤ ‖x‖
⊢ ¬‖x‖ ≤ S

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
obtain ⟨S, hS, hS'⟩ := hK1.isBounded.exists_pos_norm_le

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_eq_countP' {a : α} : count a = countP (· == a)

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
⊢ count a = countP fun x => x == a

Tactic:
funext l

Result:
case h
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ count a l = countP (fun x => x == a) l

Proof state:
case h
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ count a l = countP (fun x => x == a) l

Tactic:
apply count_eq_countP

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem ghostComponent_frobeniusFun (n : ℕ) (x : 𝕎 R) :
    ghostComponent n (frobeniusFun x) = ghostComponent (n + 1) x

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
x : 𝕎 R
⊢ (ghostComponent n) x.frobeniusFun = (ghostComponent (n + 1)) x

Tactic:
simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial,
  aeval_bind₁]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_pos_iff : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem isTwoCoboundary_of_mem_twoCoboundaries
    (f : G × G → A) (hf : f ∈ twoCoboundaries (Rep.ofDistribMulAction k G A)) :
    IsTwoCoboundary f

Proof state:
case intro
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : G → ↑(Rep.ofDistribMulAction k G A).V
⊢ IsTwoCoboundary ((dOne (Rep.ofDistribMulAction k G A)) a)

Tactic:
exact ⟨a, fun _ _ => rfl⟩

Result:
no goals

Proof state:
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G × G → A
hf : f ∈ twoCoboundaries (Rep.ofDistribMulAction k G A)
⊢ IsTwoCoboundary f

Tactic:
rcases hf with ⟨a, rfl⟩

Result:
case intro
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : G → ↑(Rep.ofDistribMulAction k G A).V
⊢ IsTwoCoboundary ((dOne (Rep.ofDistribMulAction k G A)) a)
-- Mathlib/Topology/Constructions.lean
theorem prod_induced_induced {X Z} (f : X → Y) (g : Z → W) :
    @instTopologicalSpaceProd X Z (induced f ‹_›) (induced g ‹_›) =
      induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd

Proof state:
Y : Type v
W : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced (f ∘ Prod.fst) inst✝¹ ⊓ induced (g ∘ Prod.snd) inst✝ =
    induced (Prod.fst ∘ fun p => (f p.1, g p.2)) inst✝¹ ⊓ induced (Prod.snd ∘ fun p => (f p.1, g p.2)) inst✝

Tactic:
rfl

Result:
no goals

Proof state:
Y : Type v
W : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced Prod.fst (induced f inst✝¹) ⊓ induced Prod.snd (induced g inst✝) =
    induced (fun p => (f p.1, g p.2)) (induced Prod.fst inst✝¹ ⊓ induced Prod.snd inst✝)

Tactic:
simp_rw [induced_inf, induced_compose]

Result:
Y : Type v
W : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced (f ∘ Prod.fst) inst✝¹ ⊓ induced (g ∘ Prod.snd) inst✝ =
    induced (Prod.fst ∘ fun p => (f p.1, g p.2)) inst✝¹ ⊓ induced (Prod.snd ∘ fun p => (f p.1, g p.2)) inst✝

Proof state:
Y : Type v
W : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ instTopologicalSpaceProd = induced (fun p => (f p.1, g p.2)) instTopologicalSpaceProd

Tactic:
delta instTopologicalSpaceProd

Result:
Y : Type v
W : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace W
X : Type u_5
Z : Type u_6
f : X → Y
g : Z → W
⊢ induced Prod.fst (induced f inst✝¹) ⊓ induced Prod.snd (induced g inst✝) =
    induced (fun p => (f p.1, g p.2)) (induced Prod.fst inst✝¹ ⊓ induced Prod.snd inst✝)
-- Mathlib/Topology/Bornology/Constructions.lean
theorem isBounded_prod_self : IsBounded (s ×ˢ s) ↔ IsBounded s

Proof state:
α : Type u_1
inst✝ : Bornology α
s : Set α
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Result:
case inl
α : Type u_1
inst✝ : Bornology α
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Proof state:
case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : Bornology α
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem takeWhile_toArray (p : α → Bool) (l : List α) :
    l.toArray.takeWhile p = (l.takeWhile p).toArray

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ Array.takeWhile p l.toArray = (takeWhile p l).toArray

Tactic:
simp [Array.takeWhile, takeWhile_go_toArray]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem toSubring_injective : Function.Injective (toSubring : ValuationSubring K → Subring K) :=
  fun x y h => by cases x; cases y; congr

Proof state:
K : Type u
inst✝ : Field K
x y : ValuationSubring K
h : x.toSubring = y.toSubring
⊢ x = y

Tactic:
cases x

Result:
case mk
K : Type u
inst✝ : Field K
y : ValuationSubring K
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h : { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring = y.toSubring
⊢ { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ } = y

Proof state:
case mk.mk
K : Type u
inst✝ : Field K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
K : Type u
inst✝ : Field K
y : ValuationSubring K
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h : { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring = y.toSubring
⊢ { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ } = y

Tactic:
cases y

Result:
case mk.mk
K : Type u
inst✝ : Field K
toSubring✝¹ : Subring K
mem_or_inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier ∨ x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
mem_or_inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier ∨ x⁻¹ ∈ toSubring✝.carrier
h :
  { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ }.toSubring =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }.toSubring
⊢ { toSubring := toSubring✝¹, mem_or_inv_mem' := mem_or_inv_mem'✝¹ } =
    { toSubring := toSubring✝, mem_or_inv_mem' := mem_or_inv_mem'✝ }
-- Mathlib/RingTheory/Invariant.lean
theorem charpoly_eq_prod_smul (b : B) : charpoly G b = ∏ g : G, g • (X - C b)

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ charpoly G b = ∏ g : G, g • (X - C b)

Tactic:
simp only [smul_sub, smul_C, smul_X, charpoly_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.isBase_of_ground_subset_closure (hI : M.Indep I) (h : M.E ⊆ M.closure I) :
    M.IsBase I

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBase I

Tactic:
rw [← isBasis_ground_iff]

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
h : M.E ⊆ M.closure I
⊢ M.IsBasis I M.E

Tactic:
exact hI.isBasis_of_subset_of_subset_closure hI.subset_ground h

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
/-- For a based functor `F : 𝒳 ⟶ 𝒴`, and an arrow `φ` in `𝒳`, then `φ` lifts an arrow `f` in `𝒮`
if `F(φ)` does. -/
lemma isHomLift_map [IsHomLift 𝒴.p f (F.map φ)] : IsHomLift 𝒳.p f φ

Proof state:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ 𝒳.p.IsHomLift f φ

Tactic:
apply of_fac 𝒳.p f φ  (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ))
  (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))

Result:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯

Proof state:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒴.p.IsHomLift f (F.map φ)
⊢ f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯

Tactic:
simp [congr_hom F.w.symm, fac 𝒴.p f (F.map φ)]

Result:
no goals