harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ}
    (h : Nat.Coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
  IsCoprime.ne_zero_or_ne_zero (R := A) <| by
    simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

Proof state:
A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b

Tactic:
simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem exists_mem_subalgebra_near_continuous_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ))
    (w : A.SeparatesPoints) (f : X → ℝ) (c : Continuous f) (ε : ℝ) (pos : 0 < ε) :
    ∃ g : A, ∀ x, ‖(g : X → ℝ) x - f x‖ < ε

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε
⊢ ∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε

Tactic:
use g

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε
⊢ ∀ (x : X), ‖↑g x - f x‖ < ε

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
⊢ ∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε

Tactic:
obtain ⟨g, b⟩ := exists_mem_subalgebra_near_continuousMap_of_separatesPoints A w ⟨f, c⟩ ε pos

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε
⊢ ∃ g, ∀ (x : X), ‖↑g x - f x‖ < ε

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖↑g - { toFun := f, continuous_toFun := c }‖ < ε
⊢ ∀ (x : X), ‖↑g x - f x‖ < ε

Tactic:
rwa [norm_lt_iff _ pos] at b

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem le_rank_iff_exists_linearIndependent [Module.Free K V] {c : Cardinal} :
    c ≤ Module.rank K V ↔ ∃ s : Set V, #s = c ∧ LinearIndepOn K id s

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ c ≤ Module.rank K V → ∃ s, #↑s = c ∧ LinearIndepOn K id s

case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ (∃ s, #↑s = c ∧ LinearIndepOn K id s) → c ≤ Module.rank K V

Proof state:
case h.e'_8.h
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
x✝ : V
⊢ x✝ ∈ range ⇑t' ↔ x✝ ∈ range ⇑t

Tactic:
simp [t]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isClosed_iff_clusterPt : IsClosed s ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s :=
  calc
    IsClosed s ↔ closure s ⊆ s := closure_subset_iff_isClosed.symm
    _ ↔ ∀ a, ClusterPt a (𝓟 s) → a ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ closure s ⊆ s ↔ ∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s

Tactic:
simp only [subset_def, mem_closure_iff_clusterPt]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem coe_mul_self_eq (s : Submonoid M) : (s : Set M) * s = s

Proof state:
case h.intro.intro.intro.intro
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
a : M
ha : a ∈ ↑s
b : M
hb : b ∈ ↑s
⊢ (fun x1 x2 => x1 * x2) a b ∈ ↑s

Tactic:
exact s.mul_mem ha hb

Result:
no goals

Proof state:
case h
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s ↔ x ∈ ↑s

Tactic:
refine ⟨?_, fun h => ⟨x, h, 1, s.one_mem, mul_one x⟩⟩

Result:
case h
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s → x ∈ ↑s

Proof state:
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
⊢ ↑s * ↑s = ↑s

Tactic:
ext x

Result:
case h
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s ↔ x ∈ ↑s

Proof state:
case h
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s → x ∈ ↑s

Tactic:
rintro ⟨a, ha, b, hb, rfl⟩

Result:
case h.intro.intro.intro.intro
M : Type u_3
inst✝ : Monoid M
s : Submonoid M
a : M
ha : a ∈ ↑s
b : M
hb : b ∈ ↑s
⊢ (fun x1 x2 => x1 * x2) a b ∈ ↑s
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size

Proof state:
self : UnionFind
i : Nat
⊢ self.parent i < self.size ↔ i < self.size

Tactic:
simp only [parentD]

Result:
self : UnionFind
i : Nat
⊢ (if h : i < self.arr.size then self.arr[i].parent else i) < self.size ↔ i < self.size

Proof state:
self : UnionFind
i : Nat
⊢ (if h : i < self.arr.size then self.arr[i].parent else i) < self.size ↔ i < self.size

Tactic:
split <;> simp only [*, parent'_lt]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Group.lean
theorem tendsto_zero_iff_abs_tendsto_zero (f : α → G) :
    Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f : α → G
⊢ Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)

Tactic:
refine ⟨fun h => (abs_zero : |(0 : G)| = 0) ▸ h.abs, fun h => ?_⟩

Result:
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -|f a|) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Tactic:
exact
  tendsto_of_tendsto_of_tendsto_of_le_of_le this h (fun x => neg_abs_le <| f x) fun x =>
    le_abs_self <| f x

Result:
no goals

Proof state:
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Tactic:
have : Tendsto (fun a => -|f a|) l (𝓝 0) := (neg_zero : -(0 : G) = 0) ▸ h.neg

Result:
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -|f a|) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback v : β} :
    getD (m.insert k v) a fallback = if k == a then v else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
fallback v : β
⊢ getD (m.insert k v) a fallback = if (k == a) = true then v else getD m a fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_insert

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_zero_one_iff {x : R} : Wbtw R 0 x 1 ↔ x ∈ Set.Icc (0 : R) 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (∃ x_1 ∈ Set.Icc 0 1, (1 - x_1) * 0 + x_1 * 1 = x) ↔ x ∈ Set.Icc 0 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (∃ x_1 ∈ Set.Icc 0 1, (lineMap 0 1) x_1 = x) ↔ x ∈ Set.Icc 0 1

Tactic:
simp_rw [lineMap_apply_ring]

Result:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (∃ x_1 ∈ Set.Icc 0 1, (1 - x_1) * 0 + x_1 * 1 = x) ↔ x ∈ Set.Icc 0 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1

Tactic:
rw [Wbtw, affineSegment, Set.mem_image]

Result:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (∃ x_1 ∈ Set.Icc 0 1, (lineMap 0 1) x_1 = x) ↔ x ∈ Set.Icc 0 1
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)] lemma mulEnergy_pos_iff : 0 < Eₘ[s, t] ↔ s.Nonempty ∧ t.Nonempty where
  mp h := of_not_not fun H => by
    simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H
    obtain rfl | rfl := H <;> simp [Nat.not_lt_zero] at h
  mpr h := mulEnergy_pos h.1 h.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
H : ¬(s.Nonempty ∧ t.Nonempty)
⊢ False

Tactic:
simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
H : s = ∅ ∨ t = ∅
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
H : s = ∅ ∨ t = ∅
⊢ False

Tactic:
obtain rfl | rfl := H <;> simp [Nat.not_lt_zero] at h

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph_iff (f : E →ₗ.[R] F) {x : E × F} :
    x ∈ f.graph ↔ ∃ y : f.domain, (↑y : E) = x.1 ∧ f y = x.2

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E × F
⊢ x ∈ f.graph ↔ ∃ y, ↑y = x.1 ∧ ↑f y = x.2

Tactic:
cases x

Result:
case mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ f.graph ↔ ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2

Proof state:
case mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
fst✝ : E
snd✝ : F
⊢ (fst✝, snd✝) ∈ f.graph ↔ ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2

Tactic:
simp_rw [mem_graph_iff', Prod.mk.inj_iff]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem mul_top_of_one_le (hf : 1 ≤ f) : f * ⊤ = ⊤

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤

Tactic:
refine top_le_iff.1 fun s => ?_

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → s ∈ ⊤

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ

Tactic:
rintro ⟨t, ht, hs⟩

Result:
case intro.intro
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ

Proof state:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → s ∈ ⊤

Tactic:
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]

Result:
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ

Proof state:
case intro.intro
α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ

Tactic:
rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_inl : range (@Sum.inl α β) = {x | Sum.isLeft x}

Proof state:
α : Type u_1
β : Type u_2
⊢ range Sum.inl = {x | x.isLeft = true}

Tactic:
ext (_|_) <;> simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem eq_preimage_subtype_val_iff {p : α → Prop} {s : Set (Subtype p)} {t : Set α} :
    s = Subtype.val ⁻¹' t ↔ ∀ (x) (h : p x), (⟨x, h⟩ : Subtype p) ∈ s ↔ x ∈ t :=
  ⟨fun s_eq x h => by
    rw [s_eq]
    simp, fun h => ext fun ⟨x, hx⟩ => by simp [h]⟩

Proof state:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ ⟨x, h⟩ ∈ s ↔ x ∈ t

Tactic:
rw [s_eq]

Result:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ ⟨x, h⟩ ∈ Subtype.val ⁻¹' t ↔ x ∈ t

Proof state:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ ⟨x, h⟩ ∈ Subtype.val ⁻¹' t ↔ x ∈ t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
h : ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t
x✝ : Subtype p
x : α
hx : p x
⊢ ⟨x, hx⟩ ∈ s ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' t

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
    snoc (α := fun _ => α) f a i.rev = cons (α := fun _ => α) a (f ∘ Fin.rev : Fin _ → α) i

Proof state:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ snoc f a i.rev = cons a (f ∘ rev) i

Tactic:
simpa using insertNth_rev (last n) a f i

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppLeft_apply (t : (ι →₀ M) ⊗[R] N) (i : ι) :
    finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t

Proof state:
case zero
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
⊢ ((finsuppLeft R M N ι) 0) i = (rTensor N (Finsupp.lapply i)) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
t : (ι →₀ M) ⊗[R] N
i : ι
⊢ ((finsuppLeft R M N ι) t) i = (rTensor N (Finsupp.lapply i)) t

Tactic:
induction t with
| zero => simp
| tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
| add x y hx hy => simp [map_add, hx, hy]

Result:
no goals

Proof state:
case tmul
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
f : ι →₀ M
n : N
⊢ ((finsuppLeft R M N ι) (f ⊗ₜ[R] n)) i = (rTensor N (Finsupp.lapply i)) (f ⊗ₜ[R] n)

Tactic:
simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]

Result:
no goals

Proof state:
case add
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
x y : (ι →₀ M) ⊗[R] N
hx : ((finsuppLeft R M N ι) x) i = (rTensor N (Finsupp.lapply i)) x
hy : ((finsuppLeft R M N ι) y) i = (rTensor N (Finsupp.lapply i)) y
⊢ ((finsuppLeft R M N ι) (x + y)) i = (rTensor N (Finsupp.lapply i)) (x + y)

Tactic:
simp [map_add, hx, hy]

Result:
no goals
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      (0, n + 2) ::ₘ (n + 2, 0) ::ₘ (antidiagonal n).map (Prod.map Nat.succ Nat.succ)

Proof state:
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]

Result:
n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_le_nhds {a : α} {s : Set α} : 𝓝[s] a ≤ 𝓝 a

Proof state:
case h
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a

Tactic:
exact univ_mem

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a

Tactic:
apply nhdsWithin_le_of_mem

Result:
case h
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a

Tactic:
rw [← nhdsWithin_univ]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_le (a b : α) : ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉

Tactic:
gcongr <;> apply le_ceil

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

Tactic:
rw [ceil_le, Int.cast_add]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b ≤ ↑⌈a⌉ + ↑⌈b⌉
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_self_of_lt_one (h₁ : 0 < x) (h₂ : x < 1) (h₃ : 1 < y) : x ^ y < x

Proof state:
x y : ℝ
h₁ : 0 < x
h₂ : x < 1
h₃ : 1 < y
⊢ x ^ y < x

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_gt h₁ h₂ h₃

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_append {K L : List α} :
    (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.length)

Proof state:
case nil
α : Type u_1
α✝ : Type u_2
L : List α
f : Nat → α → α✝
⊢ mapIdx f ([] ++ L) = mapIdx f [] ++ mapIdx (fun i => f (i + [].length)) L

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : List α
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i => f (i + K.length)) L

Tactic:
induction K generalizing f with
| nil => rfl
| cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]

Result:
no goals

Proof state:
case cons
α : Type u_1
α✝ : Type u_2
L : List α
head✝ : α
tail✝ : List α
ih : ∀ {f : Nat → α → α✝}, mapIdx f (tail✝ ++ L) = mapIdx f tail✝ ++ mapIdx (fun i => f (i + tail✝.length)) L
f : Nat → α → α✝
⊢ mapIdx f (head✝ :: tail✝ ++ L) = mapIdx f (head✝ :: tail✝) ++ mapIdx (fun i => f (i + (head✝ :: tail✝).length)) L

Tactic:
simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]

Result:
no goals
-- Mathlib/RingTheory/EuclideanDomain.lean
theorem left_div_gcd_ne_zero {p q : R} (hp : p ≠ 0) : p / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
nth_rw 1 [hr]

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Proof state:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q

Result:
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
⊢ p / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
exact r0

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
-- Mathlib/Order/Category/BddDistLat.lean
lemma inv_hom_apply {X Y : BddDistLat} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : BddDistLat
e : X ≅ Y
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_one_atTop_pow (x : G) : MapClusterPt 1 atTop (x ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt 1 atTop fun x_1 => x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 0

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group of size at least `p ^ n`
then there is a subgroup of cardinality `p ^ n`. -/
lemma exists_subgroup_card_pow_prime_of_le_card {n p : ℕ} (hp : p.Prime) (h : IsPGroup p G)
    (hn : p ^ n ≤ Nat.card G) : ∃ H : Subgroup G, Nat.card H = p ^ n

Proof state:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
have : Fact p.Prime := ⟨hp⟩

Result:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ ∃ H, Nat.card ↥H = p ^ n

Proof state:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
obtain ⟨m, hm⟩ := h.exists_card_eq

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ H, Nat.card ↥H = p ^ n

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ Nat.card G

Tactic:
rw [hm] at hn ⊢

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m

Proof state:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ Nat.card G ≠ 0

Tactic:
linarith [Nat.one_le_pow n p hp.pos]

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this : Fact (Nat.Prime p)
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]

Result:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
⊢ ∃ H, Nat.card ↥H = p ^ n

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
refine exists_subgroup_card_pow_prime _ ?_

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ Nat.card G

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
this✝ : Fact (Nat.Prime p)
this : Finite G
m : ℕ
hn : p ^ n ≤ p ^ m
hm : Nat.card G = p ^ m
⊢ p ^ n ∣ p ^ m

Tactic:
exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

Result:
no goals