harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem maximalIdeal_eq_span_p : maximalIdeal ℤ_[p] = Ideal.span {(p : ℤ_[p])}

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]

Tactic:
rw [Ideal.span_le, Set.singleton_subset_iff]

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ ↑(maximalIdeal ℤ_[p])

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}

Tactic:
simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits] at hx

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ ↑(maximalIdeal ℤ_[p])

Tactic:
exact p_nonnunit

Result:
no goals

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}

Tactic:
intro x hx

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}

Tactic:
rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] = Ideal.span {↑p}

Tactic:
apply le_antisymm

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}

case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_comm (a b : G) (f : G → α) : τ a (τ b f) = τ b (τ a f)

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a b : G
f : G → α
⊢ τ a (τ b f) = τ b (τ a f)

Tactic:
rw [← translate_add, translate_add']

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsAdjointPair.add {f f' : M → M₁} {g g' : M₁ → M} (h : IsAdjointPair B B' f g)
    (h' : IsAdjointPair B B' f' g') :
    IsAdjointPair B B' (f + f') (g + g') := fun x _ ↦ by
  rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, h, h']

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f + f') x)) x✝ = (B x) ((g + g') x✝)

Tactic:
rw [Pi.add_apply, Pi.add_apply, B'.map_add₂, (B x).map_add, h, h']

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Single.lean
lemma singleObjApplyIsoOfEq_inv_single_map (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
    (singleObjApplyIsoOfEq j X i h).inv ≫ (single j).map f i =
      f ≫ (singleObjApplyIsoOfEq j Y i h).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (singleObjApplyIsoOfEq i X i ⋯).inv ≫ (single i).map f i = f ≫ (singleObjApplyIsoOfEq i Y i ⋯).inv

Tactic:
simp [singleObjApplyIsoOfEq, single]

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
⊢ (singleObjApplyIsoOfEq j X i h).inv ≫ (single j).map f i = f ≫ (singleObjApplyIsoOfEq j Y i h).inv

Tactic:
subst h

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (singleObjApplyIsoOfEq i X i ⋯).inv ≫ (single i).map f i = f ≫ (singleObjApplyIsoOfEq i Y i ⋯).inv
-- Mathlib/Data/ZMod/Basic.lean
theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 else n - a.val

Proof state:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ 0 < a.val

Tactic:
contrapose! h

Result:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a.val ≤ 0
⊢ a = 0

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
rw [if_neg h]

Result:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
by_cases h : a = 0

Result:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Proof state:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a.val ≤ 0
⊢ a = 0

Tactic:
rwa [Nat.le_zero, val_eq_zero] at h

Result:
no goals

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val

Tactic:
apply Nat.mod_eq_of_lt

Result:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
rw [neg_val']

Result:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]

Result:
no goals

Proof state:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n

Tactic:
apply Nat.sub_lt (NeZero.pos n)

Result:
case neg.h
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ 0 < a.val
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} :
    aig.UnsatAt idx hidx → (aig.relabel r).UnsatAt idx (by simp [hidx])

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦assign ∘ r, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ = false
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
h : aig.UnsatAt idx hidx
assign : β → Bool
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false

Tactic:
specialize h (assign ∘ r)

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
assign : β → Bool
h : ⟦assign ∘ r, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ = false
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
⊢ idx < (relabel r aig).decls.size

Tactic:
simp [hidx]

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
⊢ aig.UnsatAt idx hidx → (relabel r aig).UnsatAt idx ⋯

Tactic:
intro h assign

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
aig : AIG α
r : α → β
hidx : idx < aig.decls.size
h : aig.UnsatAt idx hidx
assign : β → Bool
⊢ ⟦assign, { aig := relabel r aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma two_mul_apply_root_root_of_isOrthogonal (P : RootPairing ι R M N)
    (B : LinearMap.BilinForm R M) (i j : ι) (h : B.IsOrthogonal (P.reflection j)) :
    2 * B (P.root i) (P.root j) = P.pairing i j * B (P.root j) (P.root j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : LinearMap.BilinForm R M
i j : ι
h : LinearMap.IsOrthogonal B ⇑(P.reflection j)
⊢ 2 * (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j)

Tactic:
rw [two_mul, ← eq_sub_iff_add_eq]

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : LinearMap.BilinForm R M
i j : ι
h : LinearMap.IsOrthogonal B ⇑(P.reflection j)
⊢ (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : LinearMap.BilinForm R M
i j : ι
h : LinearMap.IsOrthogonal B ⇑(P.reflection j)
⊢ (B ((P.reflection j) (P.root i))) ((P.reflection j) (P.root j)) =
    P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)

Tactic:
rw [reflection_apply, reflection_apply_self, root_coroot'_eq_pairing, LinearMap.map_sub₂,
  LinearMap.map_smul₂, smul_eq_mul, LinearMap.map_neg, LinearMap.map_neg, mul_neg, neg_sub_neg]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : LinearMap.BilinForm R M
i j : ι
h : LinearMap.IsOrthogonal B ⇑(P.reflection j)
⊢ (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)

Tactic:
nth_rw 1 [← h]

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
B : LinearMap.BilinForm R M
i j : ι
h : LinearMap.IsOrthogonal B ⇑(P.reflection j)
⊢ (B ((P.reflection j) (P.root i))) ((P.reflection j) (P.root j)) =
    P.pairing i j * (B (P.root j)) (P.root j) - (B (P.root i)) (P.root j)
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.ins : ∀ {t : RBNode α}, t.Ordered cmp → (ins cmp x t).Ordered cmp
  | nil, _ => ⟨⟨⟩, ⟨⟩, ⟨⟩, ⟨⟩⟩
  | node red a y b, ⟨ay, yb, ha, hb⟩ => by
    unfold ins; split
    · next h => exact ⟨ay.ins ⟨h⟩, yb, ha.ins, hb⟩
    · next h => exact ⟨ay, yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩, ha, hb.ins⟩
    · next h => exact (⟨
        ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
        yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)
  | node black a y b, ⟨ay, yb, ha, hb⟩ => by
    unfold ins; split
    · next h => exact ha.ins.balance1 (ay.ins ⟨h⟩) yb hb
    · next h => exact ha.balance2 ay (yb.ins ⟨OrientedCmp.cmp_eq_gt.1 h⟩) hb.ins
    · next h => exact (⟨
        ay.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_right h).trans h'⟩,
        yb.imp fun ⟨h'⟩ => ⟨(TransCmp.cmp_congr_left h).trans h'⟩, ha, hb⟩)

Proof state:
case h_1
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
x✝ : Ordering
heq✝ : cmp x y = Ordering.lt
⊢ Ordered cmp ((ins cmp x a).balance1 y b)

Tactic:
next h => exact ha.ins.balance1 (ay.ins ⟨h⟩) yb hb

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp (ins cmp x (node black a y b))

Tactic:
unfold ins

Result:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp
    (match cmp x y with
    | Ordering.lt => (ins cmp x a).balance1 y b
    | Ordering.gt => a.balance2 y (ins cmp x b)
    | Ordering.eq => node black a x b)

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp (ins cmp x (node red a y b))

Tactic:
unfold ins

Result:
α : Type u_1
cmp : α → α → Ordering
x : α
a : RBNode α
y : α
b : RBNode α
ay : All (fun x => cmpLT cmp x y) a
yb : All (fun x => cmpLT cmp y x) b
ha : Ordered cmp a
hb : Ordered cmp b
⊢ Ordered cmp
    (match cmp x y with
    | Ordering.lt => node red (ins cmp x a) y b
    | Ordering.gt => node red a y (ins cmp x b)
    | Ordering.eq => node red a x b)
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem dist_le_of_le (hf : HolderOnWith C r f s) (hx : x ∈ s) (hy : y ∈ s)
    {d : ℝ} (hd : dist x y ≤ d) : dist (f x) (f y) ≤ C * d ^ (r : ℝ)

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : ↑(nndist x y) ≤ ↑d
⊢ ↑(nndist (f x) (f y)) ≤ ↑C * ↑d ^ ↑r

Tactic:
norm_cast at hd ⊢

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : dist x y ≤ ↑d
⊢ dist (f x) (f y) ≤ ↑C * ↑d ^ ↑r

Tactic:
rw [dist_nndist] at hd ⊢

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : ↑(nndist x y) ≤ ↑d
⊢ ↑(nndist (f x) (f y)) ≤ ↑C * ↑d ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ
hd : dist x y ≤ d
⊢ dist (f x) (f y) ≤ ↑C * d ^ ↑r

Tactic:
lift d to ℝ≥0 using dist_nonneg.trans hd

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : dist x y ≤ ↑d
⊢ dist (f x) (f y) ≤ ↑C * ↑d ^ ↑r

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r

Tactic:
exact hf.nndist_le_of_le hx hy hd

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem map_surjective [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} :
    Surjective (map f g) ↔ Surjective f ∧ Surjective g :=
  ⟨fun h =>
    ⟨fun c => by
      inhabit δ
      obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
      exact ⟨a, congr_arg Prod.fst h⟩,
      fun d => by
      inhabit γ
      obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
      exact ⟨b, congr_arg Prod.snd h⟩⟩,
    fun h => h.1.prodMap h.2⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
inhabit γ

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
inhabit δ

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c

Proof state:
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d

Tactic:
exact ⟨b, congr_arg Prod.snd h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
⊢ ∃ a, f a = c

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (c, default)

Result:
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c

Proof state:
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
c : γ
inhabited_h : Inhabited δ
a : α
b : β
h : map f g (a, b) = (c, default)
⊢ ∃ a, f a = c

Tactic:
exact ⟨a, congr_arg Prod.fst h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
⊢ ∃ a, g a = d

Tactic:
obtain ⟨⟨a, b⟩, h⟩ := h (default, d)

Result:
case intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h✝ : Surjective (map f g)
d : δ
inhabited_h : Inhabited γ
a : α
b : β
h : map f g (a, b) = (default, d)
⊢ ∃ a, g a = d
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_eq_self (h : y ≤ x) : x \ (x \ y) = y

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ≤ x
⊢ x \ (x \ y) = y

Tactic:
rw [sdiff_sdiff_right_self, inf_of_le_right h]

Result:
no goals
-- Mathlib/AlgebraicTopology/TopologicalSimplex.lean
theorem continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) : Continuous (toTopMap f)

Proof state:
x y : SimplexCategory
f : x ⟶ y
⊢ Continuous (toTopMap f)

Tactic:
refine Continuous.subtype_mk (continuous_pi fun i => ?_) _

Result:
x y : SimplexCategory
f : x ⟶ y
i : ToType y
⊢ Continuous fun a => ∑ j ∈ Finset.filter (fun x_1 => (ConcreteCategory.hom f) x_1 = i) Finset.univ, ↑a j

Proof state:
x y : SimplexCategory
f : x ⟶ y
i : ToType y
⊢ Continuous fun a => ∑ j ∈ Finset.filter (fun x_1 => (ConcreteCategory.hom f) x_1 = i) Finset.univ, ↑a j

Tactic:
exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the positive naturals then they are
equal. -/
lemma ext_nnrat_on_pnat (same_on_pnat : ∀ n : ℕ, 0 < n → f n = g n) : f = g :=
  ext_nnrat' <| DFunLike.congr_fun <| ext_nat''
    ((f : ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕ →*₀ ℚ≥0))
    ((g : ℚ≥0 →*₀ M₀).comp (Nat.castRingHom ℚ≥0 : ℕ →*₀ ℚ≥0)) (by simpa)

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n
⊢ ∀ {n : ℕ}, 0 < n → ((↑f).comp ↑(Nat.castRingHom ℚ≥0)) n = ((↑g).comp ↑(Nat.castRingHom ℚ≥0)) n

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.List.foldr_inf_eq_inf_toFinset [DecidableEq α] (l : List α) :
    l.foldr (· ⊓ ·) ⊤ = l.toFinset.inf id

Proof state:
α : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 => x1 ⊓ x2) ⊤ (↑l).dedup = (↑l).dedup.inf

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
l : List α
⊢ List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l = l.toFinset.inf id

Tactic:
rw [← coe_fold_r, ← Multiset.fold_dedup_idem, inf_def, ← List.toFinset_coe, toFinset_val,
  Multiset.map_id]

Result:
α : Type u_2
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 => x1 ⊓ x2) ⊤ (↑l).dedup = (↑l).dedup.inf
-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
theorem Presheaf.isSheaf_iff_preservesFiniteProducts (F : Cᵒᵖ ⥤ D) :
    IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F

case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_sUnion (x : ZFSet.{u}) : (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Proof state:
x : ZFSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
ext

Result:
case h
x x✝ : ZFSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)

Proof state:
case h
x x✝ : ZFSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
    (∑ i ∈ range (n + 2), ((n + 1).choose i : R) * f i (n + 1 - i)) =
      (∑ i ∈ range (n + 1), (n.choose i : R) * f i (n + 1 - i)) +
        ∑ i ∈ range (n + 1), (n.choose i : R) * f (i + 1) (n - i)

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i ∈ range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) =
    ∑ i ∈ range (n + 1), ↑(n.choose i) * f i (n + 1 - i) + ∑ i ∈ range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)

Tactic:
simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_δ_of_mono {n : ℕ} (θ : mk n ⟶ mk (n + 1)) [Mono θ] : ∃ i : Fin (n + 2), θ = δ i

Proof state:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)

Tactic:
rw [← h]

Result:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono θ

Proof state:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Function.Surjective ⇑(Hom.toOrderHom θ)

Tactic:
by_contra h

Result:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
h : Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ False

Proof state:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
h : Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ False

Tactic:
simpa using le_of_epi (epi_iff_surjective.mpr h)

Result:
no goals

Proof state:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i

Tactic:
rw [h, eq_id_of_mono θ', Category.id_comp]

Result:
no goals

Proof state:
case intro.intro
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i

Tactic:
use i

Result:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ θ = δ i

Proof state:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ∃ i, θ = δ i

Tactic:
rcases eq_comp_δ_of_not_surjective θ (by
  by_contra h
  simpa using le_of_epi (epi_iff_surjective.mpr h)) with ⟨i, θ', h⟩

Result:
case intro.intro
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i

Proof state:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ θ = δ i

Tactic:
haveI : Mono (θ' ≫ δ i) := by
  rw [← h]
  infer_instance

Result:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i

Proof state:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i

Tactic:
haveI := CategoryTheory.mono_of_mono θ' (δ i)

Result:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i

Proof state:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono θ

Tactic:
infer_instance

Result:
no goals