harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_listTransvecRow_last_col (i : Fin r ⊕ Unit) :
    (M * (listTransvecRow M).prod) i (inr unit) = M i (inr unit)

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (listTransvecRow M).length = r

Tactic:
simp [listTransvecRow]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

Tactic:
rw [← List.take_length (listTransvecRow M), A]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
simpa using mul_listTransvecRow_last_col_take M i le_rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset_Ioo (h : x < y) : openSegment 𝕜 x y ⊆ Ioo x y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • x < a • x + b • y

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < a • y + b • y

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y

Tactic:
calc
  x = a • x + b • x := (Convex.combo_self hab _).symm
  _ < a • x + b • y := by gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
⊢ openSegment 𝕜 x y ⊆ Ioo x y

Tactic:
rintro z ⟨a, b, ha, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y

Proof state:
case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y

Tactic:
calc
  a • x + b • y < a • y + b • y := by gcongr
  _ = y := Convex.combo_self hab _

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y

Tactic:
constructor

Result:
case intro.intro.intro.intro.intro.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y

case intro.intro.intro.intro.intro.right
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    getD (insertMany m l) k' fallback = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v fallback : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ getD (insertMany m l) k' fallback = v

Tactic:
simp_to_raw using Raw₀.Const.getD_insertMany_list_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Subarray.lean
theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size

Proof state:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ stop ≤ array.size

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
s : Subarray α
⊢ s.size ≤ s.array.size

Tactic:
let {array, start, stop, start_le_stop, stop_le_array_size} := s

Result:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size }.size ≤
    { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
          stop_le_array_size := stop_le_array_size }.array.size

Proof state:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ stop - start ≤ array.size

Tactic:
apply Nat.le_trans (Nat.sub_le stop start)

Result:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ stop ≤ array.size

Proof state:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size }.size ≤
    { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
          stop_le_array_size := stop_le_array_size }.array.size

Tactic:
simp [size]

Result:
α : Type u_1
s : Subarray α
array : Array α
start stop : Nat
start_le_stop : start ≤ stop
stop_le_array_size : stop ≤ array.size
⊢ stop - start ≤ array.size
-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_accumulate (m : AddContent C) (hC : IsSetRing C)
    {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s)) (hsC : ∀ i, s i ∈ C) (n : ℕ) :
      m (Set.Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)

Proof state:
case succ
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Disjoint (Accumulate s n) (s (n + 1))

Tactic:
exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)

Result:
no goals

Proof state:
case zero
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
⊢ m (Accumulate s 0) = ∑ i ∈ Finset.range (0 + 1), m (s i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Accumulate s n ∈ C

Tactic:
exact hC.accumulate_mem hsC n

Result:
no goals

Proof state:
case succ
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ m (Accumulate s (n + 1)) = ∑ i ∈ Finset.range (n + 1 + 1), m (s i)

Tactic:
rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]

Result:
case succ
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Disjoint (Accumulate s n) (s (n + 1))

α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ Accumulate s n ∈ C
-- Mathlib/Data/Finset/Piecewise.lean
@[simp]
lemma piecewise_erase_univ [DecidableEq ι] (i : ι) (f g : ∀ i, π i) :
    (Finset.univ.erase i).piecewise f g = Function.update f i (g i)

Proof state:
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ (univ.erase i).piecewise f g = update f i (g i)

Tactic:
rw [← compl_singleton, piecewise_compl, piecewise_singleton]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_transpose (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) : (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : l ⊕ m
j : n ⊕ o
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : l ⊕ m
j : n ⊕ o
⊢ (fromBlocks A B C D)ᵀ i j = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ i j
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive (attr := simp)]
lemma lipschitzOnWith_inv_iff : LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
s : Set α
⊢ LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

Tactic:
simp [LipschitzOnWith]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Sum.lean
theorem colorable_sum {n : ℕ} : (G ⊕g H).Colorable n ↔ G.Colorable n ∧ H.Colorable n :=
  ⟨fun cGH => ⟨cGH.of_sum_left, cGH.of_sum_right⟩,
    fun ⟨cG, cH⟩ => by rw [← n.max_self]; exact cG.sum_max cH⟩

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable (n ⊔ n)

Tactic:
exact cG.sum_max cH

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable n

Tactic:
rw [← n.max_self]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable (n ⊔ n)
-- Mathlib/Topology/Order/PartialSups.lean
protected lemma partialSups_apply (hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))) :
    Tendsto (fun a ↦ partialSups (f · a) n) l (𝓝 (partialSups g n))

Proof state:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto (fun a => (partialSups fun x => f x a) n) l (𝓝 ((partialSups g) n))

Tactic:
simpa only [← Pi.partialSups_apply] using Tendsto.partialSups hf

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalarsSum_zero : ofScalarsSum c (0 : E) = c 0 • 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
⊢ ofScalarsSum c 0 = c 0 • 1

Tactic:
simp [ofScalarsSum_eq_tsum, ← ofScalars_apply_eq, ofScalars_apply_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem gluedCoverT'_snd_fst (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ pullback.snd _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)

Tactic:
delta gluedCoverT'

Result:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)
-- Mathlib/Data/Finsupp/Single.lean
theorem card_support_le_one [Nonempty α] {f : α →₀ M} :
    #f.support ≤ 1 ↔ ∃ a, f = single a (f a)

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ a, f = single a (f a)

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem inv_mem_iff {c d : C} (f : c ⟶ d) :
    Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
apply S.inv

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
h : Groupoid.inv f ∈ S.arrows d c
⊢ f ∈ S.arrows c d

Tactic:
simpa only [inv_eq_inv, IsIso.inv_inv] using S.inv h

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d

Tactic:
intro h

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
h : Groupoid.inv f ∈ S.arrows d c
⊢ f ∈ S.arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d

case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c
-- Mathlib/Data/List/Basic.lean
lemma filter_attach (l : List α) (p : α → Bool) :
    (l.attach.filter fun x => p x : List {x // x ∈ l}) =
      (l.filter p).attach.map (Subtype.map id fun _ => mem_of_mem_filter) :=
  map_injective_iff.2 Subtype.coe_injective <| by
    simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]

Proof state:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a => ↑a) (filter (fun x => p ↑x) l.attach) = map (fun a => ↑a) (map (Subtype.map id ⋯) (filter p l).attach)

Tactic:
simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
  ← filter_map, attach_map_subtype_val]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/PartialAdjoint.lean
lemma partialLeftAdjointHomEquiv_map_comp {X X' : F.PartialLeftAdjointSource} {Y : D}
    (f : X ⟶ X') (g : F.partialLeftAdjointObj X' ⟶ Y) :
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) =
      by exact f ≫ F.partialLeftAdjointHomEquiv g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ X.obj ⟶ F.obj Y

Tactic:
exact f ≫ F.partialLeftAdjointHomEquiv g

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) = f ≫ F.partialLeftAdjointHomEquiv g

Tactic:
rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc,
  ← partialLeftAdjointHomEquiv_comp, id_comp]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem intCast_im (n : ℤ) : im (n : K) = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ im ↑n = 0

Tactic:
rw [← ofReal_intCast, ofReal_im]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Sheaf.lean
lemma unitHomEquiv_symm_comp {M N : SheafOfModules.{u} R} (s : M.sections) (p : M ⟶ N) :
    M.unitHomEquiv.symm s ≫ p = N.unitHomEquiv.symm (sectionsMap p s) :=
  N.unitHomEquiv.injective (by simp [unitHomEquiv_comp_apply])

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)
M N : SheafOfModules R
s : M.sections
p : M ⟶ N
⊢ N.unitHomEquiv (M.unitHomEquiv.symm s ≫ p) = N.unitHomEquiv (N.unitHomEquiv.symm (sectionsMap p s))

Tactic:
simp [unitHomEquiv_comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Unramified/Locus.lean
lemma isOpen_unramifiedLocus [EssFiniteType R A] : IsOpen (unramifiedLocus R A)

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ IsOpen (unramifiedLocus R A)

Tactic:
rw [unramifiedLocus_eq_compl_support, Module.support_eq_zeroLocus]

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ IsOpen (PrimeSpectrum.zeroLocus ↑(Module.annihilator A (Ω[A⁄R])))ᶜ

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ IsOpen (PrimeSpectrum.zeroLocus ↑(Module.annihilator A (Ω[A⁄R])))ᶜ

Tactic:
exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x

Proof state:
w : Nat
x y : BitVec w
⊢ x.toInt ≤ y.toInt ↔ ¬y.toInt < x.toInt

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.sle y = !y.slt x

Tactic:
simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]

Result:
w : Nat
x y : BitVec w
⊢ x.toInt ≤ y.toInt ↔ ¬y.toInt < x.toInt
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem _root_.Nat.card_divisors {n : ℕ} (hn : n ≠ 0) :
    #n.divisors = n.primeFactors.prod (n.factorization · + 1)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Tactic:
rw [← sigma_zero_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]

Result:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => (σ 0) (p ^ k)) = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun p k => (σ 0) (p ^ k)) = ∏ x ∈ n.primeFactors, (n.factorization x + 1)

Tactic:
exact Finset.prod_congr n.support_factorization fun _ h =>
  sigma_zero_apply_prime_pow <| Nat.prime_of_mem_primeFactors h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False

Proof state:
a b : Prop
h : (a ∨ b) = False
⊢ b = False

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem length_replaceF : length (replaceF f l) = length l

Proof state:
α✝ : Type u_1
f : α✝ → Option α✝
l : List α✝
⊢ (replaceF f l).length = l.length

Tactic:
induction l <;> simp [replaceF]

Result:
case cons
α✝ : Type u_1
f : α✝ → Option α✝
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : (replaceF f tail✝).length = tail✝.length
⊢ (match f head✝ with
      | none => head✝ :: replaceF f tail✝
      | some a => a :: tail✝).length =
    tail✝.length + 1

Proof state:
case cons
α✝ : Type u_1
f : α✝ → Option α✝
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : (replaceF f tail✝).length = tail✝.length
⊢ (match f head✝ with
      | none => head✝ :: replaceF f tail✝
      | some a => a :: tail✝).length =
    tail✝.length + 1

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousAt_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {x : α × β} :
    ContinuousAt f x ↔ ContinuousAt (f ⟨·, x.2⟩) x.1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x_1, x.2)) x.1

Tactic:
simp_rw [← continuousWithinAt_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) univ x.1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
x : α × β
⊢ ContinuousWithinAt f univ x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) univ x.1

Tactic:
exact continuousWithinAt_prod_of_discrete_right

Result:
no goals