harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Control/Traversable/Lemmas.lean
theorem map_traverse (x : t α) : map f <$> traverse g x = traverse (map f ∘ g) x

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (pure ∘ f) <$> traverse g x = traverse (map f ∘ g) x

Tactic:
refine (comp_traverse (pure ∘ f) g x).symm.trans ?_

Result:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (Comp.mk ∘ map (pure ∘ f) ∘ g) x = traverse (map f ∘ g) x

Tactic:
congr

Result:
case h.e_4.h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Proof state:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ map f <$> traverse g x = traverse (map f ∘ g) x

Tactic:
rw [map_eq_traverse_id f]

Result:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ traverse (pure ∘ f) <$> traverse g x = traverse (map f ∘ g) x

Proof state:
case h.e_4.h
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
apply Comp.applicative_comp_id

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sq : sin x ^ 2 = 1 - cos x ^ 2

Proof state:
x : ℂ
⊢ sin x ^ 2 = 1 - cos x ^ 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_abs (f : Perm α) :
    |(Equiv.Perm.sign f : ℤ)| = 1

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ |↑(sign f)| = 1

Tactic:
rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

Result:
no goals
-- Mathlib/Data/Multiset/Sum.lean
theorem inr_mem_disjSum : inr b ∈ s.disjSum t ↔ b ∈ t

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ (∃ b_1 ∈ t, inr b_1 = inr b) ↔ b ∈ t

Tactic:
simp only [inr.injEq, exists_eq_right]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
a : α
left✝ : a ∈ s
ha : inl a = inr b
⊢ False

Tactic:
exact inl_ne_inr ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ¬∃ a ∈ s, inl a = inr b

Tactic:
rintro ⟨a, _, ha⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
a : α
left✝ : a ∈ s
ha : inl a = inr b
⊢ False

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ inr b ∈ s.disjSum t ↔ b ∈ t

Tactic:
rw [mem_disjSum, or_iff_right]

Result:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ (∃ b_1 ∈ t, inr b_1 = inr b) ↔ b ∈ t

α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ¬∃ a ∈ s, inl a = inr b
-- Mathlib/Algebra/Group/Nat/Hom.lean
lemma ext_nat' [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g :=
  DFunLike.ext f g <| by
    intro n
    induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]

Proof state:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
n : ℕ
⊢ f n = g n

Tactic:
induction n with
| zero => simp_rw [map_zero f, map_zero g]
| succ n ihn =>
  simp [h, ihn]

Result:
no goals

Proof state:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ ∀ (x : ℕ), f x = g x

Tactic:
intro n

Result:
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
n : ℕ
⊢ f n = g n

Proof state:
case zero
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ f 0 = g 0

Tactic:
simp_rw [map_zero f, map_zero g]

Result:
no goals

Proof state:
case succ
A : Type u_3
F : Type u_5
inst✝² : FunLike F ℕ A
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
n : ℕ
ihn : f n = g n
⊢ f (n + 1) = g (n + 1)

Tactic:
simp [h, ihn]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma eq_of_not_mem_uIoc_of_not_mem_uIoc (ha : a ≤ c) (hb : b ≤ c) :
    a ∉ Ι b c → b ∉ Ι a c → a = b

Proof state:
case inr.intro.inl.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b

Tactic:
exact absurd ha (not_le_of_lt ‹c < a›)

Result:
no goals

Proof state:
case inl.intro.inr.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a

Tactic:
exact absurd hb (not_le_of_lt ‹c < b›)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a → b ≤ a ∧ b ≤ c ∨ c < b ∧ a < b → a = b

Tactic:
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;>
    apply le_antisymm <;>
  first |assumption|exact le_of_lt ‹_›|
  exact absurd hb (not_le_of_lt ‹c < b›)|exact absurd ha (not_le_of_lt ‹c < a›)

Result:
no goals

Proof state:
case inr.intro.inr.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a

Tactic:
exact le_of_lt ‹_›

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ∉ Ι b c → b ∉ Ι a c → a = b

Tactic:
simp_rw [not_mem_uIoc]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a → b ≤ a ∧ b ≤ c ∨ c < b ∧ a < b → a = b

Proof state:
case inr.intro.inl.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
assumption

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Preconnected.ofBoxProdRight [Nonempty α] (h : (G □ H).Preconnected) :
    H.Preconnected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
⊢ H.Preconnected

Tactic:
rintro b₁ b₂

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
⊢ H.Reachable b₁ b₂

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
⊢ H.Reachable b₁ b₂

Tactic:
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)

Result:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ H.Reachable b₁ b₂

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
⊢ H.Preconnected

Tactic:
classical
rintro b₁ b₂
obtain ⟨w⟩ := h (Classical.arbitrary _, b₁) (Classical.arbitrary _, b₂)
exact ⟨w.ofBoxProdRight⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝ : Nonempty α
h : (G □ H).Preconnected
b₁ b₂ : β
w : (G □ H).Walk (Classical.arbitrary α, b₁) (Classical.arbitrary α, b₂)
⊢ H.Reachable b₁ b₂

Tactic:
exact ⟨w.ofBoxProdRight⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_empty :
    indicatorConstLp p MeasurableSet.empty (by simp : μ ∅ ≠ ∞) c = 0

Proof state:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ μ ∅ ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = 0

Tactic:
simp only [indicatorConstLp, Set.indicator_empty', MemLp.toLp_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_iff (f : K[X]) :
    Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ f.map i → degree g = 1

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
⊢ Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ map i f → g.degree = 1

Tactic:
rw [Splits, Polynomial.map_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
lemma BoundaryGE.false_of_isTruncLE {j : ι} (hj : e.BoundaryGE j) [e.IsTruncLE] : False

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst✝ : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ False

Tactic:
exact hj.2 i (by simpa only [hi] using hj.1)

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst✝ : e.IsTruncLE
⊢ False

Tactic:
obtain ⟨i, hi⟩ := e.mem_prev hj.1

Result:
case intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst✝ : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ False

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
inst✝ : e.IsTruncLE
i : ι
hi : e.f i = c'.prev (e.f j)
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [hi] using hj.1

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_atTop_principal {s : Set β} : Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
f : α → β
s : Set β
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s

Tactic:
simp_rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets, mem_preimage]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem univBall_target (c : P) {r : ℝ} (hr : 0 < r) : (univBall c r).target = ball c r

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univUnitBall.trans' (unitBallBall c r hr) ⋯).target = ball c r

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univBall c r).target = ball c r

Tactic:
rw [univBall, dif_pos hr]

Result:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univUnitBall.trans' (unitBallBall c r hr) ⋯).target = ball c r
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.lift_K_comp_cyclesIso_inv :
    h.liftK k hk ≫ h.cyclesIso.inv = S.liftCycles k hk

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ h.liftK k hk ≫ h.cyclesIso.inv = S.liftCycles k hk

Tactic:
rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.inf {β} [NormedLatticeAddCommGroup β] {f g : α → β} (hf : Integrable f μ)
    (hg : Integrable g μ) : Integrable (f ⊓ g) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊓ g) 1 μ

Tactic:
exact hf.inf hg

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊓ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : NormedLatticeAddCommGroup β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊓ g) 1 μ
-- Mathlib/Data/Ordmap/Ordset.lean
theorem any_iff_exists {P : α → Prop} : ∀ {t}, Any P t ↔ ∃ x, Emem x t ∧ P x
  | nil => ⟨by rintro ⟨⟩, by rintro ⟨_, ⟨⟩, _⟩⟩
  | node _ l x r => by simp only [Emem]; simp [Any, any_iff_exists, or_and_right, exists_or]

Proof state:
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1

Tactic:
simp [Any, any_iff_exists, or_and_right, exists_or]

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
⊢ Any P nil → ∃ x, Emem x nil ∧ P x

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Emem x_1 (node size✝ l x r) ∧ P x_1

Tactic:
simp only [Emem]

Result:
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1

Proof state:
α : Type u_1
P : α → Prop
⊢ (∃ x, Emem x nil ∧ P x) → Any P nil

Tactic:
rintro ⟨_, ⟨⟩, _⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem C_half_mul_two_eq_one [Invertible (2 : R)] : C (⅟ 2 : R) * 2 = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ C ⅟2 * 2 = 1

Tactic:
rw [mul_comm, two_mul_C_half_eq_one]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pmul_comm [CommMonoidWithZero R] (f g : ArithmeticFunction R) : f.pmul g = g.pmul f

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ f.pmul g = g.pmul f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ (f.pmul g) x✝ = (g.pmul f) x✝

Proof state:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ (f.pmul g) x✝ = (g.pmul f) x✝

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
/-- First coefficient of the product of two power series. -/
lemma coeff_one_mul (φ ψ : R⟦X⟧) : coeff R 1 (φ * ψ) =
    coeff R 1 φ * constantCoeff R ψ + coeff R 1 ψ * constantCoeff R φ

Proof state:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff R 1) (φ * ψ) = (coeff R 1) φ * (constantCoeff R) ψ + (coeff R 1) ψ * (constantCoeff R) φ

Tactic:
rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff,
  mul_comm, add_comm]

Result:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Proof state:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
⊢ antidiagonal 1 = {(0, 1), (1, 0)}

Tactic:
exact rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
⊢ (coeff R 1) (φ * ψ) = (coeff R 1) φ * (constantCoeff R) ψ + (coeff R 1) ψ * (constantCoeff R) φ

Tactic:
have : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl

Result:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (coeff R 1) (φ * ψ) = (coeff R 1) φ * (constantCoeff R) ψ + (coeff R 1) ψ * (constantCoeff R) φ
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a

Proof state:
a b c : Prop
⊢ a ∨ b ∨ c ↔ b ∨ c ∨ a

Tactic:
simp only [or_left_comm, Or.comm]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem mapRange_add {v w : VectorMeasure α M} {f : M →+ N} (hf : Continuous f) :
    (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ⇑f
⊢ (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf

Tactic:
ext

Result:
case h
α : Type u_1
inst✝⁶ : MeasurableSpace α
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑((v + w).mapRange f hf) i✝ = ↑(v.mapRange f hf + w.mapRange f hf) i✝

Proof state:
case h
α : Type u_1
inst✝⁶ : MeasurableSpace α
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑((v + w).mapRange f hf) i✝ = ↑(v.mapRange f hf + w.mapRange f hf) i✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem one_mem_divisors : 1 ∈ divisors n ↔ n ≠ 0

Proof state:
n : ℕ
⊢ 1 ∈ n.divisors ↔ n ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem reverse_cons (a : α) (as : List α) : reverse (a :: as) = reverse as ++ [a]

Proof state:
α : Type u
a : α
as : List α
⊢ as.reverseAux (a :: nil) = as.reverseAux nil ++ a :: nil

Tactic:
rw [← reverseAux_eq_append]

Result:
no goals

Proof state:
α : Type u
a : α
as : List α
⊢ (a :: as).reverse = as.reverse ++ a :: nil

Tactic:
simp [reverse, reverseAux]

Result:
α : Type u
a : α
as : List α
⊢ as.reverseAux (a :: nil) = as.reverseAux nil ++ a :: nil
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
    x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) ↔ n ≤ x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x ↔ n ≤ x.valuation

Tactic:
constructor

Result:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → n ≤ x.valuation

case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ n + c.valuation

Tactic:
exact le_self_add

Result:
no goals

Proof state:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → n ≤ x.valuation

Tactic:
rintro ⟨c, rfl⟩

Result:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Proof state:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Tactic:
suffices c ≠ 0 by
  rw [valuation_p_pow_mul _ _ this]
  exact le_self_add

Result:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0

Proof state:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ x.valuation

Tactic:
simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Tactic:
rw [valuation_p_pow_mul _ _ this]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ n + c.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation

Tactic:
rw [Ideal.mem_span_singleton]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x ↔ n ≤ x.valuation

Proof state:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ x

Tactic:
nth_rewrite 2 [unitCoeff_spec hx]

Result:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ x.valuation

Proof state:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0

Tactic:
rw [hx, mul_zero]

Result:
no goals

Proof state:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0

Tactic:
contrapose! hx

Result:
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
theorem eulerProduct_hasProd (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
    HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)
⊢ HasProd (F ∘ Subtype.val) (∑' (n : ℕ), f n)

Tactic:
rw [hasProd_subtype_iff_mulIndicator,
  show Set.mulIndicator (fun p : ℕ ↦ Irreducible p) =  {p | Nat.Prime p}.mulIndicator from rfl,
  HasProd, Metric.tendsto_atTop]

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x => ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∏ b ∈ n, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_basis (hvs : Set.InjOn v s) (hi : i ∈ s) :
    (Lagrange.basis s v i).degree = ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ (Lagrange.basis s v i).degree = ↑(#s - 1)

Tactic:
rw [degree_eq_natDegree (basis_ne_zero hvs hi), natDegree_basis hvs hi]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem indicator_summable {f : α → ℝ≥0} (hf : Summable f) (s : Set α) :
    Summable (s.indicator f)

Proof state:
case pos
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∈ s
⊢ f a ≤ f a

Tactic:
exact le_refl (f a)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
⊢ (if a ∈ s then f a else 0) ≤ f a

Tactic:
split_ifs

Result:
case pos
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∈ s
⊢ f a ≤ f a

case neg
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∉ s
⊢ 0 ≤ f a

Proof state:
case neg
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
h✝ : a ∉ s
⊢ 0 ≤ f a

Tactic:
exact zero_le_coe

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
⊢ Summable (s.indicator f)

Tactic:
refine NNReal.summable_of_le (fun a => le_trans (le_of_eq (s.indicator_apply f a)) ?_) hf

Result:
α : Type u_1
f : α → ℝ≥0
hf : Summable f
s : Set α
a : α
⊢ (if a ∈ s then f a else 0) ≤ f a
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_embDomain (f : α ↪ α') (l : α →₀ R) :
    (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ f)) l

Proof state:
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ↪ α'
l : α →₀ R
⊢ (linearCombination R v') (embDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
simp [linearCombination_apply, Finsupp.sum, support_embDomain, embDomain_apply]

Result:
no goals