harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Fraisse.lean
theorem age.fg_substructure {S : L.Substructure M} (fg : S.FG) : Bundled.mk S ∈ L.age M

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
fg : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age M

Tactic:
exact ⟨(Substructure.fg_iff_structure_fg _).1 fg, ⟨subtype _⟩⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_one : (∫ _ in a..b, (1 : ℝ)) = b - a

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 = b - a

Tactic:
simp only [mul_one, smul_eq_mul, integral_const]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem IsInternal.collectedBasis_repr_of_mem_ne (h : IsInternal A) {α : ι → Type*}
    (v : ∀ i, Basis (α i) R (A i)) {x : M} {i j : ι} (hij : i ≠ j) {a : α j} (hx : x ∈ A i) :
    (h.collectedBasis v).repr x ⟨j, a⟩ = 0

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((h.collectedBasis v).repr x) ⟨j, a⟩ = 0

Tactic:
change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _

Result:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((sigmaFinsuppLequivDFinsupp R).symm
        (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x)))
      ⟨j, a⟩ =
    0

Proof state:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
x : M
i j : ι
hij : i ≠ j
a : α j
hx : x ∈ A i
⊢ ((sigmaFinsuppLequivDFinsupp R).symm
        (DFinsupp.mapRange (fun i => ⇑(v i).repr) ⋯ (↑(LinearEquiv.ofBijective (coeLinearMap A) h).symm x)))
      ⟨j, a⟩ =
    0

Tactic:
simp [h.ofBijective_coeLinearMap_of_mem_ne hij hx]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
@[simp] lemma cond_eq_zero : μ[|s] = 0 ↔ μ s = ∞ ∨ μ s = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ μ[|s] = 0 ↔ μ s = ⊤ ∨ μ s = 0

Tactic:
simp [cond]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem tendsto_lift_nhds_mk {f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {l : Filter α} :
    Tendsto (lift f hf) (𝓝 <| mk x) l ↔ Tendsto f (𝓝 x) l

Proof state:
X : Type u_1
α : Type u_4
inst✝ : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
l : Filter α
⊢ Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l

Tactic:
simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma ofTensorProduct_eq :
    ofTensorProduct I (ι → R) = (piEquivOfFintype I (ι := ι) (fun _ : ι ↦ R)).symm.toLinearMap ∘ₗ
      (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).toLinearMap

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    ↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)

Tactic:
rw [← piEquivOfFintype_comp_ofTensorProduct_eq I ι, ← LinearMap.comp_assoc]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    (↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piEquivOfFintype I fun x => R)) ∘ₗ ofTensorProduct I (ι → R)

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) =
    (↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piEquivOfFintype I fun x => R)) ∘ₗ ofTensorProduct I (ι → R)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_map (f : β → γ) (l : Array β) : findSome? p (l.map f) = l.findSome? (p ∘ f)

Proof state:
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
l : Array β
⊢ findSome? p (map f l) = findSome? (p ∘ f) l

Tactic:
cases l

Result:
case mk
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
toList✝ : List β
⊢ findSome? p (map f { toList := toList✝ }) = findSome? (p ∘ f) { toList := toList✝ }

Proof state:
case mk
β : Type u_1
γ : Type u_2
α✝ : Type u_3
p : γ → Option α✝
f : β → γ
toList✝ : List β
⊢ findSome? p (map f { toList := toList✝ }) = findSome? (p ∘ f) { toList := toList✝ }

Tactic:
simp [List.findSome?_map]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux_cons (t : α) (ts is : List α) :
    permutationsAux (t :: ts) is =
      foldr (fun y r => (permutationsAux2 t ts r y id).2) (permutationsAux ts (t :: is))
        (permutations is)

Proof state:
α : Type u_1
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).2)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) ts (t :: is))
      is.permutations

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
t : α
ts is : List α
⊢ (t :: ts).permutationsAux is =
    foldr (fun y r => (permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations

Tactic:
rw [permutationsAux, permutationsAux.rec]

Result:
α : Type u_1
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).2)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)) ts (t :: is))
      is.permutations
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_add_of_degree_lt_left {p q : R[X]} (pq : q.degree < p.degree) :
    (p + q).eraseLead = p.eraseLead + q

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ ¬n = (p + q).natDegree

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree

Tactic:
simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_degree_lt pq).symm]

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ 0 = (p.eraseLead + q).coeff p.natDegree

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
rintro rfl

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
⊢ (p + q).eraseLead = p.eraseLead + q

Tactic:
ext n

Result:
case a
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_left_of_degree_lt pq)

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

Tactic:
by_cases nd : n = p.natDegree

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem prod_multiset_X_sub_C_dvd (p : R[X]) : (p.roots.map fun a => X - C a).prod ∣ p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (Multiset.map (fun a => X - C a) p.roots).prod ∣ p

Tactic:
rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R) monic_prod_multiset_X_sub_C]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.map (fun a => X - C a) p.roots).prod ∣
    map (algebraMap R (FractionRing R)) p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∏ i ∈ p.roots.toFinset, map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p) ∣
    map (algebraMap R (FractionRing R)) p

Tactic:
refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_

Result:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i => map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p)) a b

case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝ : a ∈ p.roots.toFinset
⊢ map (algebraMap R (FractionRing R)) ((X - C a) ^ rootMultiplicity a p) ∣ map (algebraMap R (FractionRing R)) p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.map (fun a => X - C a) p.roots).prod ∣
    map (algebraMap R (FractionRing R)) p

Tactic:
rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∏ i ∈ p.roots.toFinset, map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p) ∣
    map (algebraMap R (FractionRing R)) p

Proof state:
case refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝ : a ∈ p.roots.toFinset
⊢ map (algebraMap R (FractionRing R)) ((X - C a) ^ rootMultiplicity a p) ∣ map (algebraMap R (FractionRing R)) p

Tactic:
exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i => map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p)) a b

Tactic:
simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]

Result:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i => (X - C ((algebraMap R (FractionRing R)) i)) ^ rootMultiplicity i p) a b

Proof state:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i => (X - C ((algebraMap R (FractionRing R)) i)) ^ rootMultiplicity i p) a b

Tactic:
exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_subtype_lt [Finite α] {p : α → Prop} {x : α} (hx : ¬p x) :
    Nat.card { x // p x } < Nat.card α

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
classical
haveI := Fintype.ofFinite α
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_descFactorial_eq_ascFactorial' (n : ℕ) :
    ∀ k : ℕ, (n + k - 1).descFactorial k = n.ascFactorial k
  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
  | succ k => by
    rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
      add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
      Nat.add_sub_cancel]

Proof state:
n k : ℕ
⊢ (n + k.succ - 1).descFactorial k.succ = n.ascFactorial k.succ

Tactic:
rw [descFactorial_succ, ascFactorial_succ, ← succ_add_eq_add_succ,
  add_descFactorial_eq_ascFactorial' _ k, ← succ_ascFactorial, succ_add_sub_one,
  Nat.add_sub_cancel]

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0

Tactic:
rw [ascFactorial_zero, descFactorial_zero]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.toCore_toTopologicalSpace (u : UniformSpace α) :
    u.toCore.toTopologicalSpace = u.toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by
    rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

Proof state:
α : Type ua
u : UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = id _ _

Proof state:
R₁ : Type u_1
inst✝³ : Semiring R₁
M₁ : Type u_4
inst✝² : TopologicalSpace M₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ →L[R₁] M₁
⊢ ↑f = LinearMap.id ↔ f = id R₁ M₁

Tactic:
rw [← coe_id, coe_inj]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_self_of_le_one {x : ℝ≥0∞} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) : x ^ z ≤ x

Proof state:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
nth_rw 2 [← ENNReal.rpow_one x]

Result:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1

Proof state:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_add_of_disjoint [DecidableEq σ] (h : Disjoint p.vars q.vars) :
    (p + q).vars = p.vars ∪ q.vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Disjoint p.degrees q.degrees
hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset
⊢ x ∈ (p + q).degrees.toFinset

Tactic:
rwa [degrees_add_of_disjoint h, Multiset.toFinset_union]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint p.vars q.vars
x : σ
hx : x ∈ p.vars ∪ q.vars
⊢ x ∈ (p + q).vars

Tactic:
simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
x : σ
h : Disjoint p.degrees q.degrees
hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset
⊢ x ∈ (p + q).degrees.toFinset

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint p.vars q.vars
⊢ (p + q).vars = p.vars ∪ q.vars

Tactic:
refine (vars_add_subset p q).antisymm fun x hx => ?_

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint p.vars q.vars
x : σ
hx : x ∈ p.vars ∪ q.vars
⊢ x ∈ (p + q).vars
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_eq_spanSingleton [NoZeroSMulDivisors R P] {x y : P} :
    spanSingleton S x = spanSingleton S y ↔ ∃ z : Rˣ, z • x = y

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsLocalization S P
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ ⟨span R {x}, ⋯⟩ = ⟨span R {y}, ⋯⟩ ↔ span R {x} = span R {y}

Tactic:
exact Subtype.mk_eq_mk

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsLocalization S P
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ spanSingleton S x = spanSingleton S y ↔ ∃ z, z • x = y

Tactic:
rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]

Result:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsLocalization S P
inst✝ : NoZeroSMulDivisors R P
x y : P
⊢ ⟨span R {x}, ⋯⟩ = ⟨span R {y}, ⋯⟩ ↔ span R {x} = span R {y}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Sigma.fst) :
    getKeyD k' (insertList l toInsert) fallback = k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k k' fallback : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Sigma.fst toInsert
⊢ getKeyD k' (insertList l toInsert) fallback = k

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem,
  Option.getD_some]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma hasSmallLocalizedHom_iff_of_isos {X' Y' : C} (e : X ≅ X') (e' : Y ≅ Y') :
    HasSmallLocalizedHom.{w} W X Y ↔ HasSmallLocalizedHom.{w} W X' Y'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')

Tactic:
exact small_congr (Iso.homCongr (W.Q.mapIso e) (W.Q.mapIso e'))

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurve_comp_add {dt : ℝ} :
    IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ (· + dt)) v

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
⊢ IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x + dt) v

Tactic:
refine ⟨fun hγ ↦ hγ.comp_add _, fun hγ ↦ ?_⟩

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
⊢ IsIntegralCurve γ v

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
⊢ IsIntegralCurve γ v

Tactic:
convert hγ.comp_add (-dt)

Result:
case h.e'_10
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
⊢ γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt

Proof state:
case h.e'_10
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
⊢ γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt

Tactic:
ext t

Result:
case h.e'_10.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
t : ℝ
⊢ γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t

Proof state:
case h.e'_10.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
hγ : IsIntegralCurve (γ ∘ fun x => x + dt) v
t : ℝ
⊢ γ t = ((γ ∘ fun x => x + dt) ∘ fun x => x + -dt) t

Tactic:
simp only [Function.comp_apply, neg_add_cancel_right]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
@[simp] lemma lowerBounds_closure (s : Set α) : lowerBounds (closure s : Set α) = lowerBounds s :=
  ext fun a ↦ by simp_rw [mem_lowerBounds_iff_subset_Ici, isClosed_Ici.closure_subset_iff]

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIciTopology α
s : Set α
a : α
⊢ a ∈ lowerBounds (closure s) ↔ a ∈ lowerBounds s

Tactic:
simp_rw [mem_lowerBounds_iff_subset_Ici, isClosed_Ici.closure_subset_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_eq_iInter_thickening'' (δ : ℝ) (E : Set α) :
    cthickening δ E = ⋂ (ε : ℝ) (_ : max 0 δ < ε), thickening ε E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : 0 ⊔ δ < ε), thickening ε E

Tactic:
rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]

Result:
case δ_nn
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ 0 ≤ 0 ⊔ δ

Proof state:
case δ_nn
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ 0 ≤ 0 ⊔ δ

Tactic:
exact le_max_left _ _

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem extendSubtype_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : p x) :
    q (e.extendSubtype x)

Proof state:
case h.e'_1
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ e.extendSubtype x = ↑(e ⟨x, hx⟩)

Tactic:
rw [e.extendSubtype_apply_of_mem _ hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ q (e.extendSubtype x)

Tactic:
convert (e ⟨x, hx⟩).2

Result:
case h.e'_1
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ e.extendSubtype x = ↑(e ⟨x, hx⟩)