harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_eq_zero_iff [IsReduced R] : W.j = 0 ↔ W.c₄ = 0

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : IsReduced R
⊢ W.j = 0 ↔ W.c₄ = 0

Tactic:
rw [j_eq_zero_iff', IsReduced.pow_eq_zero_iff three_ne_zero]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_overlap_pf_zero (x : R) (e) :
    IsNat (a + b) (nat_lit 0) → IsNat (x ^ e * a + x ^ e * b) (nat_lit 0)
  | ⟨h⟩ => ⟨by simp [h, ← mul_add]⟩

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
h : a + b = ↑0
⊢ x ^ e * a + x ^ e * b = ↑0

Tactic:
simp [h, ← mul_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.or_false (b : Bool) : (b || false) = b

Proof state:
b : Bool
⊢ (b || false) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_symm_map (e : α ≃ᵐ β) : (μ.map e).map e.symm = μ

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ map (⇑e.symm) (map (⇑e) μ) = μ

Tactic:
simp [map_map e.symm.measurable e.measurable]

Result:
no goals
-- Mathlib/Data/Finsupp/Fintype.lean
@[simp] lemma Fintype.card_finsupp : card (ι →₀ α) = card α ^ card ι

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
inst✝¹ : Zero α
inst✝ : Fintype α
⊢ card (ι →₀ α) = card α ^ card ι

Tactic:
simp [card_congr Finsupp.equivFunOnFinite]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mul_right_apply_of_ne (i : m) (j : n) (a : l) (b : n) (hbj : b ≠ j) (M : Matrix l m α) :
    (M * stdBasisMatrix i j c) a b = 0

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
b : n
hbj : b ≠ j
M : Matrix l m α
⊢ (M * stdBasisMatrix i j c) a b = 0

Tactic:
simp [mul_apply, hbj.symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.and_mem {l : List α} :
    Pairwise R l ↔ Pairwise (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l :=
  Pairwise.iff_of_mem <| by simp +contextual

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_finset_sum {ι} {s : Finset ι} {f : ι → ℝ → E}
    (h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) :
    ∫ x in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ x in a..b, f i x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
ι : Type u_6
s : Finset ι
f : ι → ℝ → E
h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b
⊢ ∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_finset_sum s fun i hi => (h i hi).def',
  Finset.smul_sum]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem right_mem_Ico : b ∈ Ico a b ↔ False

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ b ∈ Ico a b ↔ False

Tactic:
simp [lt_irrefl]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_pow (f : R → R) (n : ℕ) (a : A)
    (hf : ContinuousOn f ((· ^ n) '' (spectrum R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : R → R
n : ℕ
a : A
hf : autoParam (ContinuousOn f ((fun x => x ^ n) '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (x ^ n)) a = cfc f (a ^ n)

Tactic:
rw [cfc_comp' .., cfc_pow_id ..]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDeriv_comp (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x)
    {i : ℕ} (hi : i ≤ n) :
    iteratedFDeriv 𝕜 i (g ∘ f) x =
      (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
x : E
n : WithTop ℕ∞
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (g ∘ f) x = (ftaylorSeries 𝕜 g (f x)).taylorComp (ftaylorSeries 𝕜 f x) i

Tactic:
simp only [← iteratedFDerivWithin_univ, ← ftaylorSeriesWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
x : E
n : WithTop ℕ∞
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (g ∘ f) univ x =
    (ftaylorSeriesWithin 𝕜 g univ (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f univ x) i

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
x : E
n : WithTop ℕ∞
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (g ∘ f) univ x =
    (ftaylorSeriesWithin 𝕜 g univ (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f univ x) i

Tactic:
exact iteratedFDerivWithin_comp hg.contDiffWithinAt hf.contDiffWithinAt
  uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) (mapsTo_univ _ _) hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p → List α} :
    (x ∈ if h : p then [] else l h) ↔ ∃ h : ¬ p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : ¬p → List α
⊢ (x ∈ if h : p then [] else l h) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_eq_fract_mul (b : α) : toIcoMod hp 0 b = Int.fract (b / p) * p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b = Int.fract (b / p) * p

Tactic:
simp [toIcoMod_eq_add_fract_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem Parallel.refl (s : AffineSubspace k P) : s ∥ s :=
  ⟨0, by simp⟩

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ s = map (↑(constVAdd k P 0)) s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_ofBool (b : Bool) : (ofBool b).msb = b

Proof state:
b : Bool
⊢ (ofBool b).msb = b

Tactic:
cases b <;> simp [BitVec.msb]

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem dvd_choose_pow_iff (hp : Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Proof state:
p n k : ℕ
hp : Prime p
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩ <;> rintro rfl <;>
  simp [hp.ne_one] at h

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_abs : cosh |x| = cosh x

Proof state:
x : ℝ
⊢ cosh |x| = cosh x

Tactic:
cases le_total x 0 <;> simp [*, abs_of_nonneg, abs_of_nonpos]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem inv_eq_symplectic_inv (A : Matrix (l ⊕ l) (l ⊕ l) R) (hA : A ∈ symplecticGroup l R) :
    A⁻¹ = (-J l R) * Aᵀ * J l R :=
  inv_eq_left_inv (by simp only [Matrix.neg_mul, inv_left_mul_aux hA])

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * Aᵀ * J l R * A = 1

Tactic:
simp only [Matrix.neg_mul, inv_left_mul_aux hA]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonneg_of_base_lt_one (hx : 0 < x) (hx' : x ≤ 1) : 0 ≤ logb b x

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1

Tactic:
exact hx'

Result:
no goals

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ 0 ≤ logb b x

Tactic:
rw [logb_nonneg_iff_of_base_lt_one b_pos b_lt_one hx]

Result:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_natCast_mul (x : ℝ≥0) (n : ℕ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ≥0
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_natCast]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_add_mul_left_right (h : IsCoprime x (y + x * z)) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y

Tactic:
rw [isCoprime_comm] at h ⊢

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x

Tactic:
exact h.of_add_mul_left_left

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindex_apply (i' : ι') : b.reindex e i' = b (e.symm i') :=
  show (b.repr.trans (Finsupp.domLCongr e)).symm (Finsupp.single i' 1) =
    b.repr.symm (Finsupp.single (e.symm i') 1)
  by rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
⊢ (b.repr ≪≫ₗ Finsupp.domLCongr e).symm (single i' 1) = b.repr.symm (single (e.symm i') 1)

Tactic:
rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_eq_one_of_le (h : B ≤ A) : relrank A B = 1

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : B ≤ A
⊢ A.relrank B = 1

Tactic:
rw [← inf_relrank_right, inf_eq_right.2 h, relrank_self]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem Filter.HasBasis.uniformContinuousOn_iff {ι'} [UniformSpace β] {p : ι → Prop}
    {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}
    (hb : (𝓤 β).HasBasis q t) {f : α → β} {S : Set α} :
    UniformContinuousOn f S ↔
      ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i :=
  ((ha.inf_principal (S ×ˢ S)).tendsto_iff hb).trans <| by
    simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
ι' : Sort u_2
inst✝ : UniformSpace β
p : ι → Prop
s : ι → Set (α × α)
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ x ∈ s ia ∩ S ×ˢ S, (f x.1, f x.2) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
theorem isUniformEmbedding_translate_mul (a : α) : IsUniformEmbedding fun x : α => x * a :=
  { comap_uniformity

Proof state:
case mk.mk
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ (fun x => (x.1 * a, x.2 * a)) (p₁, p₂) = (fun x => (x.1 * a, x.2 * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)

Tactic:
simp only [Prod.mk.injEq, mul_left_inj, imp_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.1 * a, x.2 * a)

Tactic:
rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩

Result:
case mk.mk
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ (fun x => (x.1 * a, x.2 * a)) (p₁, p₂) = (fun x => (x.1 * a, x.2 * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ comap (fun x => (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α

Tactic:
nth_rw 1 [← uniformity_translate_mul a, comap_map]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
a : α
⊢ Function.Injective fun x => (x.1 * a, x.2 * a)
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (Metric.ball a r)

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : E
r : ℝ
⊢ Convex ℝ (ball a r)

Tactic:
simpa only [Metric.ball, sep_univ] using (convexOn_univ_dist a).convex_lt r

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_apply_ne_zero {a x : α} {b : M} : single a b x ≠ 0 ↔ x = a ∧ b ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a x : α
b : M
⊢ (single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/TensorProduct.lean
theorem liftLie_apply (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N) :
    liftLie R L M N P f (m ⊗ₜ n) = f m n

Proof state:
R : Type u
inst✝¹⁴ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : LieRingModule L M
inst✝⁸ : LieModule R L M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : LieRingModule L N
inst✝⁴ : LieModule R L N
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : LieRingModule L P
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
m : M
n : N
⊢ ((liftLie R L M N P) f) (m ⊗ₜ[R] n) = (f m) n

Tactic:
simp only [coe_liftLie_eq_lift_coe, LieModuleHom.coe_toLinearMap, lift_apply]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem not_ex_isAtomic (φ : L.BoundedFormula α (n + 1)) : ¬φ.ex.IsAtomic := fun con => by cases con

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃'φ).IsAtomic
⊢ False

Tactic:
cases con

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.eventually_mul_div_cancel (h : IsBigOWith c l u v) : u / v * v =ᶠ[l] u :=
  Eventually.mono h.bound fun y hy => div_mul_cancel_of_imp fun hv => by simpa [hv] using hy

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
h : IsBigOWith c l u v
y : α
hy : ‖u y‖ ≤ c * ‖v y‖
hv : v y = 0
⊢ u y = 0

Tactic:
simpa [hv] using hy

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kerase_cons_ne {a} {s : Sigma β} {l : List (Sigma β)} (h : a ≠ s.1) :
    kerase a (s :: l) = s :: kerase a l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l : List (Sigma β)
h : a ≠ s.fst
⊢ kerase a (s :: l) = s :: kerase a l

Tactic:
simp [kerase, h]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso (e : J ≃o J') :
    W.IsStableUnderTransfiniteCompositionOfShape J ↔
      W.IsStableUnderTransfiniteCompositionOfShape J'

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
e : J ≃o J'
⊢ W.IsStableUnderTransfiniteCompositionOfShape J ↔ W.IsStableUnderTransfiniteCompositionOfShape J'

Tactic:
simp only [isStableUnderTransfiniteCompositionOfShape_iff,
  W.transfiniteCompositionsOfShape_eq_of_orderIso e]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
    rank (f.comp g) ≤ min (rank f) (rank g)

Proof state:
K : Type u
V : Type v
V' V'₁ : Type v'
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V'₁
inst✝ : Module K V'₁
g : V →ₗ[K] V'
f : V' →ₗ[K] V'₁
⊢ (f ∘ₗ g).rank ≤ f.rank ⊓ g.rank

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_comp_le g f

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma orbitRel.Quotient.subgroup_quotient_eq_iff {H : Subgroup G} {x : orbitRel.Quotient G α}
    {a b : x.orbit} : (⟦a⟧ : orbitRel.Quotient H x.orbit) = ⟦b⟧ ↔
      (⟦↑a⟧ : orbitRel.Quotient H α) = ⟦↑b⟧

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ (orbitRel ↥H ↑x.orbit) a b ↔ (orbitRel (↥H) α) ↑a ↑b

Tactic:
exact orbitRel.Quotient.mem_subgroup_orbit_iff.symm

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

Tactic:
simp_rw [← @Quotient.mk''_eq_mk, Quotient.eq'']

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ (orbitRel ↥H ↑x.orbit) a b ↔ (orbitRel (↥H) α) ↑a ↑b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)}
    (h : Perm l' l) : DistinctKeys l → DistinctKeys l' :=
  DistinctKeys.perm_keys (by simpa only [keys_eq_map] using h.map _)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
h : l'.Perm l
⊢ (keys l').Perm (keys l)

Tactic:
simpa only [keys_eq_map] using h.map _

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_singleton {r : S} :
    spanNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
  le_antisymm
    (span_le.mpr fun x hx =>
      mem_span_singleton.mpr
        (by
          obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
          exact map_dvd _ (mem_span_singleton.mp hx')))
    ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanNorm _ (mem_span_singleton_self _)))

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
r : S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ x

Tactic:
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx

Result:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x

Proof state:
case intro.intro
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x

Tactic:
exact map_dvd _ (mem_span_singleton.mp hx')

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.symm (H : IsCoprime x y) : IsCoprime y x :=
  let ⟨a, b, H⟩ := H
  ⟨b, a, by rw [add_comm, H]⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
H✝ : IsCoprime x y
a b : R
H : a * x + b * y = 1
⊢ b * y + a * x = 1

Tactic:
rw [add_comm, H]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_one : ∫⁻ _, (1 : ℝ≥0∞) ∂μ = μ univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 1 ∂μ = μ univ

Tactic:
rw [lintegral_const, one_mul]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem Term.realize_le {t₁ t₂ : L.Term (α ⊕ (Fin n))} {v : α → M}
    {xs : Fin n → M} :
    (t₁.le t₂).Realize v xs ↔ t₁.realize (Sum.elim v xs) ≤ t₂.realize (Sum.elim v xs)

Proof state:
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
t₁ t₂ : L.Term (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.le t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂

Tactic:
simp [Term.le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_lt_add_left {a b : Int} (h : a < b) (c : Int) : c + a < c + b :=
  Int.lt_iff_le_and_ne.2 ⟨Int.add_le_add_left (Int.le_of_lt h) _, fun heq =>
    b.lt_irrefl <| by rwa [Int.add_left_cancel heq] at h⟩

Proof state:
a b : Int
h : a < b
c : Int
heq : c + a = c + b
⊢ b < b

Tactic:
rwa [Int.add_left_cancel heq] at h

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem tendsto_of_ne_zero {γ : Γ₀} (h : γ ≠ 0) : Tendsto f l (𝓝 γ) ↔ ∀ᶠ x in l, f x = γ

Proof state:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ

Tactic:
rw [nhds_of_ne_zero h, tendsto_pure]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_add (a b : R[X]) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
rw [← ofFinsupp_add]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a b : R[X]
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Tactic:
cases a

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
b : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
b : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp

Tactic:
cases b

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.precompose_isIso_iff {F G : J ⥤ C} (α : F ⟶ G) [IsIso α]
    {c : Cocone G} : IsVanKampenColimit ((Cocones.precompose α).obj c) ↔ IsVanKampenColimit c :=
  ⟨fun hc ↦ IsVanKampenColimit.of_iso (IsVanKampenColimit.precompose_isIso (inv α) hc)
    (Cocones.ext (Iso.refl _) (by simp)),
    IsVanKampenColimit.precompose_isIso α⟩

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit ((Cocones.precompose α).obj c)
⊢ ∀ (j : J),
    ((Cocones.precompose (inv α)).obj ((Cocones.precompose α).obj c)).ι.app j ≫
        (Iso.refl ((Cocones.precompose (inv α)).obj ((Cocones.precompose α).obj c)).pt).hom =
      c.ι.app j

Tactic:
simp

Result:
no goals