harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Dual.lean
theorem LinearMap.toMatrix_transpose (u : V₁ →ₗ[K] V₂) :
    LinearMap.toMatrix B₂.dualBasis B₁.dualBasis (Module.Dual.transpose (R := K) u) =
      (LinearMap.toMatrix B₁ B₂ u)ᵀ

Proof state:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
⊢ (toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) = ((toMatrix B₁ B₂) u)ᵀ

Tactic:
ext i j

Result:
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
i : ι₁
j : ι₂
⊢ (toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) i j = ((toMatrix B₁ B₂) u)ᵀ i j

Proof state:
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
i : ι₁
j : ι₂
⊢ (toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) i j = ((toMatrix B₁ B₂) u)ᵀ i j

Tactic:
simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr,
  B₂.dualBasis_apply, Matrix.transpose_apply, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem lf_zero_iff {G : PGame} [G.Impartial] : G ⧏ 0 ↔ 0 ⧏ G

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G ⧏ 0 ↔ 0 ⧏ G

Tactic:
rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.getElem_eq_getLsbD (a : BitVec w) (i : Nat) (h : i < w) :
    a[i]'h = a.getLsbD i

Proof state:
w : Nat
a : BitVec w
i : Nat
h : i < w
⊢ a[i] = a.getLsbD i

Tactic:
simp [BitVec.getLsbD_eq_getElem?_getD, BitVec.getElem?_eq, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem HasDerivAt.div (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) (hx : d x ≠ 0) :
    HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) univ x

Tactic:
exact hc.div hd hx

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
⊢ HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) univ x
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma one_sub_inv_le_log_of_pos (hx : 0 < x) : 1 - x⁻¹ ≤ log x

Proof state:
x : ℝ
hx : 0 < x
⊢ 1 - x⁻¹ ≤ log x

Tactic:
simpa [add_comm] using log_le_sub_one_of_pos (inv_pos.2 hx)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.ball_zero_eq_Ico' (c : ℝ≥0) :
    Metric.ball (0 : ℝ≥0) c.toReal = Set.Ico 0 c

Proof state:
case h
c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c

Tactic:
simp

Result:
no goals

Proof state:
c : ℝ≥0
⊢ ball 0 ↑c = Ico 0 c

Tactic:
ext x

Result:
case h
c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c
-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma hom1_isIntegral (fne : f ≠ 0) (fi : f ∈ I): (hom1 f I).IsIntegral

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
u : IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff
⊢ (NoetherNormalization.hom1 f I).IsIntegral

Tactic:
exact (monic_of_isUnit_leadingCoeff_inv_smul u).quotient_isIntegral <|
  Submodule.smul_of_tower_mem _ u.unit⁻¹.val <| mem_map_of_mem _ <| mem_map_of_mem _ fi

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
⊢ (NoetherNormalization.hom1 f I).IsIntegral

Tactic:
obtain u := T_leadingcoeff_isUnit f fne

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
u : IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff
⊢ (NoetherNormalization.hom1 f I).IsIntegral
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem ofNat'_self {n : Nat} [NeZero n] : Fin.ofNat' n n = 0

Proof state:
case h
n : Nat
inst✝ : NeZero n
⊢ 0 = ↑0

Tactic:
congr

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
⊢ Fin.ofNat' n n = 0

Tactic:
ext

Result:
case h
n : Nat
inst✝ : NeZero n
⊢ ↑(Fin.ofNat' n n) = ↑0

Proof state:
case h
n : Nat
inst✝ : NeZero n
⊢ ↑(Fin.ofNat' n n) = ↑0

Tactic:
simp

Result:
case h
n : Nat
inst✝ : NeZero n
⊢ 0 = ↑0
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem ball_prod_same [PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) :
    ball x r ×ˢ ball y r = ball (x, y) r :=
  ext fun z => by simp [Prod.edist_eq]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r

Tactic:
simp [Prod.edist_eq]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_partition (R : Setoid α) [DecidableRel R.r] :
    ∏ x ∈ s, f x = ∏ xbar ∈ s.image (Quotient.mk _), ∏ y ∈ s with ⟦y⟧ = xbar, f y

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
⊢ ∏ x ∈ s, f x = ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ filter (fun y => ⟦y⟧ = xbar) s, f y

Tactic:
refine (Finset.prod_image' f fun x _hx => ?_).symm

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
x : α
_hx : x ∈ s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = ∏ j ∈ filter (fun j => ⟦j⟧ = ⟦x⟧) s, f j

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
x : α
_hx : x ∈ s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = ∏ j ∈ filter (fun j => ⟦j⟧ = ⟦x⟧) s, f j

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_eq_nil_iff {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ filter p l = [] ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

Tactic:
simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem containsThenInsertIfNew_fst {k : α} {v : β k} :
    (m.containsThenInsertIfNew k v).1 = m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (m.containsThenInsertIfNew k v).fst = m.contains k

Tactic:
rw [containsThenInsertIfNew_eq_containsₘ, contains_eq_containsₘ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getD_val [BEq α] [Hashable α] {m : Raw₀ α (fun _ => β)} {a : α} {fallback : β} :
    Raw.Const.getD m.val a fallback = Raw₀.Const.getD m a fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
a : α
fallback : β
⊢ Raw.Const.getD m.val a fallback = Raw₀.Const.getD m a fallback

Tactic:
simp [Raw.Const.getD, m.2]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
    diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i)

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.char_nsmul_eq_zero (x : G) : n • x = 0

Proof state:
n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
x : G
⊢ n • x = 0

Tactic:
simp [← Nat.cast_smul_eq_nsmul (ZMod n)]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ}
    (h : n.minFac ^ n.factorization n.minFac = n) (hn : n ≠ 1) : IsPrimePow n

Proof state:
case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < n.factorization n.minFac

Tactic:
simp [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.support_factorization, hn',
  Nat.minFac_prime hn, Nat.minFac_dvd]

Result:
no goals

Proof state:
case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n

Tactic:
refine ⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩

Result:
case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ 0 < n.factorization n.minFac

Proof state:
case inl
h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0

Tactic:
simp_all

Result:
no goals

Proof state:
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
⊢ IsPrimePow n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn')

Result:
case inl
h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0

case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasDerivWithinAt.rpow_const (hf : HasDerivWithinAt f f' s x) (hx : f x ≠ 0 ∨ 1 ≤ p) :
    HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x

Proof state:
case h.e'_9
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'

Tactic:
ring

Result:
no goals

Proof state:
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x

Tactic:
convert (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1

Result:
case h.e'_9
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
-- Mathlib/Data/Set/Basic.lean
theorem inter_compl_nonempty_iff {s t : Set α} : (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t :=
  (not_subset.trans <| exists_congr fun x => by simp [mem_compl]).symm

Proof state:
α : Type u
s t : Set α
x : α
⊢ x ∈ s ∧ x ∉ t ↔ x ∈ s ∩ tᶜ

Tactic:
simp [mem_compl]

Result:
no goals
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
@[simp] lemma Topology.IsScott.ωscottContinuous_iff_continuous {α : Type*}
    [OmegaCompletePartialOrder α] [TopologicalSpace α]
    [Topology.IsScott α (Set.range fun c : Chain α => Set.range c)] {f : α → Prop} :
    ωScottContinuous f ↔ Continuous f

Proof state:
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c => range ⇑c)
f : α → Prop
⊢ ωScottContinuous f ↔ Continuous f

Tactic:
rw [ωScottContinuous, scottContinuous_iff_continuous (fun a b hab => by
  use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c => range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ (fun c => range ⇑c) (Chain.pair a b hab) = {a, b}

Tactic:
exact OmegaCompletePartialOrder.Chain.range_pair a b hab

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c => range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ {a, b} ∈ range fun c => range ⇑c

Tactic:
use Chain.pair a b hab

Result:
case h
α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c => range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ (fun c => range ⇑c) (Chain.pair a b hab) = {a, b}
-- Mathlib/MeasureTheory/Constructions/Polish/EmbeddingReal.lean
theorem exists_nat_measurableEquiv_range_coe_fin_of_finite [Finite α] :
    ∃ n : ℕ, Nonempty (α ≃ᵐ range ((↑) : Fin n → ℝ))

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))

Tactic:
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α

Result:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))

Proof state:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x => ↑↑x)

Tactic:
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x => ↑↑x))

Tactic:
refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩

Result:
case intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x => ↑↑x)
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma shift_distinguished_triangle (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT : T ∈ distinguishedTriangles C) (n : ℤ) :
      (Triangle.shiftFunctor _ n).obj T ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles C
n : ℤ
⊢ (Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ distinguishedTriangles C

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT

Result:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
n : ℤ
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ (Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ distinguishedTriangles C

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
n : ℤ
K L : CochainComplex C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ (Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ distinguishedTriangles C

Tactic:
exact ⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩

Result:
no goals
-- Mathlib/Topology/Bases.lean
@[simp] lemma isTopologicalBasis_empty : IsTopologicalBasis (∅ : Set (Set α)) ↔ IsEmpty α where
  mp h

Proof state:
α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis ∅
⊢ IsEmpty α

Tactic:
simpa using h.sUnion_eq.symm

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ t₁ ∈ ∅, ∀ t₂ ∈ ∅, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ∅, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ ∅ = univ

Tactic:
simp [Set.univ_eq_empty_iff.2]

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem cancel_left {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.dropUntil {u v w : V} {p : G.Walk v w} (hc : p.IsTrail)
    (h : u ∈ p.support) : (p.dropUntil u h).IsTrail :=
  IsTrail.of_append_right (p := p.takeUntil u h) (q := p.dropUntil u h)
    (by rwa [← take_spec _ h] at hc)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
hc : p.IsTrail
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).IsTrail

Tactic:
rwa [← take_spec _ h] at hc

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasStrictFDerivAt.abs (hf : HasStrictFDerivAt f f' x)
    (h₀ : f x ≠ 0) : HasStrictFDerivAt (fun x ↦ |f x|) ((SignType.sign (f x) : ℝ) • f') x

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ ↑(SignType.sign (f x)) • f' = (ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
y : E
⊢ (↑(SignType.sign (f x)) • f') y = ((ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f') y

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
y : E
⊢ (↑(SignType.sign (f x)) • f') y = ((ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f') y

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasStrictFDerivAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') x

Tactic:
convert (hasStrictDerivAt_abs h₀).hasStrictFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
⊢ ↑(SignType.sign (f x)) • f' = (ContinuousLinearMap.smulRight 1 ↑(SignType.sign (f x))).comp f'
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem symm_comp_toContinuousMap :
    (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ (↑f.symm).comp ↑f = ContinuousMap.id α

Tactic:
rw [← coe_trans, self_trans_symm, coe_refl]

Result:
no goals
-- Mathlib/Order/TransfiniteIteration.lean
lemma transfiniteIterate_limit (i₀ : I) (j : J) (hj : Order.IsSuccLimit j) :
    transfiniteIterate φ j i₀ =
      ⨆ (x : Set.Iio j), transfiniteIterate φ x.1 i₀

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ transfiniteIterate φ j i₀ = ⨆ x, transfiniteIterate φ (↑x) i₀

Tactic:
dsimp [transfiniteIterate]

Result:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    ⨆ x, SuccOrder.limitRecOn (↑x) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ (⨆ x, (fun x x_1 => SuccOrder.limitRecOn x (fun x x => id) (fun x x g => φ ∘ g) fun y x h => ⨆ x, h ↑x ⋯) ↑x ⋯) i₀ =
    ⨆ x, SuccOrder.limitRecOn (↑x) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀

Tactic:
simp only [iSup_apply]

Result:
no goals

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    ⨆ x, SuccOrder.limitRecOn (↑x) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀

Tactic:
rw [SuccOrder.limitRecOn_of_isSuccLimit _ _ _ hj]

Result:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ (⨆ x, (fun x x_1 => SuccOrder.limitRecOn x (fun x x => id) (fun x x g => φ ∘ g) fun y x h => ⨆ x, h ↑x ⋯) ↑x ⋯) i₀ =
    ⨆ x, SuccOrder.limitRecOn (↑x) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀
-- Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean
theorem effectiveEpi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) :
    EffectiveEpi f ↔ Function.Surjective f

Proof state:
X Y : LightProfinite
f : X ⟶ Y
⊢ EffectiveEpi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨effectiveEpiStruct f h⟩⟩⟩

Result:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Proof state:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Epi f

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [← epi_iff_surjective]

Result:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Epi f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isNe_iff_ne_eq {o : Ordering} : o.isNe ↔ o ≠ .eq

Proof state:
o : Ordering
⊢ o.isNe = true ↔ o ≠ eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem prod_eq_prod_coe [CommMonoid α] (m : Multiset α) : m.prod = ∏ x : m, (x : α)

Proof state:
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) Finset.univ.val

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x : m.ToType, x.fst

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.fst) Finset.univ.val
-- Mathlib/Logic/Basic.lean
theorem ite_or : ite (P ∨ Q) a b = ite P a (ite Q a b)

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblY_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.dblY P = W.dblU P

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblU P

Tactic:
rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Result:
no goals