harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_gcd (m n : ℕ+) :
    factorMultiset (gcd m n) = factorMultiset m ⊓ factorMultiset n

Proof state:
case a.left
m n : ℕ+
⊢ m.gcd n ∣ m

Tactic:
exact gcd_dvd_left m n

Result:
no goals

Proof state:
case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset

Tactic:
apply le_inf_iff.mpr

Result:
case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset

Proof state:
case a.right
m n : ℕ+
⊢ m.gcd n ∣ n

Tactic:
exact gcd_dvd_right m n

Result:
no goals

Proof state:
case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Tactic:
rw [← PrimeMultiset.prod_dvd_iff, prod_factorMultiset]

Result:
case a
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n

Proof state:
m n : ℕ+
⊢ (m.gcd n).factorMultiset = m.factorMultiset ⊓ n.factorMultiset

Tactic:
apply le_antisymm

Result:
case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset

case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Proof state:
case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ∧ (m.gcd n).factorMultiset ≤ n.factorMultiset

Tactic:
constructor <;> apply factorMultiset_le_iff.mpr

Result:
case a.left
m n : ℕ+
⊢ m.gcd n ∣ m

case a.right
m n : ℕ+
⊢ m.gcd n ∣ n

Proof state:
case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
case a
m n : ℕ+
⊢ (m.factorMultiset ⊓ n.factorMultiset).prod ∣ m.gcd n

Tactic:
apply dvd_gcd <;> rw [PrimeMultiset.prod_dvd_iff']

Result:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

case a.hn
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ n.factorMultiset

Proof state:
case a.hm
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ m.factorMultiset

Tactic:
exact inf_le_left

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem is_left_invariant_chaar {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
    chaar K₀ (K.map _ <| continuous_mul_left g) = chaar K₀ K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ chaar K₀ (Compacts.map (fun b => g * b) ⋯ K) - chaar K₀ K = 0

Tactic:
show chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' {0}

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}

Tactic:
unfold clPrehaar

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ chaar K₀ ∈ eval ⁻¹' {0}

Tactic:
apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f (Compacts.map (fun b => g * b) ⋯ K) - f K
this : Continuous eval
⊢ clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {0}
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp] lemma orthogonal_span_coroot_eq_ker (α : Weight K H L) :
    (traceForm K H L).orthogonal (K ∙ coroot α) = α.ker

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
hα' : coroot α = 0
⊢ Weight.ker = ⊤

Tactic:
ext

Result:
case h
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsZero
hα' : coroot α = 0
x✝ : ↥H
⊢ x✝ ∈ Weight.ker ↔ x✝ ∈ ⊤

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
⊢ (traceForm K (↥H) L).orthogonal (span K {coroot α}) = Weight.ker

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)

Result:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : x ∈ (traceForm K (↥H) L).orthogonal (span K {coroot α})
⊢ x ∈ Weight.ker

case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : ¬α.IsZero
x : ↥H
hx : x ∈ Weight.ker
y : ↥H
hy : y ∈ span K {coroot α}
⊢ (traceForm K (↥H) L).IsOrtho y x
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem one_le_of_le_mul_right [MulLeftReflectLE α] {a b : α} (h : a ≤ a * b) :
    1 ≤ b :=
  le_of_mul_le_mul_left' (a := a) <| by simpa only [mul_one]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulLeftReflectLE α
a b : α
h : a ≤ a * b
⊢ a * 1 ≤ a * b

Tactic:
simpa only [mul_one]

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem map_iterate (f : α → α) (g : β → β) (n : ℕ) :
    (Prod.map f g)^[n] = Prod.map f^[n] g^[n]

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
n : ℕ
⊢ (map f g)^[n] = map f^[n] g^[n]

Tactic:
induction n <;> simp [*, Prod.map_comp_map]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iInf_eq_generate (s : ι → Filter α) : iInf s = generate (⋃ i, (s i).sets) :=
  eq_of_forall_le_iff fun _ ↦ by simp [le_generate_iff]

Proof state:
α : Type u
ι : Sort x
s : ι → Filter α
x✝ : Filter α
⊢ x✝ ≤ iInf s ↔ x✝ ≤ generate (⋃ i, (s i).sets)

Tactic:
simp [le_generate_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
lemma weightedVSubOfPoint_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V]
    (s : Finset ι) (w : ι → k) (p : ι → V) (b : V) (a : G) :
    s.weightedVSubOfPoint (a • p) b w = a • s.weightedVSubOfPoint p (a⁻¹ • b) w

Proof state:
k : Type u_1
V : Type u_2
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ι : Type u_4
G : Type u_6
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
s : Finset ι
w : ι → k
p : ι → V
b : V
a : G
⊢ (s.weightedVSubOfPoint (a • p) b) w = a • (s.weightedVSubOfPoint p (a⁻¹ • b)) w

Tactic:
simp [smul_sum, smul_sub, smul_comm a (w _)]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/ModN.lean
lemma basis_apply_eq_mkQ {ι : Type*} (b : Basis ι ℤ G) (i : ι) : basis b i = mkQ n (b i)

Proof state:
G : Type u_1
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ (basis b) i = (mkQ n) (b i)

Tactic:
rw [Basis.apply_eq_iff]

Result:
G : Type u_1
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ (basis b).repr ((mkQ n) (b i)) = single i 1

Proof state:
G : Type u_1
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ (basis b).repr ((mkQ n) (b i)) = single i 1

Tactic:
simp [basis, mkQ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
cases isEmpty_or_nonempty n

Result:
case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ A⁻¹.det = Ring.inverse A.det

case neg.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : Nonempty n
⊢ A⁻¹.det = Ring.inverse A.det

Proof state:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
letI := invertibleOfDetInvertible A

Result:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
⊢ A⁻¹.det = Ring.inverse A.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
by_cases h : IsUnit A.det

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹.det = Ring.inverse A.det

case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹.det = Ring.inverse A.det

Proof state:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
this : Invertible A := A.invertibleOfDetInvertible
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]

Result:
no goals

Proof state:
case neg.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : Nonempty n
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]

Result:
no goals

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
cases h.nonempty_invertible

Result:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
⊢ A⁻¹.det = Ring.inverse A.det

Proof state:
case neg.inl
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
h✝ : IsEmpty n
⊢ A⁻¹.det = Ring.inverse A.det

Tactic:
rw [det_isEmpty, det_isEmpty, Ring.inverse_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_eq_zero_iff {x : ℝ≥0} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Proof state:
x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]

Result:
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0

Proof state:
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0

Tactic:
exact Real.rpow_eq_zero_iff_of_nonneg x.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem getElem_eraseIdx_of_ge (l : Array α) (i : Nat) (w : i < l.size) (j : Nat) (h : j < (l.eraseIdx i).size) (h' : i ≤ j) :
    (l.eraseIdx i)[j] = l[j + 1]'(by simp at h; omega)

Proof state:
case mk
α : Type u_1
i j : Nat
h' : i ≤ j
l : List α
w : i < { toList := l }.size
h : j < ({ toList := l }.eraseIdx i w).size
⊢ ({ toList := l }.eraseIdx i w)[j] = { toList := l }[j + 1]

Tactic:
simp [List.getElem_eraseIdx_of_ge, *]

Result:
no goals

Proof state:
α : Type ?u.66833
l : Array α
i : Nat
w : i < l.size
j : Nat
h' : i ≤ j
h : j < l.size - 1
⊢ j + 1 < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.66833
l : Array α
i : Nat
w : i < l.size
j : Nat
h : j < (l.eraseIdx i w).size
h' : i ≤ j
⊢ j + 1 < l.size

Tactic:
simp at h

Result:
α : Type ?u.66833
l : Array α
i : Nat
w : i < l.size
j : Nat
h' : i ≤ j
h : j < l.size - 1
⊢ j + 1 < l.size

Proof state:
α : Type u_1
l : Array α
i : Nat
w : i < l.size
j : Nat
h : j < (l.eraseIdx i w).size
h' : i ≤ j
⊢ (l.eraseIdx i w)[j] = l[j + 1]

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i j : Nat
h' : i ≤ j
l : List α
w : i < { toList := l }.size
h : j < ({ toList := l }.eraseIdx i w).size
⊢ ({ toList := l }.eraseIdx i w)[j] = { toList := l }[j + 1]
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem addRothNumber_Ico (a b : ℕ) : addRothNumber (Ico a b) = rothNumberNat (b - a)

Proof state:
case h.e'_2.h.e'_6
a b : ℕ
h : a ≤ b
⊢ Ico a b = image (⇑(addLeftEmbedding a)) (Ico 0 (b - a))

Tactic:
convert (image_add_left_Ico 0 (b - a) _).symm

Result:
case h.e'_2.h.e'_5
a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)

Proof state:
a b : ℕ
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

Tactic:
obtain h | h := le_total b a

Result:
case inl
a b : ℕ
h : b ≤ a
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

case inr
a b : ℕ
h : a ≤ b
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

Proof state:
case inl
a b : ℕ
h : b ≤ a
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

Tactic:
rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))

Tactic:
rw [range_eq_Ico, map_eq_image]

Result:
case h.e'_2.h.e'_6
a b : ℕ
h : a ≤ b
⊢ Ico a b = image (⇑(addLeftEmbedding a)) (Ico 0 (b - a))

Proof state:
case inr
a b : ℕ
h : a ≤ b
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

Tactic:
convert addRothNumber_map_add_left _ a

Result:
case h.e'_2.h.e'_6
a b : ℕ
h : a ≤ b
⊢ Ico a b = map (addLeftEmbedding a) (range (b - a))

Proof state:
case h.e'_2.h.e'_5
a b : ℕ
h : a ≤ b
⊢ b = a + (b - a)

Tactic:
exact (add_tsub_cancel_of_le h).symm

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem restriction_zero : restriction (0 : R[X]) = 0

Proof state:
R : Type u
inst✝ : Ring R
⊢ restriction 0 = 0

Tactic:
simp only [restriction, Finset.sum_empty, support_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem sheafificationAdjunction_counit_app_val (P : Sheaf J D) :
    ((sheafificationAdjunction J D).counit.app P).val = sheafifyLift J (𝟙 P.val) P.cond

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).val =
    ((presheafToSheaf J D).map (𝟙 P.val) ≫ (sheafificationAdjunction J D).counit.app { val := P.val, cond := ⋯ }).val

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).val = sheafifyLift J (𝟙 P.val) ⋯

Tactic:
unfold sheafifyLift

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).val =
    (((sheafificationAdjunction J D).homEquiv P.val { val := P.val, cond := ⋯ }).symm (𝟙 P.val)).val

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).val =
    (((sheafificationAdjunction J D).homEquiv P.val { val := P.val, cond := ⋯ }).symm (𝟙 P.val)).val

Tactic:
rw [Adjunction.homEquiv_counit]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).val =
    ((presheafToSheaf J D).map (𝟙 P.val) ≫ (sheafificationAdjunction J D).counit.app { val := P.val, cond := ⋯ }).val
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem toMatrix_distrib_mul_action_toLinearMap (x : R) :
    LinearMap.toMatrix v₁ v₁ (DistribMulAction.toLinearMap R M₁ x) =
    Matrix.diagonal fun _ ↦ x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ (toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 => x

Tactic:
ext

Result:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
i✝ j✝ : n
⊢ (toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ j✝ = Matrix.diagonal (fun x_1 => x) i✝ j✝

Proof state:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
i✝ j✝ : n
⊢ (toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ j✝ = Matrix.diagonal (fun x_1 => x) i✝ j✝

Tactic:
rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul,
  Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
  Pi.single_apply]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_sup_right {S T : NonUnitalStarSubalgebra R A} : ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ T ≤ S ⊔ T
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem go_get_aux (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
    (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) :
    -- `hfoo` makes it possible to `generalize` below. With a concrete proof term this
    -- `generalize` would produce a type incorrect term as the proof term would talk about
    -- a `go` application instead of the fresh variable.
    ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
        (go aig lhs rhs curr hcurr cin s).vec.get idx (by omega)
          =
        (s.get idx hidx).cast hfoo

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig lhs rhs curr hcurr cin s).aig.decls.size),
    (go aig lhs rhs curr hcurr cin s).vec.get idx ⋯ = (s.get idx hidx).cast hfoo

Tactic:
generalize hgo : go aig lhs rhs curr hcurr cin s = res

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx : Nat
hidx : idx < curr
res : RefVecEntry α w
hgo : go aig lhs rhs curr hcurr cin s = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.vec.get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_rightUnitor_hom {X Y : C} (f : X ⟶ Y) (g : X ⟶ 𝟙_ C) :
    lift f g ≫ (ρ_ Y).hom = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g ≫ (ρ_ Y).hom = f

Tactic:
rw [← Iso.eq_comp_inv]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g = f ≫ (ρ_ Y).inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g = f ≫ (ρ_ Y).inv

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem getElem_cyclicPermutations (l : List α) (n : Nat) (h : n < length (cyclicPermutations l)) :
    (cyclicPermutations l)[n] = l.rotate n

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.cyclicPermutations.length
⊢ l.cyclicPermutations[n] = l.rotate n

Tactic:
cases l with
| nil => simp
| cons a l =>
  simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
    getElem_inits]
  rw [rotate_eq_drop_append_take (by simpa using h.le)]

Result:
no goals

Proof state:
case nil
α : Type u
n : ℕ
h : n < [].cyclicPermutations.length
⊢ [].cyclicPermutations[n] = [].rotate n

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ (a :: l).cyclicPermutations[n] = (a :: l).rotate n

Tactic:
simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
  getElem_inits]

Result:
case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n

Proof state:
case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n

Tactic:
rw [rotate_eq_drop_append_take (by simpa using h.le)]

Result:
no goals

Proof state:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
simpa using h.le

Result:
no goals