harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem continuousAt_tan {x : ℝ} : ContinuousAt tan x ↔ cos x ≠ 0

Proof state:
x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Result:
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Proof state:
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _
  (hc.norm.tendsto.mono_left inf_le_left)

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
lemma map_subtype_mem_of_mem_invtSubmodule {p : Submodule R M} (hp : p ∈ f.invtSubmodule)
    {q : Submodule R p} (hq : q ∈ invtSubmodule (LinearMap.restrict f hp)) :
    Submodule.map p.subtype q ∈ f.invtSubmodule

Proof state:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
specialize hq hx'

Result:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
hq : ⟨x, hx⟩ ∈ Submodule.comap (LinearMap.restrict f hp) q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Proof state:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
simpa [hq] using hp hx

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
⊢ Submodule.map p.subtype q ∈ f.invtSubmodule

Tactic:
rintro - ⟨⟨x, hx⟩, hx', rfl⟩

Result:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Proof state:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
hq : ⟨x, hx⟩ ∈ Submodule.comap (LinearMap.restrict f hp) q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
rw [Submodule.mem_comap, LinearMap.restrict_apply] at hq

Result:
case intro.mk.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : ⟨x, hx⟩ ∈ ↑q
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma map_op_pow (s : Finset α) :
    ∀ n : ℕ, (s ^ n).map opEquiv.toEmbedding = s.map opEquiv.toEmbedding ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', map_op_mul, map_op_pow]

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ map opEquiv.toEmbedding (s ^ 0) = map opEquiv.toEmbedding s ^ 0

Tactic:
simp [singleton_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ map opEquiv.toEmbedding (s ^ (n + 1)) = map opEquiv.toEmbedding s ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ', map_op_mul, map_op_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
    l[i]?.getD d = if p : i < l.length then l[i]'p else d

Proof state:
α : Type u_1
l : List α
i : Nat
d : α
h : ¬i < l.length
p : i ≥ l.length
⊢ l[i]?.getD d = if p : i < l.length then l[i] else d

Tactic:
simp [getElem?_eq_none p, h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
d : α
h : i < l.length
⊢ l[i]?.getD d = if p : i < l.length then l[i] else d

Tactic:
simp [h, getElem?_def]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
d : α
h : ¬i < l.length
⊢ l[i]?.getD d = if p : i < l.length then l[i] else d

Tactic:
have p : i ≥ l.length := Nat.le_of_not_gt h

Result:
α : Type u_1
l : List α
i : Nat
d : α
h : ¬i < l.length
p : i ≥ l.length
⊢ l[i]?.getD d = if p : i < l.length then l[i] else d

Proof state:
α : Type u_1
l : List α
i : Nat
d : α
⊢ l[i]?.getD d = if p : i < l.length then l[i] else d

Tactic:
if h : i < l.length then
  simp [h, getElem?_def]
else
  have p : i ≥ l.length := Nat.le_of_not_gt h
  simp [getElem?_eq_none p, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.isoLimitCone_inv_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
    (limit.isoLimitCone t).inv ≫ limit.π F j = t.cone.π.app j

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ lift F t.cone ≫ π F j = t.cone.π.app j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = t.cone.π.app j

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ lift F t.cone ≫ π F j = t.cone.π.app j
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isLittleO_deriv_one_add_smoothingFn :
    deriv (fun x => 1 + ε x) =o[atTop] fun (x : ℝ) => x⁻¹ := calc
  deriv (fun x => 1 + ε x) =ᶠ[atTop] fun z => deriv ε z

Proof state:
⊢ (deriv fun x => 1 + ε x) =ᶠ[atTop] fun z => deriv ε z

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 + ε x) x = deriv ε x

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 + ε x) x = deriv ε x

Tactic:
rw [deriv_add] <;> aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1

Proof state:
n : Nat
⊢ -[n+1] = -↑n - 1

Tactic:
rw [Int.sub_eq_add_neg, ← Int.neg_add]

Result:
n : Nat
⊢ -[n+1] = -(↑n + 1)

Proof state:
n : Nat
⊢ -[n+1] = -(↑n + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem desc_op_comp_opCoproductIsoProduct'_hom {c : Cofan Z} {f : Fan (op <| Z ·)}
    (hc : IsColimit c) (hf : IsLimit f) (c' : Cofan Z) :
    (hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
⊢ (hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op

Tactic:
refine (Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c.ι.app { as := j } ≫ (hc.desc c').op.unop).op =
    (c.ι.app { as := j } ≫ (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv).unop).op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op =
    hf.lift (Fan.mk (op c'.pt) fun a => (c'.inj a).op) ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.ι.app { as := j }).op

Tactic:
erw [opCoproductIsoProduct'_inv_comp_inj, IsLimit.fac]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op = (Fan.mk (op c'.pt) fun a => (c'.inj a).op).π.app { as := j }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op = (Fan.mk (op c'.pt) fun a => (c'.inj a).op).π.app { as := j }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c.ι.app { as := j } ≫ (hc.desc c').op.unop).op =
    (c.ι.app { as := j } ≫ (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv).unop).op

Tactic:
simp only [unop_op, Discrete.functor_obj, const_obj_obj, Quiver.Hom.unop_op, IsColimit.fac,
  Cofan.op, unop_comp, op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x => op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op =
    hf.lift (Fan.mk (op c'.pt) fun a => (c'.inj a).op) ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.ι.app { as := j }).op
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) :
    δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j.succ))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i))

Proof state:
case h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j.succ))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_le H

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem dvd_lcm_left (x y : R) : x ∣ lcm x y :=
  by_cases
    (fun hxy : gcd x y = 0 => by
      rw [lcm, hxy, div_zero]
      exact dvd_zero _)
    fun hxy =>
    let ⟨z, hz⟩ := (gcd_dvd x y).2
    ⟨z, Eq.symm <| eq_div_of_mul_eq_left hxy <| by rw [mul_right_comm, mul_assoc, ← hz]⟩

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * z * gcd x y = x * y

Tactic:
rw [mul_right_comm, mul_assoc, ← hz]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem sup_toSubalgebra_of_isAlgebraic_right [Algebra.IsAlgebraic K E2] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin ↥E1 ↑E2).toSubalgebra = Algebra.adjoin ↥E1 ↑E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
apply_fun Subalgebra.restrictScalars K at this

Result:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this :
  Subalgebra.restrictScalars K (adjoin ↥E1 ↑E2).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
exact this

Result:
no goals

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_algebraic_toSubalgebra fun x h ↦
  IsAlgebraic.tower_top E1 (isAlgebraic_iff.1
    (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))

Result:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin ↥E1 ↑E2).toSubalgebra = Algebra.adjoin ↥E1 ↑E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this :
  Subalgebra.restrictScalars K (adjoin ↥E1 ↑E2).toSubalgebra = Subalgebra.restrictScalars K (Algebra.adjoin ↥E1 ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin,
  Algebra.restrictScalars_adjoin] at this

Result:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E1 E2 : IntermediateField K L
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem OrthonormalBasis.measurePreserving_measurableEquiv (b : OrthonormalBasis ι ℝ F) :
    MeasurePreserving b.measurableEquiv volume volume

Proof state:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ MeasurePreserving (⇑b.measurableEquiv) volume volume

Tactic:
convert (b.measurableEquiv.symm.measurable.measurePreserving _).symm

Result:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) volume

Proof state:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) volume

Tactic:
rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]

Result:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) (EuclideanSpace.basisFun ι ℝ).toBasis.addHaar

Proof state:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = ((EuclideanSpace.basisFun ι ℝ).toBasis.map b.repr.symm.toContinuousLinearEquiv.toLinearEquiv).addHaar

Tactic:
exact b.addHaar_eq_volume.symm

Result:
no goals

Proof state:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = map (⇑b.measurableEquiv.symm) (EuclideanSpace.basisFun ι ℝ).toBasis.addHaar

Tactic:
erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]

Result:
case h.e'_6.h
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3✝ : MeasureSpace.toMeasurableSpace = inst✝³
⊢ volume = ((EuclideanSpace.basisFun ι ℝ).toBasis.map b.repr.symm.toContinuousLinearEquiv.toLinearEquiv).addHaar
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem bot_le (x : α) : ⊥ ⊑ x

Proof state:
case hchain
α : Sort u
inst✝ : CCPO α
x✝ x y : α
hx hy : False
⊢ x ⊑ y ∨ y ⊑ x

Tactic:
contradiction

Result:
no goals

Proof state:
case a
α : Sort u
inst✝ : CCPO α
x✝ x : α
hx : False
⊢ x ⊑ x✝

Tactic:
contradiction

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
x : α
⊢ ⊥ ⊑ x

Tactic:
apply csup_le

Result:
case hchain
α : Sort u
inst✝ : CCPO α
x : α
⊢ chain fun x => False

case a
α : Sort u
inst✝ : CCPO α
x : α
⊢ ∀ (y : α), False → y ⊑ x

Proof state:
case hchain
α : Sort u
inst✝ : CCPO α
x : α
⊢ chain fun x => False

Tactic:
intro x y hx hy

Result:
case hchain
α : Sort u
inst✝ : CCPO α
x✝ x y : α
hx hy : False
⊢ x ⊑ y ∨ y ⊑ x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
x : α
⊢ ∀ (y : α), False → y ⊑ x

Tactic:
intro x hx

Result:
case a
α : Sort u
inst✝ : CCPO α
x✝ x : α
hx : False
⊢ x ⊑ x✝
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem units_mem_iff {x : (CliffordAlgebra Q)ˣ} :
    ↑x ∈ pinGroup Q ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ ↑x ∈ pinGroup Q ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)

Tactic:
rw [mem_iff, lipschitzGroup.coe_mem_iff_mem]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem exists_subset_image_finite_and {f : α → β} {s : Set α} {p : Set β → Prop} :
    (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
  Finset.subset_set_image_iff]

Result:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, (∃ s', ↑s' ⊆ s ∧ Finset.image f s' = s_1) ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
classical
simp_rw [@and_comm (_ ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
  Finset.subset_set_image_iff]
aesop

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, (∃ s', ↑s' ⊆ s ∧ Finset.image f s' = s_1) ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem count_associates_factors_eq [DecidableEq (Ideal R)] [DecidableEq <| Associates (Ideal R)]
    [∀ (p : Associates <| Ideal R), Decidable (Irreducible p)]
    {I J : Ideal R} (hI : I ≠ 0) (hJ : J.IsPrime) (hJ₀ : J ≠ ⊥) :
    (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : DecidableEq (Ideal R)
inst✝¹ : DecidableEq (Associates (Ideal R))
inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)

Tactic:
have hJ' : Irreducible (Associates.mk J) := by
  simpa only [Associates.irreducible_mk] using (Ideal.prime_of_isPrime hJ₀ hJ).irreducible

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : DecidableEq (Ideal R)
inst✝¹ : DecidableEq (Associates (Ideal R))
inst✝ : (p : Associates (Ideal R)) → Decidable (Irreducible p)
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)
-- Mathlib/Topology/Basic.lean
theorem closure_eq_compl_interior_compl : closure s = (interior sᶜ)ᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ closure s = (interior sᶜ)ᶜ

Tactic:
rw [interior, closure, compl_sUnion, compl_image_set_of]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ ⋂₀ {t | IsClosed t ∧ s ⊆ t} = ⋂₀ {s_1 | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ}

Tactic:
simp only [compl_subset_compl, isOpen_compl_iff]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem succ_le_castSucc_iff {a b : Fin n} : succ a ≤ castSucc b ↔ a < b

Proof state:
n : ℕ
a b : Fin n
⊢ a.succ ≤ b.castSucc ↔ a < b

Tactic:
rw [le_castSucc_iff, succ_lt_succ_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@[reassoc]
lemma ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality
    {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f)
    (F : C ⥤ D) [F.Additive] :
    F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
      (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ

Tactic:
dsimp

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)

Tactic:
rw [← cancel_epi (P.isoLeftDerivedToHomotopyCategoryObj F).inv, Iso.inv_hom_id_assoc,
  isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc f P Q φ comm F,
  Iso.inv_hom_id, comp_id]

Result:
no goals