harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem zero_of_num_eq_bot [NoZeroSMulDivisors R P] (hS : 0 ∉ S) {I : FractionalIdeal S P}
    (hI : I.num = ⊥) : I = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ ↑I ≤ ⊥

Tactic:
intro x hx

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ x ∈ ⊥

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ I = 0

Tactic:
rw [← coeToSubmodule_eq_bot, eq_bot_iff]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
⊢ ↑I ≤ ⊥

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ ↑I.den • x = 0

Tactic:
have h_eq : I.den • (I : Submodule R P) = ⊥ := by rw [den_mul_self_eq_num, hI, Submodule.map_bot]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
h_eq : I.den • ↑I = ⊥
⊢ ↑I.den • x = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ I.den • ↑I = ⊥

Tactic:
rw [den_mul_self_eq_num, hI, Submodule.map_bot]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ x ∈ ⊥

Tactic:
suffices (den I : R) • x = 0 from
  (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ ↑I.den • x = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : NoZeroSMulDivisors R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
h_eq : I.den • ↑I = ⊥
⊢ ↑I.den • x = 0

Tactic:
exact (Submodule.eq_bot_iff _).mp h_eq (den I • x) ⟨x, hx, rfl⟩

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem norm_conj (z : ℂ) : ‖conj z‖ = ‖z‖

Proof state:
z : ℂ
⊢ ‖(starRingEnd ℂ) z‖ = ‖z‖

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem disjoint_nhdsSet_principal : Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)

Tactic:
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftOn'_div {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ p, f p 0 = f 0 1)
    (H) :
    (RatFunc.liftOn' (algebraMap _ (RatFunc K) p / algebraMap _ _ q)) f @H = f p q

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn' f H = f p q

Tactic:
rw [RatFunc.liftOn', liftOn_div _ _ _ f0]

Result:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'

Tactic:
apply liftOn_condition_of_liftOn'_condition H

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem norm_algebraMap (x : 𝕜) : ‖algebraMap 𝕜 𝕜' x‖ = ‖x‖ * ‖(1 : 𝕜')‖

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖

Tactic:
exact norm_smul _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
-- Mathlib/SetTheory/Surreal/Basic.lean
lemma zero_def : 0 = mk 0 numeric_zero

Proof state:
⊢ 0 = mk 0 numeric_zero

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem CauchySeq.tendsto_uniformity [Preorder β] {u : β → α} (h : CauchySeq u) :
    Tendsto (Prod.map u u) atTop (𝓤 α)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod {m : Fin n → 𝕜} :
    (iteratedFDeriv 𝕜 n f x : (Fin n → 𝕜) → F) m = (∏ i, m i) • iteratedDeriv n f x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDeriv 𝕜 n f x) m = (iteratedFDeriv 𝕜 n f x) fun i => m i • 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv n f x

Tactic:
rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDeriv 𝕜 n f x) m = (iteratedFDeriv 𝕜 n f x) fun i => m i • 1
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem isOrdered_iff [@TransCmp α cmp] {t : RBNode α} :
    isOrdered cmp t ↔ Ordered cmp t

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBNode α
⊢ isOrdered cmp t = true ↔ Ordered cmp t

Tactic:
simp [isOrdered_iff']

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem mem_unique {s : Computation α} {a b : α} : a ∈ s → b ∈ s → a = b
  | ⟨m, ha⟩, ⟨n, hb⟩ => by
    injection
      (le_stable s (le_max_left m n) ha.symm).symm.trans (le_stable s (le_max_right m n) hb.symm)

Proof state:
α : Type u
s : Computation α
a b : α
m : ℕ
ha : (fun b => some a = b) ((↑s).get m)
n : ℕ
hb : (fun b_1 => some b = b_1) ((↑s).get n)
⊢ a = b

Tactic:
injection
  (le_stable s (le_max_left m n) ha.symm).symm.trans (le_stable s (le_max_right m n) hb.symm)

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (map f) (destruct s))

Proof state:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ (map f s).destruct = lmap f (rmap (map f) s.destruct)

Tactic:
apply s.recOn <;> intro <;> simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma exists_of_eq {a b : R} (h : algebraMap R S a = algebraMap R S b) :
    ∃ (n : ℕ), x ^ n * a = x ^ n * b

Proof state:
case intro.mk.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hx : ↑⟨(fun x_1 => x ^ x_1) n, ⋯⟩ * a = ↑⟨(fun x_1 => x ^ x_1) n, ⋯⟩ * b
⊢ ∃ n, x ^ n * a = x ^ n * b

Tactic:
use n

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, x ^ n * a = x ^ n * b

Tactic:
obtain ⟨⟨-, n, rfl⟩, hx⟩ := IsLocalization.exists_of_eq (M := Submonoid.powers x) h

Result:
case intro.mk.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hx : ↑⟨(fun x_1 => x ^ x_1) n, ⋯⟩ * a = ↑⟨(fun x_1 => x ^ x_1) n, ⋯⟩ * b
⊢ ∃ n, x ^ n * a = x ^ n * b
-- Mathlib/Data/Set/Prod.lean
theorem singleton_prod_singleton : ({a} : Set α) ×ˢ ({b} : Set β) = {(a, b)}

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem dist_map_map_zero_lt : dist (f 0 + g 0) (f (g 0)) < 1

Proof state:
f g : CircleDeg1Lift
⊢ f 0 + g 0 - 1 < f (g 0) ∧ f (g 0) < f 0 + g 0 + 1

Tactic:
exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩

Result:
no goals

Proof state:
f g : CircleDeg1Lift
⊢ dist (f 0 + g 0) (f (g 0)) < 1

Tactic:
rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]

Result:
f g : CircleDeg1Lift
⊢ f 0 + g 0 - 1 < f (g 0) ∧ f (g 0) < f 0 + g 0 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_append_left {s t : List α} (i : Nat) (x : α) (h : i < s.length) :
    (s ++ t).set i x = s.set i x ++ t

Proof state:
α : Type u_1
s t : List α
i : Nat
x : α
h : i < s.length
⊢ (s ++ t).set i x = s.set i x ++ t

Tactic:
simp [set_append, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem mul_div_self_eq_mod_sub_self {x k : Nat} : k * (x / k) = x - (x % k)

Proof state:
x k : Nat
⊢ k * (x / k) = x - x % k

Tactic:
rw [Nat.mul_comm, div_mul_self_eq_mod_sub_self]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem Topology.IsQuotientMap.continuousOn_isOpen_iff {f : α → β} {g : β → γ} (h : IsQuotientMap f)
    {s : Set β} (hs : IsOpen s) : ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen s
⊢ Continuous (s.restrict g ∘ s.restrictPreimage f) ↔ Continuous ((f ⁻¹' s).restrict (g ∘ f))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen s
⊢ ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

Tactic:
simp only [continuousOn_iff_continuous_restrict, (h.restrictPreimage_isOpen hs).continuous_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
h : IsQuotientMap f
s : Set β
hs : IsOpen s
⊢ Continuous (s.restrict g ∘ s.restrictPreimage f) ↔ Continuous ((f ⁻¹' s).restrict (g ∘ f))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_singleton (f : α → Array β) (x : α) : #[x].flatMap f = f x

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
x : α
⊢ flatMap f #[x] = f x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem range_pair_subset (f : α → β) (g : α → γ) :
    (range fun x => (f x, g x)) ⊆ range f ×ˢ range g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ (range fun x => (f x, g x)) ⊆ range f ×ˢ range g

Tactic:
rw [this, ← range_prod_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ range (Prod.map f g ∘ fun x => (x, x)) ⊆ range (Prod.map f g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
⊢ (range fun x => (f x, g x)) ⊆ range f ×ˢ range g

Tactic:
have : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x) := funext fun x => rfl

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ (range fun x => (f x, g x)) ⊆ range f ×ˢ range g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ range (Prod.map f g ∘ fun x => (x, x)) ⊆ range (Prod.map f g)

Tactic:
apply range_comp_subset_range

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getMsbD_udiv (n d : BitVec w) (hd : 0#w < d)  (i : Nat) :
    (n / d).getMsbD i = (decide (i < w) && (divRec w {n, d} (DivModState.init w)).q.getMsbD i)

Proof state:
w : Nat
n d : BitVec w
hd : 0#w < d
i : Nat
⊢ 0#?m.78228 < ?m.78229

Tactic:
assumption

Result:
no goals

Proof state:
w : Nat
n d : BitVec w
hd : 0#w < d
i : Nat
⊢ (n / d).getMsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getMsbD i)

Tactic:
simp [getMsbD_eq_getLsbD, getLsbD_udiv, udiv_eq_divRec (by assumption)]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma pairingIn_pairingIn_mem_set_of_isCrystallographic :
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
      ({(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3),
        (-3, -1), (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Set (ℤ × ℤ))

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
⊢ (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
refine (Int.mul_mem_zero_one_two_three_four_iff ?_).mp
  (P.coxeterWeightIn_mem_set_of_isCrystallographic i j)

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
⊢ P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
this : Fintype ι
⊢ P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0

Tactic:
simpa [← P.algebraMap_pairingIn ℤ] using pairing_zero_iff (P.posRootForm ℤ) i j

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
⊢ P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0

Tactic:
have : Fintype ι := Fintype.ofFinite ι

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : P.IsCrystallographic
i j : ι
inst✝ : NoZeroDivisors R
this : Fintype ι
⊢ P.pairingIn ℤ i j = 0 ↔ P.pairingIn ℤ j i = 0
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem continuousAt_extChartAt' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    ContinuousAt (extChartAt I x) x' :=
  continuousAt_extend _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
⊢ x' ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoTerminal_hom [HasTerminal C] : zeroIsoTerminal.hom = (0 : 0 ⟶ ⊤_ C)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.hom = 0

Tactic:
ext

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma latticeClosure_singleton (a : α) : latticeClosure {a} = {a}

Proof state:
α : Type u_3
inst✝ : Lattice α
a : α
⊢ latticeClosure {a} = {a}

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem compl_mem_coprod {s : Set (α × β)} {la : Filter α} {lb : Filter β} :
    sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Proof state:
α : Type u_1
β : Type u_2
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Tactic:
simp only [Filter.coprod, mem_sup, compl_mem_comap]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_inter_product [DecidableEq α] [DecidableEq β] :
    s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Proof state:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t' ↔ (x, y) ∈ (s ∩ s') ×ˢ (t ∩ t')

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ∩ s' ×ˢ t' ↔ (x, y) ∈ (s ∩ s') ×ˢ (t ∩ t')

Tactic:
simp only [and_assoc, and_left_comm, mem_inter, mem_product]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_ex (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α (k + 1)) :
    φ.ex.relabel g = (φ.relabel g).ex

Proof state:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ relabel g φ.ex = (relabel g φ).ex

Tactic:
simp [BoundedFormula.ex]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem fg_iSup {ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ i, (S i).FG) :
    (⨆ i, S i).FG

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (⨆ i, S i).FG

Tactic:
simp_rw [← hs, ← adjoin_iUnion]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (adjoin F (⋃ i, ↑(s i))).FG

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (adjoin F (⋃ i, ↑(s i))).FG

Tactic:
exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
h : ∀ (i : ι), (S i).FG
⊢ (⨆ i, S i).FG

Tactic:
choose s hs using h

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Sort u_3
inst✝ : Finite ι
S : ι → IntermediateField F E
s : ι → Finset E
hs : ∀ (i : ι), adjoin F ↑(s i) = S i
⊢ (⨆ i, S i).FG
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isLittleO_pow_exp_pos_mul_atTop (k : ℕ) {b : ℝ} (hb : 0 < b) :
    (fun x : ℝ => x ^ k) =o[atTop] fun x => exp (b * x)

Proof state:
k : ℕ
b : ℝ
hb : 0 < b
⊢ (fun x => x ^ k) =o[atTop] fun x => rexp (b * x)

Tactic:
simpa using isLittleO_zpow_exp_pos_mul_atTop k hb

Result:
no goals
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_card_fiber_lt_of_card_lt_nsmul (ht : #s < #t • b) :
    ∃ y ∈ t, #{x ∈ s | f x = y} < b

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : ↑(#s) < #t • b
⊢ ∃ y ∈ t, ↑(#(filter (fun x => f x = y) s)) < b

Tactic:
simp_rw [cast_card] at ht ⊢

Result:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : ∑ x ∈ s, 1 < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ filter (fun x => f x = y) s, 1 < b

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : ∑ x ∈ s, 1 < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ filter (fun x => f x = y) s, 1 < b

Tactic:
exact
  exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
    (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma RightHomologyData.opcyclesIso_inv_comp_descOpcycles :
    h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk

Tactic:
simp only [← cancel_epi h.p, p_comp_opcyclesIso_inv_assoc, p_descOpcycles, p_descQ]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem monotoneOn (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) :
    MonotoneOn (variationOnFromTo f s a) s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
⊢ MonotoneOn (variationOnFromTo f s a) s

Tactic:
rintro b bs c cs bc

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a c

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
exact le_add_of_nonneg_right (variationOnFromTo.nonneg_of_le f s bc)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a c

Tactic:
rw [← variationOnFromTo.add hf as bs cs]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c