harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bounded_singleton {r : α → α → Prop} [IsWellOrder α r] (hr : (type r).IsLimit) (x) :
    Bounded r {x}

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x : α
⊢ ∀ b ∈ {x}, r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
intro b hb

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r ((enum r) ⟨(typein r).toRelEmbedding x, ⋯⟩) ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
nth_rw 1 [← enum_typein r x]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r ((enum r) ⟨(typein r).toRelEmbedding x, ⋯⟩) ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)

Tactic:
apply lt_succ

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
rw [mem_singleton_iff.1 hb]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x b : α
hb : b ∈ {x}
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x : α
⊢ Bounded r {x}

Tactic:
refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (type r).IsLimit
x : α
⊢ ∀ b ∈ {x}, r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    let a := n + 2
    have ha : a ≠ 1 := Nat.succ_succ_ne_one n
    simp only [a, true_iff, Ne, not_false_iff, ha]
    exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩

Proof state:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
simp only [a, true_iff, Ne, not_false_iff, ha]

Result:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n + 2

Proof state:
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
have ha : a ≠ 1 := Nat.succ_succ_ne_one n

Result:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Proof state:
⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1

Tactic:
simp [Nat.not_prime_one]

Result:
no goals

Proof state:
⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0

Tactic:
simpa using Exists.intro 2 Nat.prime_two

Result:
no goals

Proof state:
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩

Result:
no goals

Proof state:
n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
let a := n + 2

Result:
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_eq_some : or o o' = some a ↔ o = some a ∨ (o = none ∧ o' = some a)

Proof state:
α✝ : Type u_1
o o' : Option α✝
a : α✝
⊢ o.or o' = some a ↔ o = some a ∨ o = none ∧ o' = some a

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem inf_himp (a b : α) : a ⊓ (a ⇨ b) = a ⊓ b :=
  le_antisymm (le_inf inf_le_left <| by rw [inf_comm, ← le_himp_iff]) <| inf_le_inf_left _ le_himp

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ (a ⇨ b) ≤ b

Tactic:
rw [inf_comm, ← le_himp_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Lemmas.lean
theorem map_inj_of_left_inverse [Applicative m] [LawfulApplicative m] {f : α → β}
    (w : ∃ g : β → α, ∀ x, g (f x) = x) {x y : m α}
    (h : f <$> x = f <$> y) : x = y

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
f : α → β
w : ∃ g, ∀ (x : α), g (f x) = x
x y : m α
h : f <$> x = f <$> y
⊢ x = y

Tactic:
rcases w with ⟨g, w⟩

Result:
case intro
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
f : α → β
x y : m α
h : f <$> x = f <$> y
g : β → α
w : ∀ (x : α), g (f x) = x
⊢ x = y

Proof state:
case intro
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
f : α → β
x y : m α
g : β → α
w : ∀ (x : α), g (f x) = x
h : (fun x => g <$> x) (f <$> x) = (fun x => g <$> x) (f <$> y)
⊢ x = y

Tactic:
simpa [w] using h

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
theorem isBoundedAtImInfty_iff {α : Type*} [Norm α] {f : ℍ → α} :
    IsBoundedAtImInfty f ↔ ∃ M A : ℝ, ∀ z : ℍ, A ≤ im z → ‖f z‖ ≤ M

Proof state:
α : Type u_1
inst✝ : Norm α
f : ℍ → α
⊢ IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ M

Tactic:
simp [IsBoundedAtImInfty, BoundedAtFilter, Asymptotics.isBigO_iff, Filter.Eventually,
  atImInfty_mem]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem image_subset_iff_subset_preimage [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β}
    (hf : Set.InjOn f (f ⁻¹' ↑t)) : s.image f ⊆ t ↔ s ⊆ t.preimage f hf :=
  image_subset_iff.trans <| by simp only [subset_iff, mem_preimage]

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
hf : InjOn f (f ⁻¹' ↑t)
⊢ (∀ x ∈ s, f x ∈ t) ↔ s ⊆ t.preimage f hf

Tactic:
simp only [subset_iff, mem_preimage]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b_relation_of_char_two : W.b₂ * W.b₆ = W.b₄ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₂ * W.b₆ = W.b₄ ^ 2

Tactic:
linear_combination -W.b_relation + 2 * W.b₈ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_diff_singleton_of_mem (h : a ∈ s) :
    (s \ {a}).encard = s.encard - 1

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard = s.encard - 1

Tactic:
rw [← encard_diff_singleton_add_one h, ← WithTop.add_right_inj WithTop.one_ne_top,
  tsub_add_cancel_of_le (self_le_add_left _ _)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem eq_zero_of_hasseDeriv_eq_zero {R} [CommRing R] (f : R[X]) (r : R)
    (h : ∀ k, (hasseDeriv k f).eval r = 0) : f = 0

Proof state:
case a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = (taylor r) 0

Tactic:
rw [LinearMap.map_zero]

Result:
case a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = 0

Proof state:
case a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = 0

Tactic:
ext k

Result:
case a.a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
k : ℕ
⊢ ((taylor r) f).coeff k = coeff 0 k

Proof state:
case a.a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
k : ℕ
⊢ ((taylor r) f).coeff k = coeff 0 k

Tactic:
simp only [taylor_coeff, h, coeff_zero]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ f = 0

Tactic:
apply taylor_injective r

Result:
case a
R : Type u_2
inst✝ : CommRing R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = (taylor r) 0
-- Mathlib/Algebra/Order/Pi.lean
@[to_additive extend_nonneg] lemma one_le_extend (hg : 1 ≤ g) (he : 1 ≤ e) : 1 ≤ extend f g e :=
  fun _b ↦ by classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
classical exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : One γ
inst✝ : LE γ
f : α → β
g : α → γ
e : β → γ
hg : 1 ≤ g
he : 1 ≤ e
_b : β
⊢ 1 _b ≤ extend f g e _b

Tactic:
exact one_le_dite (fun _ ↦ hg _) (fun _ ↦ he _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_replicate (a : α) (n : Nat) : (replicate n a).head? = if n = 0 then none else some a

Proof state:
α : Type u_1
a : α
n : Nat
⊢ (replicate n a).head? = if n = 0 then none else some a

Tactic:
cases n <;> simp [replicate_succ]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_of_models_theory {T' : L.Theory}
    (h : ∀ φ : L.Sentence, φ ∈ T' → T ⊨ᵇ φ)
    {φ : L.Formula α} (hφ : T' ⊨ᵇ φ) : T ⊨ᵇ φ := fun M => by
  have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)
  let M' : ModelType T' := ⟨M⟩
  exact hφ M'

Proof state:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : ↑M ⊨ T'
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
let M' : ModelType T' := ⟨M⟩

Result:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : ↑M ⊨ T'
M' : T'.ModelType := ModelType.mk ↑M
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Proof state:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)

Result:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : ↑M ⊨ T'
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Proof state:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : ↑M ⊨ T'
M' : T'.ModelType := ModelType.mk ↑M
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
exact hφ M'

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
theorem IsIntegral.smul {R} [CommSemiring R] [Algebra R B] [Algebra S B] [Algebra R S]
    [IsScalarTower R S B] {x : B} (r : R)(hx : IsIntegral S x) : IsIntegral S (r • x) :=
  .of_mem_of_fg _ hx.fg_adjoin_singleton _ <| by
    rw [← algebraMap_smul S]; apply Subalgebra.smul_mem; exact Algebra.subset_adjoin rfl

Proof state:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ Algebra.adjoin S {x}

Tactic:
apply Subalgebra.smul_mem

Result:
case hx
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ Algebra.adjoin S {x}

Proof state:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ r • x ∈ Algebra.adjoin S {x}

Tactic:
rw [← algebraMap_smul S]

Result:
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ (algebraMap R S) r • x ∈ Algebra.adjoin S {x}

Proof state:
case hx
B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ x ∈ Algebra.adjoin S {x}

Tactic:
exact Algebra.subset_adjoin rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem monomial_has_deriv_aux (t x : ℝ) (n : ℕ) :
    HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(n + 1) * (x - t) ^ n) t

Proof state:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t

Tactic:
simp_rw [sub_eq_neg_add]

Result:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t

Proof state:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t

Tactic:
rw [← neg_one_mul, mul_comm (-1 : ℝ), mul_assoc, mul_comm (-1 : ℝ), ← mul_assoc]

Result:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t

Proof state:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t

Tactic:
convert HasDerivAt.pow (n + 1) ((hasDerivAt_id t).neg.add_const x)

Result:
case h.e'_9.h.e'_5.h.e'_5
t x : ℝ
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

Proof state:
case h.e'_9.h.e'_5.h.e'_5
t x : ℝ
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

Tactic:
simp only [Nat.cast_add, Nat.cast_one]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r • x + s • x :=
  have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by simp_rw [TensorProduct.smul_zero, add_zero])
    (fun m n => by simp_rw [this, add_smul, add_tmul]) fun x y ihx ihy => by
    simp_rw [TensorProduct.smul_add]
    rw [ihx, ihy, add_add_add_comm]

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]

Result:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
r s : R''
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ (r + s) • m ⊗ₜ[R] n = r • m ⊗ₜ[R] n + s • m ⊗ₜ[R] n

Tactic:
simp_rw [this, add_smul, add_tmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
r s : R''
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ (r + s) • 0 = r • 0 + s • 0

Tactic:
simp_rw [TensorProduct.smul_zero, add_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)

Tactic:
rw [ihx, ihy, add_add_add_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero (x y : F) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [@norm_sub_mul_self ℝ, add_right_cancel_iff, sub_eq_add_neg, add_right_eq_self, neg_eq_zero,
  mul_eq_zero]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_diff_singleton (y : E) :
    HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
y : E
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x

Tactic:
rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem isOpen_cylinder (x : ∀ n, E n) (n : ℕ) : IsOpen (cylinder x n)

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen (cylinder x n)

Tactic:
rw [PiNat.cylinder_eq_pi]

Result:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen ((↑(Finset.range n)).pi fun i => {x i})

Proof state:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
x : (n : ℕ) → E n
n : ℕ
⊢ IsOpen ((↑(Finset.range n)).pi fun i => {x i})

Tactic:
exact isOpen_set_pi (Finset.range n).finite_toSet fun a _ => isOpen_discrete _

Result:
no goals
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrictComp_surjective (hq : q.natDegree ≠ 0) :
    Function.Surjective (restrictComp p q hq)

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
⊢ Function.Surjective ⇑(restrictComp p q hq)

Tactic:
haveI : Fact (Splits (algebraMap F (SplittingField (comp p q))) p) :=
  ⟨splits_in_splittingField_of_comp p q hq⟩

Result:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
this : Fact (Splits (algebraMap F (p.comp q).SplittingField) p)
⊢ Function.Surjective ⇑(restrictComp p q hq)

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
this : Fact (Splits (algebraMap F (p.comp q).SplittingField) p)
⊢ Function.Surjective ⇑(restrictComp p q hq)

Tactic:
simpa only [restrictComp] using restrict_surjective _ _

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp] lemma cast_nonpos : (n : R) ≤ 0 ↔ n ≤ 0

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n ≤ 0 ↔ n ≤ 0

Tactic:
rw [← cast_zero, cast_le]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_empty : (∅ : Set α).encard = 0

Proof state:
α : Type u_1
⊢ ∅.encard = 0

Tactic:
rw [encard_eq_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem HD_bound_aux1 [Nonempty Y] (f : Cb X Y) (C : ℝ) :
    BddAbove (range fun x : X => ⨅ y, f (inl x, inr y) + C)

Proof state:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
x : X
⊢ ⨅ y, f (inl x, inr y) + C ≤ Cf + C

Tactic:
calc
  ⨅ y, f (inl x, inr y) + C ≤ f (inl x, inr default) + C := ciInf_le (HD_below_aux1 C) default
  _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Result:
no goals

Proof state:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun x => ⨅ y, f (inl x, inr y) + C)

Tactic:
refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩

Result:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
x : X
⊢ ⨅ y, f (inl x, inr y) + C ≤ Cf + C

Proof state:
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
C : ℝ
⊢ BddAbove (range fun x => ⨅ y, f (inl x, inr y) + C)

Tactic:
obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove

Result:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun x => ⨅ y, f (inl x, inr y) + C)
-- Mathlib/Analysis/Convex/Hull.lean
theorem convexHull_eq_iInter : convexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : Convex 𝕜 t), t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t

Tactic:
simp [convexHull, iInter_subtype, iInter_and]

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem sub_le (a b : ℕ+) : a - b ≤ a

Proof state:
case pos
a b : ℕ+
h : b < a
⊢ ↑a - ↑b ≤ ↑a

Tactic:
exact Nat.sub_le a b

Result:
no goals

Proof state:
a b : ℕ+
⊢ a - b ≤ a

Tactic:
rw [← coe_le_coe, sub_coe]

Result:
a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a

Proof state:
a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a

Tactic:
split_ifs with h

Result:
case pos
a b : ℕ+
h : b < a
⊢ ↑a - ↑b ≤ ↑a

case neg
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ ↑a

Proof state:
case neg
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ ↑a

Tactic:
exact a.2

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_biUnion_left (s : Finset ι) (t : Finset β) (f : ι → Finset α) :
    interedges r (s.biUnion f) t = s.biUnion fun a ↦ interedges r (f a) t

Proof state:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a✝ : α × β
⊢ a✝ ∈ interedges r (s.biUnion f) t ↔ a✝ ∈ s.biUnion fun a => interedges r (f a) t

Tactic:
simp only [mem_biUnion, mem_interedges_iff, exists_and_right, ← and_assoc]

Result:
no goals

Proof state:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
⊢ interedges r (s.biUnion f) t = s.biUnion fun a => interedges r (f a) t

Tactic:
ext

Result:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset β
f : ι → Finset α
a✝ : α × β
⊢ a✝ ∈ interedges r (s.biUnion f) t ↔ a✝ ∈ s.biUnion fun a => interedges r (f a) t
-- Mathlib/Data/Int/Cast/Lemmas.lean
theorem eq_intCastAddHom (f : ℤ →+ A) (h1 : f 1 = 1) : f = Int.castAddHom A :=
  ext_int <| by simp [h1]

Proof state:
A : Type u_5
inst✝ : AddGroupWithOne A
f : ℤ →+ A
h1 : f 1 = 1
⊢ f 1 = (castAddHom A) 1

Tactic:
simp [h1]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_neg (a : FreeAbelianGroup X) : support (-a) = support a

Proof state:
X : Type u_1
a : FreeAbelianGroup X
⊢ (-a).support = a.support

Tactic:
simp only [support, AddMonoidHom.map_neg, Finsupp.support_neg]

Result:
no goals