harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ind₂ {X : C} (p : Subobject X → Subobject X → Prop)
    (h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [Mono f] [Mono g],
      p (Subobject.mk f) (Subobject.mk g))
    (P Q : Subobject X) : p P Q

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ ∀ (a₁ a₂ : MonoOver X), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)

Tactic:
intro a b

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ p P Q

Tactic:
apply Quotient.inductionOn₂'

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ ∀ (a₁ a₂ : MonoOver X), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
exact h a.arrow b.arrow

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_insert_zero : span R (insert (0 : M) s) = span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) ≤ span R s

Tactic:
rw [span_le, Set.insert_subset_iff]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ 0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ 0 ∈ ↑(span R s)

Tactic:
simp only [SetLike.mem_coe, Submodule.zero_mem]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) = span R s

Tactic:
refine le_antisymm ?_ (Submodule.span_mono (Set.subset_insert 0 s))

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R (insert 0 s) ≤ span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ 0 ∈ ↑(span R s) ∧ s ⊆ ↑(span R s)

Tactic:
exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem sqrt_eq_rpow (x : ℝ) : √x = x ^ (1 / (2 : ℝ))

Proof state:
case inl
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)

Tactic:
rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg h _), mul_self_sqrt h, ← sq,
  ← rpow_natCast, ← rpow_mul h]

Result:
case inl
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)

Proof state:
case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)

Tactic:
rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

Result:
no goals

Proof state:
case inl
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2

Tactic:
ring

Result:
no goals

Proof state:
case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)

Tactic:
have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring

Result:
case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)

Proof state:
x : ℝ
⊢ √x = x ^ (1 / 2)

Tactic:
obtain h | h := le_or_lt 0 x

Result:
case inl
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)

case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_zero : num (0 : RatFunc K) = 0

Proof state:
K : Type u
inst✝ : Field K
⊢ num 0 = 0

Tactic:
convert num_div' (0 : K[X]) one_ne_zero <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMinOn.hasFDerivWithinAt_nonneg (h : IsLocalMinOn f s a)
    (hf : HasFDerivWithinAt f f' s a) (hy : y ∈ posTangentConeAt s a) : 0 ≤ f' y

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ f' y

Tactic:
simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0

Proof state:
n p : ℕ
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_restrict_subset (M : Matroid α) (hYX : Y ⊆ X) : (M ↾ X).cRk Y = M.cRk Y

Proof state:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X

Tactic:
exact fun I h ↦ h.subset.trans hYX

Result:
no goals

Proof state:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
have aux : ∀ ⦃I⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y := by
  simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
  exact fun I h ↦ h.subset.trans hYX

Result:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y

Proof state:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
simp_rw [le_antisymm_iff, cRk_le_iff]

Result:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (∀ ⦃I : Set α⦄, (M ↾ X).IsBasis' I Y → #↑I ≤ M.cRk Y) ∧ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → #↑I ≤ (M ↾ X).cRk Y

Proof state:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
aux : ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y
⊢ (∀ ⦃I : Set α⦄, (M ↾ X).IsBasis' I Y → #↑I ≤ M.cRk Y) ∧ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → #↑I ≤ (M ↾ X).cRk Y

Tactic:
exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩

Result:
no goals

Proof state:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y

Tactic:
simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]

Result:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one {p n : ℕ} (hpp : p.Prime) (hp : p ∣ n)
    (hs : IsSquare (-1 : ZMod n)) : p % 4 ≠ 3

Proof state:
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1
⊢ -1 = -1 ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3

Tactic:
exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Result:
no goals

Proof state:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3

Tactic:
rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h

Result:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3

Proof state:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3

Tactic:
haveI : Fact p.Prime := ⟨hpp⟩

Result:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3

Proof state:
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
⊢ p % 4 ≠ 3

Tactic:
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd hp hs

Result:
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem of_mul_of (x y : α) : of x * of y = of (x * y)

Proof state:
α : Type u
inst✝ : Mul α
x y : α
⊢ of x * of y = of (x * y)

Tactic:
rw [mul_def, lift.of, lift.of]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_indep_iff_exists (hI : I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M✶.Indep I ↔ ∃ B, M.IsBase B ∧ Disjoint I B

Tactic:
rw [dual_indep_iff_exists', and_iff_right hI]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomialZ (P : Fin 3 → R) : eval P W'.polynomialZ =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialZ =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)

Tactic:
rw [polynomialZ_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P)
      (C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 -
        (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)) =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P)
      (C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 -
        (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)) =
    W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
      (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5)

Tactic:
eval_simp

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_add' : Odd (m + n) ↔ (Odd n ↔ Even m)

Proof state:
m n : ℕ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
rw [add_comm, odd_add]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_num_den' (num den nz) : ∃ d : Nat, d ≠ 0 ∧
    num = (normalize num den nz).num * d ∧ den = (normalize num den nz).den * d

Proof state:
num : Int
den : Nat
nz : den ≠ 0
⊢ num = (normalize num den nz).num * ↑(num.natAbs.gcd den) ∧ den = (normalize num den nz).den * num.natAbs.gcd den

Tactic:
simp [normalize_eq, Int.ediv_mul_cancel (Int.ofNat_dvd_left.2 <| Nat.gcd_dvd_left ..),
  Nat.div_mul_cancel (Nat.gcd_dvd_right ..)]

Result:
no goals

Proof state:
num : Int
den : Nat
nz : den ≠ 0
⊢ ∃ d, d ≠ 0 ∧ num = (normalize num den nz).num * ↑d ∧ den = (normalize num den nz).den * d

Tactic:
refine ⟨num.natAbs.gcd den, Nat.gcd_ne_zero_right nz, ?_⟩

Result:
num : Int
den : Nat
nz : den ≠ 0
⊢ num = (normalize num den nz).num * ↑(num.natAbs.gcd den) ∧ den = (normalize num den nz).den * num.natAbs.gcd den
-- Mathlib/Topology/Path.lean
theorem refl_symm {a : X} : (Path.refl a).symm = Path.refl a

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ (refl a).symm x✝ = (refl a) x✝

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ (refl a).symm = refl a

Tactic:
ext

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ (refl a).symm x✝ = (refl a) x✝
-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem card_antidiagonal (s : Multiset α) : card (antidiagonal s) = 2 ^ card s

Proof state:
α : Type u_1
s : Multiset α
⊢ s.antidiagonal.card = 2 ^ s.card

Tactic:
have := card_powerset s

Result:
α : Type u_1
s : Multiset α
this : s.powerset.card = 2 ^ s.card
⊢ s.antidiagonal.card = 2 ^ s.card

Proof state:
α : Type u_1
s : Multiset α
this : s.powerset.card = 2 ^ s.card
⊢ s.antidiagonal.card = 2 ^ s.card

Tactic:
rwa [← antidiagonal_map_fst, card_map] at this

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
    dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]

Result:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ ‖p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)‖ ≤ ‖p₁ -ᵥ p₃‖ + ‖p₂ -ᵥ p₄‖

Tactic:
exact norm_sub_le _ _

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem pow : Nat.Primrec (unpaired (· ^ ·)) :=
  (prec (const 1) (mul.comp (pair (right.comp right) left))).of_eq fun p => by
    simp; induction p.unpair.2 <;> simp [*, Nat.pow_succ]

Proof state:
p : ℕ
⊢ Nat.rec 1 (fun y IH => IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2

Tactic:
induction p.unpair.2 <;> simp [*, Nat.pow_succ]

Result:
no goals

Proof state:
p : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec 1
          (fun y IH =>
            unpaired (fun x1 x2 => x1 * x2)
              (Nat.pair (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2 (unpair (Nat.pair z (Nat.pair y IH))).1))
          n)
      p =
    unpaired (fun x1 x2 => x1 ^ x2) p

Tactic:
simp

Result:
p : ℕ
⊢ Nat.rec 1 (fun y IH => IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_add_const (l : Array α) (a b : Nat) :
    l.foldr (fun _ x => x + a) b = b + a * l.size

Proof state:
α : Type u_1
l : Array α
a b : Nat
⊢ Array.foldr (fun x x => x + a) b l = b + a * l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ Array.foldr (fun x x => x + a) b { toList := l } = b + a * { toList := l }.size

Proof state:
case mk
α : Type u_1
a b : Nat
l : List α
⊢ Array.foldr (fun x x => x + a) b { toList := l } = b + a * { toList := l }.size

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean
lemma triangleOfSES_distinguished :
    triangleOfSES hS ∈ distTriang (DerivedCategory C)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ ∃ X Y f, Nonempty (triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Tactic:
exact ⟨_, _, S.f, ⟨triangleOfSESIso hS⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ triangleOfSES hS ∈ distinguishedTriangles

Tactic:
rw [mem_distTriang_iff]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ ∃ X Y f, Nonempty (triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))
-- Mathlib/GroupTheory/HNNExtension.lean
theorem t_smul_eq_unitsSMul (w : NormalWord d) :
    (t : HNNExtension G A B φ) • w = unitsSMul φ 1 w

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ t • w = unitsSMul φ 1 w

Tactic:
simp [instHSMul, SMul.smul, MulAction.toEndHom]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem map_sub : X (f - f') = X f - X f'

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (f - f') = X f - X f'

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_sub_zpow_of_undef {n : ℤ} {c w : ℂ} {R : ℝ} (hn : n < 0)
    (hw : w ∈ sphere c |R|) : (∮ z in C(c, R), (z - w) ^ n) = 0

Proof state:
case inl
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c |0|
⊢ (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) = 0

Tactic:
apply integral_radius_zero

Result:
no goals

Proof state:
case inr.hf
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R

Tactic:
simpa [circleIntegrable_sub_zpow_iff, *, not_or]

Result:
no goals

Proof state:
case inr
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0

Tactic:
apply integral_undef

Result:
case inr.hf
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R

Proof state:
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0

Tactic:
rcases eq_or_ne R 0 with (rfl | h0)

Result:
case inl
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c |0|
⊢ (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) = 0

case inr
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
h0 : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_nat_atTop_iff {f : ℕ → E''} {g : ℕ → F''} (h : ∀ x, g x = 0 → f x = 0) :
    f =O[atTop] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖

Proof state:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ (x : ℕ), g x = 0 → f x = 0
⊢ f =O[atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem apply_diag_ne [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i : V) :
    ¬A i i = 1

Proof state:
V : Type u_1
α : Type u_2
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h : A.IsAdjMatrix
i : V
⊢ ¬A i i = 1

Tactic:
simp [h.apply_diag i]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma add_cons (v : Fin n.succ → α) (y : α) (w : Fin n → α) :
    v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i

Tactic:
refine i.cases ?_ ?_ <;> simp [vecHead, vecTail]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
-- Mathlib/Data/Set/Basic.lean
theorem inclusion_inclusion (hst : s ⊆ t) (htu : t ⊆ u) (x : s) :
    inclusion htu (inclusion hst x) = inclusion (hst.trans htu) x

Proof state:
case mk
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion htu (inclusion hst ⟨val✝, property✝⟩) = inclusion ⋯ ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
x : ↑s
⊢ inclusion htu (inclusion hst x) = inclusion ⋯ x

Tactic:
cases x

Result:
case mk
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion htu (inclusion hst ⟨val✝, property✝⟩) = inclusion ⋯ ⟨val✝, property✝⟩
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive le_sum_nonempty_of_subadditive]
lemma le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)
    (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod :=
  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) s
    hs_nonempty (by simp)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ a ∈ s, (fun x => True) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → (fun x => True) (a * b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → f (a * b) ≤ f a * f b

Tactic:
simp [h_mul]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem coe_product (l₁ : List α) (l₂ : List β) :
    (l₁ : Multiset α) ×ˢ (l₂ : Multiset β) = (l₁ ×ˢ l₂)

Proof state:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a => map (Prod.mk a) ↑l₂) = (↑l₁).bind fun a => ↑(List.map (Prod.mk a) l₂)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁).product ↑l₂ = ↑(l₁.product l₂)

Tactic:
rw [product, List.product, ← coe_bind]

Result:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ((↑l₁).bind fun a => map (Prod.mk a) ↑l₂) = (↑l₁).bind fun a => ↑(List.map (Prod.mk a) l₂)

Proof state:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)

Tactic:
dsimp only [SProd.sprod]

Result:
α : Type u_1
β : Type v
l₁ : List α
l₂ : List β
⊢ (↑l₁).product ↑l₂ = ↑(l₁.product l₂)
-- Mathlib/Topology/Separation/Basic.lean
theorem isOpen_singleton_of_finite_mem_nhds [T1Space X] (x : X)
    {s : Set X} (hs : s ∈ 𝓝 x) (hsf : s.Finite) : IsOpen ({x} : Set X)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen {x}

Tactic:
have D : {x} ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen {x}

Tactic:
have A : {x} ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
⊢ IsOpen {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
⊢ IsOpen {x}

Tactic:
have B : IsClosed (s \ {x}) := (hsf.subset diff_subset).isClosed

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
⊢ IsOpen {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ {x} ⊆ s

Tactic:
simp only [singleton_subset_iff, mem_of_mem_nhds hs]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen {x}

Tactic:
rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x

Tactic:
simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
⊢ IsOpen {x}

Tactic:
have C : (s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen {x}