harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem toDualRight_symm_toDualLeft (x : M) :
    p.toDualRight.symm.dualMap (p.toDualLeft x) = Dual.eval R M x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
⊢ p.toDualRight.symm.dualMap (p.toDualLeft x) = (Dual.eval R M) x

Tactic:
ext f

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p.toDualRight.symm.dualMap (p.toDualLeft x)) f = ((Dual.eval R M) x) f

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p.toDualRight.symm.dualMap (p.toDualLeft x)) f = ((Dual.eval R M) x) f

Tactic:
simp only [LinearEquiv.dualMap_apply, Dual.eval_apply]

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p.toDualLeft x) (p.toDualRight.symm f) = f x

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p.toDualLeft x) (p.toDualRight.symm f) = f x

Tactic:
exact toDualLeft_of_toDualRight_symm p x f

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem not_mem_of_lt_hitting {m k : ι} (hk₁ : k < hitting u s n m ω) (hk₂ : n ≤ k) :
    u k ω ∉ s

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
⊢ u k ω ∉ s

Tactic:
intro h

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ False

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ k

Tactic:
simp_rw [hitting, if_pos hexists]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ k

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
⊢ u k ω ∉ s

Tactic:
classical
intro h
have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩
refine not_le.2 hk₁ ?_
simp_rw [hitting, if_pos hexists]
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ False

Tactic:
have hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s := ⟨k, ⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ False

Tactic:
refine not_le.2 hk₁ ?_

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ hitting u s n m ω ≤ k

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m k : ι
hk₁ : k < hitting u s n m ω
hk₂ : n ≤ k
h : u k ω ∈ s
hexists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ k

Tactic:
exact csInf_le bddBelow_Icc.inter_of_left ⟨⟨hk₂, le_trans hk₁.le <| hitting_le _⟩, h⟩

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Sigma.lean
theorem isEmbedding_sigmaMk_comp [Nonempty X] :
    IsEmbedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where
  toIsInducing := inducing_sigma.2
    ⟨fun i ↦ (sigmaMk i).isInducing_postcomp IsEmbedding.sigmaMk.isInducing, fun i ↦
      let ⟨x⟩ := ‹Nonempty X›
      ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩
  injective

Proof state:
case mk.mk.intro
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : HEq ⇑g ⇑g'
⊢ ⟨i, g⟩ = ⟨i, g'⟩

Tactic:
simpa using hg

Result:
no goals

Proof state:
case mk.mk
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g : C(X, Y i)
i' : ι
g' : C(X, Y i')
h : (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g => (sigmaMk g.fst).comp g.snd) ⟨i', g'⟩
⊢ ⟨i, g⟩ = ⟨i', g'⟩

Tactic:
obtain ⟨rfl, hg⟩ : i = i' ∧ HEq (⇑g) (⇑g') :=
  Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h

Result:
case mk.mk.intro
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h : (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g'⟩
hg : HEq ⇑g ⇑g'
⊢ ⟨i, g⟩ = ⟨i, g'⟩

Proof state:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
⊢ Function.Injective fun g => (sigmaMk g.fst).comp g.snd

Tactic:
rintro ⟨i, g⟩ ⟨i', g'⟩ h

Result:
case mk.mk
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g : C(X, Y i)
i' : ι
g' : C(X, Y i')
h : (fun g => (sigmaMk g.fst).comp g.snd) ⟨i, g⟩ = (fun g => (sigmaMk g.fst).comp g.snd) ⟨i', g'⟩
⊢ ⟨i, g⟩ = ⟨i', g'⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_sub_cancel' {n m : Nat} (h : m ≤ n) : m + (n - m) = n

Proof state:
n m : Nat
h : m ≤ n
⊢ m + (n - m) = n

Tactic:
rw [Nat.add_comm, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
@[to_additive AddCommute.zsmul_add]
protected lemma mul_zpow (h : Commute a b) : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
  | (n : ℕ)    => by simp [zpow_natCast, h.mul_pow n]
  | .negSucc n => by simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
simp [zpow_natCast, h.mul_pow n]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_two : Squarefree 2

Proof state:
⊢ Squarefree 2

Tactic:
rw [squarefree_iff_nodup_primeFactorsList] <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_natCast_mul {n : ℕ} {f : R[X]} :
    derivative ((n : R[X]) * f) = n * derivative f

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
theorem smul_ae_eq_self_of_mem_zpowers (hs : (x • s : Set α) =ᵐ[μ] s)
    (hy : y ∈ Subgroup.zpowers x) : (y • s : Set α) =ᵐ[μ] s

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x • s =ᶠ[ae μ] s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s

Tactic:
rw [← MulAction.mem_aestabilizer, ← Subgroup.zpowers_le] at hs

Result:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : Subgroup.zpowers x ≤ MulAction.aestabilizer G μ s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : Subgroup.zpowers x ≤ MulAction.aestabilizer G μ s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s

Tactic:
exact hs hy

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_diff [Fintype (s \ t : Set _)] : (s \ t).toFinset = s.toFinset \ t.toFinset

Proof state:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ (s \ t).toFinset ↔ a✝ ∈ s.toFinset \ t.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ (s \ t).toFinset ↔ a✝ ∈ s.toFinset \ t.toFinset
-- Mathlib/NumberTheory/Fermat.lean
theorem fermatNumber_strictMono : StrictMono fermatNumber

Proof state:
⊢ StrictMono fermatNumber

Tactic:
intro m n

Result:
m n : ℕ
⊢ m < n → m.fermatNumber < n.fermatNumber

Proof state:
m n : ℕ
⊢ m < n → m.fermatNumber < n.fermatNumber

Tactic:
simp only [fermatNumber, add_lt_add_iff_right, Nat.pow_lt_pow_iff_right (one_lt_two : 1 < 2),
  imp_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_mk {p : α → Prop} {l : Array { x // p x }} {h : l.size = n} :
    (mk l h).unattach = mk l.unattach (by simpa using h)

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Array { x // p x }
h : l.size = n
⊢ { toArray := l, size_toArray := h }.unattach = { toArray := l.unattach, size_toArray := ⋯ }

Tactic:
simp [unattach]

Result:
no goals

Proof state:
α : Type ?u.73611
n : Nat
p : α → Prop
l : Array { x // p x }
h : l.size = n
⊢ l.unattach.size = n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem pow_apply_coe (χ : MulChar R R') (n : ℕ) (a : Rˣ) : (χ ^ n) a = χ a ^ n

Proof state:
case zero
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ (χ ^ 0) ↑a = χ ↑a ^ 0

Tactic:
rw [pow_zero, pow_zero, one_apply_coe]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ (n + 1)) ↑a = χ ↑a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, mul_apply, ih]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ (χ ^ n) ↑a = χ ↑a ^ n

Tactic:
induction n with
| zero => rw [pow_zero, pow_zero, one_apply_coe]
| succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Basic.lean
theorem lift_range (H : c ≤ ker f) : MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f :=
  Submonoid.ext fun x => ⟨by rintro ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, fun ⟨y, hy⟩ => ⟨↑y, hy⟩⟩

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
⊢ x ∈ MonoidHom.mrange (c.lift f H) → x ∈ MonoidHom.mrange f

Tactic:
rintro ⟨⟨y⟩, hy⟩

Result:
case intro.mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f

Proof state:
case intro.mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : P
w✝ : c.Quotient
y : M
hy : (c.lift f H) (Quot.mk (⇑c.toSetoid) y) = x
⊢ x ∈ MonoidHom.mrange f

Tactic:
exact ⟨y, hy⟩

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_eq_iff {x₁ x₂ : Fin n.succ → ℕ} (hx₁ : ∀ i, x₁ i < d) (hx₂ : ∀ i, x₂ i < d) :
    map d x₁ = map d x₂ ↔ x₁ 0 = x₂ 0 ∧ map d (x₁ ∘ Fin.succ) = map d (x₂ ∘ Fin.succ)

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
have : x₁ 0 = x₂ 0 := by
  rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]

Result:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
⊢ (map d) x₁ = (map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
refine ⟨fun h => ?_, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩

Result:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h

Result:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : ∑ x : Fin n, x₁ x.succ * d ^ ↑x = ∑ x : Fin n, x₂ x.succ * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
⊢ (map d) x₁ = (map d) x₂

Tactic:
rw [map_succ', map_succ', h.1, h.2]

Result:
no goals

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : ∑ x : Fin n, x₁ x.succ * d ^ ↑x = ∑ x : Fin n, x₂ x.succ * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)

Tactic:
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩

Result:
no goals

Proof state:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ x₁ 0 = x₂ 0

Tactic:
rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem univ_eq_singleton_of_card_one {α} [Fintype α] (x : α) (h : Fintype.card α = 1) :
    (univ : Finset α) = {x}

Proof state:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ ≤ #{x}

Tactic:
apply le_of_eq

Result:
case hab
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ = #{x}

Proof state:
case hab
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ = #{x}

Tactic:
simp [h, Finset.card_univ]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ univ = {x}

Tactic:
symm

Result:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ

Proof state:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ {x} = univ

Tactic:
apply eq_of_subset_of_card_le (subset_univ {x})

Result:
α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ ≤ #{x}
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem IsOpen.connectedComponentIn [LocallyConnectedSpace α] {F : Set α} {x : α}
    (hF : IsOpen F) : IsOpen (connectedComponentIn F x)

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ ∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1

Tactic:
intro y hy

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ IsOpen (connectedComponentIn F x)

Tactic:
rw [isOpen_iff_mem_nhds]

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
⊢ ∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y

Tactic:
rw [connectedComponentIn_eq hy]

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F y ∈ 𝓝 y

Tactic:
exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem disjoint_iff_not_le {f : Ultrafilter α} {g : Filter α} : Disjoint (↑f) g ↔ ¬↑f ≤ g

Proof state:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g

Tactic:
rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Icc (e : α ≃o β) (a b : β) : e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Icc a b = Icc (e.symm a) (e.symm b)

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_sub_zsmul (a b : α) (m : ℤ) : toIcoMod hp a (b - m • p) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean
@[reassoc (attr := simp)]
lemma ι_colimitFiberwiseColimitIso_hom (X : C) (d : F.obj X) :
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫
      (colimitFiberwiseColimitIso G).hom = colimit.ι G ⟨X, d⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit (F.map f ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : C
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫ (colimitFiberwiseColimitIso G).hom =
    colimit.ι G { base := X, fiber := d }

Tactic:
simp [colimitFiberwiseColimitIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst)
    {h'} :
    (insertMany m l).1.getKey k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
h' : (insertMany m l).val.contains k' = true
⊢ (insertMany m l).val.getKey k' h' = k

Tactic:
simp_to_model [Const.insertMany] using List.getKey_insertListConst_of_mem

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem pointwise_smul_le_pointwise_smul_iff {a : M} {S T : Ideal R} : a • S ≤ a • T ↔ S ≤ T :=
  ⟨fun h => by simpa using smul_mono_right a⁻¹ h, fun h => smul_mono_right a h⟩

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
h : a • S ≤ a • T
⊢ S ≤ T

Tactic:
simpa using smul_mono_right a⁻¹ h

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.filter_eq (h : l.HasBasis p s) : h.isBasis.filter = l

Proof state:
case h
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
U : Set α
⊢ U ∈ ⋯.filter ↔ U ∈ l

Tactic:
simp [h.mem_iff, IsBasis.mem_filter_iff]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ ⋯.filter = l

Tactic:
ext U

Result:
case h
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
U : Set α
⊢ U ∈ ⋯.filter ↔ U ∈ l
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_X_mul (s : σ) (p : MvPolynomial σ R) :
    (X s * p).support = p.support.map (addLeftEmbedding (Finsupp.single s 1)) :=
  AddMonoidAlgebra.support_single_mul p _ (by simp) _

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), 1 * y = 0 ↔ y = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem ringConGen_le {r : R → R → Prop} {c : RingCon R}
    (h : ∀ x y, r x y → c x y) : ringConGen r ≤ c

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → c x y
⊢ ringConGen r ≤ c

Tactic:
rw [ringConGen_eq]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → c x y
⊢ sInf {s | ∀ (x y : R), r x y → s x y} ≤ c

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → c x y
⊢ sInf {s | ∀ (x y : R), r x y → s x y} ≤ c

Tactic:
exact sInf_le h

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.completeSpace_congr {f : α → β} (hf : IsUniformInducing f)
    (hsurj : f.Surjective) : CompleteSpace α ↔ CompleteSpace β

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]

Result:
no goals
-- Mathlib/Order/Basic.lean
lemma mk_lt_mk_of_lt_of_le (h₁ : a₁ < a₂) (h₂ : b₁ ≤ b₂) : (a₁, b₁) < (a₂, b₂)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ < a₂
h₂ : b₁ ≤ b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1)

Proof state:
n : Nat
⊢ n ∈ range (n + 1)

Tactic:
simp

Result:
no goals