harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) : ((replicate n a).find? p).get h = a

Proof state:
case zero
α : Type u_1
a : α
p : α → Bool
h : (find? p (replicate 0 a)).isSome = true
⊢ (find? p (replicate 0 a)).get h = a

Tactic:
simp at h

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
h : (find? p (replicate (n + 1) a)).isSome = true
⊢ (find? p (replicate (n + 1) a)).get h = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
h : (find? p (replicate n a)).isSome = true
⊢ (find? p (replicate n a)).get h = a

Tactic:
cases n with
| zero => simp at h
| succ n => simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma coe_add_eq_bot_iff : a + y = ⊥ ↔ y = ⊥

Proof state:
α : Type u
inst✝ : Add α
y : WithBot α
a : α
⊢ ↑a + y = ⊥ ↔ y = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem EventuallyLE.sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
    (hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Proof state:
α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Tactic:
filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem LinearIsometry.orthonormal_comp_iff {v : ι → E} (f : E →ₗᵢ[𝕜] E') :
    Orthonormal 𝕜 (f ∘ v) ↔ Orthonormal 𝕜 v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v

Tactic:
simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v

Tactic:
classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Pow.lean
theorem Prime.pow_minFac {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) : (p ^ k).minFac = p

Proof state:
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ (p ^ k).minFac = p

Tactic:
rw [Nat.pow_minFac hk, hp.minFac_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma lift_snd :
    (Cochain.ofHom (lift φ α β eq)).comp (snd φ) (zero_add 0) = β

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
⊢ (Cochain.ofHom (lift φ α β eq)).comp (snd φ) ⋯ = β

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem finset_sum_apply' (I : Finset ι) (κ : ι → Kernel α β) (a : α) (s : Set β) :
    (∑ i ∈ I, κ i) a s = ∑ i ∈ I, κ i a s

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
⊢ ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s

Tactic:
rw [finset_sum_apply, Measure.finset_sum_apply]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem normalize_lcm : normalize (s.lcm f) = s.lcm f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ normalize (s.lcm f) = s.lcm f

Tactic:
simp [lcm_def]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem self_mul_sign (x : α) : x * sign x = |x|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x : α
⊢ x * ↑(sign x) = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_of_isZero_X₂ (h : IsZero S.X₂) : S.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ S.Exact

Tactic:
rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem X_pow_eq_monomial : X n ^ e = monomial (Finsupp.single n e) (1 : R)

Proof state:
R : Type u
σ : Type u_1
e : ℕ
n : σ
inst✝ : CommSemiring R
⊢ X n ^ e = (monomial (Finsupp.single n e)) 1

Tactic:
simp [X, monomial_pow]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem pred : Nat.Primrec pred :=
  (casesOn1 0 Primrec.id).of_eq fun n => by cases n <;> simp [*]

Proof state:
n : ℕ
⊢ Nat.casesOn n 0 id = n.pred

Tactic:
cases n <;> simp [*]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem coe_pow : ∀ n : ℕ, ⇑(f ^ n) = f^[n]
  | 0 => rfl
  | n + 1 => by
    ext x
    simp [coe_pow n, pow_succ]

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ ⇑(f ^ (n + 1)) = (⇑f)^[n + 1]

Tactic:
ext x

Result:
case h
f : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ (f ^ (n + 1)) x = (⇑f)^[n + 1] x

Proof state:
case h
f : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ (f ^ (n + 1)) x = (⇑f)^[n + 1] x

Tactic:
simp [coe_pow n, pow_succ]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/WeakDual.lean
theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)

Tactic:
simp only [polar_def, setOf_forall]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ i ∈ s, {x | ‖x i‖ ≤ 1})

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ i ∈ s, {x | ‖x i‖ ≤ 1})

Tactic:
exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast?

Proof state:
α : Type u_1
l l' : List α
⊢ (l ++ l').getLast? = l'.getLast?.or l.getLast?

Tactic:
simp [← head?_reverse]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem add_dotProduct : (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

Tactic:
simp [dotProduct, add_mul, Finset.sum_add_distrib]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_fun' : Module.rank R (η → R) = Fintype.card η

Proof state:
R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ Module.rank R (η → R) = ↑(Fintype.card η)

Tactic:
rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem _root_.Function.LeftInverse.filter_map {f : α → β} {g : β → α} (hfg : LeftInverse g f) :
    LeftInverse (map g) (map f) := fun F ↦ by
  rw [map_map, hfg.comp_eq_id, map_id]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ map g (map f F) = F

Tactic:
rw [map_map, hfg.comp_eq_id, map_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ Ioc (-(π / 2)) (π / 2)) :
    x ≤ arcsin y ↔ sin x ≤ y

Proof state:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩,
  sin_neg, neg_le_neg_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_mirror : p.mirror.mirror = p :=
  Polynomial.ext fun n => by
    rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.mirror.mirror.coeff n = p.coeff n

Tactic:
rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]

Result:
no goals
-- Mathlib/Algebra/Group/Prod.lean
theorem mk_one_mul_mk_one [Mul M] [Monoid N] (a₁ a₂ : M) :
    (a₁, (1 : N)) * (a₂, 1) = (a₁ * a₂, 1)

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : Monoid N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

Tactic:
rw [mk_mul_mk, mul_one]

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma comp_apply {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : M) :
    (f ≫ g) x = g (f x)

Proof state:
M N T : CommMonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_isHomogeneous (M : Matrix m n R) (i : m) :
    (M.toMvPolynomial i).IsHomogeneous 1

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ (M.toMvPolynomial i).IsHomogeneous 1

Tactic:
apply MvPolynomial.IsHomogeneous.sum

Result:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ ∀ i_1 ∈ Finset.univ, ((monomial (Finsupp.single i_1 1)) (M i i_1)).IsHomogeneous 1

Proof state:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ ∀ i_1 ∈ Finset.univ, ((monomial (Finsupp.single i_1 1)) (M i i_1)).IsHomogeneous 1

Tactic:
rintro j -

Result:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ ((monomial (Finsupp.single j 1)) (M i j)).IsHomogeneous 1

Proof state:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ ((monomial (Finsupp.single j 1)) (M i j)).IsHomogeneous 1

Tactic:
apply MvPolynomial.isHomogeneous_monomial _ _

Result:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ (Finsupp.single j 1).degree = 1

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ (Finsupp.single j 1).degree = 1

Tactic:
simp [Finsupp.degree, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton,
  Finsupp.single_eq_same]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
protected lemma fg {S : Submodule R M} (h : S.IsPrincipal) : S.FG :=
  ⟨{h.generator}, by simp only [Finset.coe_singleton, span_singleton_generator]⟩

Proof state:
R : Type u
M : Type v
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
S : Submodule R M
h : S.IsPrincipal
⊢ span R ↑{generator S} = S

Tactic:
simp only [Finset.coe_singleton, span_singleton_generator]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_nil {u u' : U} (hu : u = u') : (Path.nil : Path u u).cast hu hu = Path.nil

Proof state:
U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast ⋯ ⋯ nil = nil

Proof state:
U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast ⋯ ⋯ nil = nil

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma measurable_singularPart_fun (κ η : Kernel α γ) :
    Measurable (fun p : α × γ ↦ Real.toNNReal (rnDerivAux κ (κ + η) p.1 p.2)
      - Real.toNNReal (1 - rnDerivAux κ (κ + η) p.1 p.2) * rnDeriv κ η p.1 p.2)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p =>
    ↑(κ.rnDerivAux (κ + η) p.1 p.2).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) p.1 p.2).toNNReal * κ.rnDeriv η p.1 p.2

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_shiftRightConst : eval (shiftRightConst n) = ((· >>> n) : BitVec w → BitVec w)

Proof state:
n w : Nat
⊢ (shiftRightConst n).eval = fun x => x >>> n

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_left :
    a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
  calc
    a ∆ b ∆ c = a ∆ b \ c ⊔ c \ a ∆ b := symmDiff_def _ _
    _ = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)

Tactic:
rw [sdiff_symmDiff', sup_comm (c ⊓ a ⊓ b), symmDiff_sdiff]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem separatingRight_iff_flip_ker_eq_bot {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.SeparatingRight ↔ LinearMap.ker B.flip = ⊥

Proof state:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingRight ↔ ker B.flip = ⊥

Tactic:
rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_div_const_iff (h : a ≠ 0) : (Summable fun i ↦ f i / a) ↔ Summable f

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ (Summable fun i => f i / a) ↔ Summable f

Tactic:
simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem fiber_ncard_ne_zero_iff_mem_image {y : β} (hs : s.Finite

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
z : α
hz : z ∈ s
⊢ {x | x ∈ s ∧ f x = f z}.ncard ≠ 0

Tactic:
exact @ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl)
  (hs.subset (sep_subset _ _))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : autoParam s.Finite _auto✝
⊢ {x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s

Tactic:
refine ⟨nonempty_of_ncard_ne_zero, ?_⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : autoParam s.Finite _auto✝
⊢ y ∈ f '' s → {x | x ∈ s ∧ f x = y}.ncard ≠ 0

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : autoParam s.Finite _auto✝
⊢ y ∈ f '' s → {x | x ∈ s ∧ f x = y}.ncard ≠ 0

Tactic:
rintro ⟨z, hz, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : autoParam s.Finite _auto✝
z : α
hz : z ∈ s
⊢ {x | x ∈ s ∧ f x = f z}.ncard ≠ 0
-- Mathlib/Topology/Constructions.lean
@[simp] lemma IsOpen.inter_preimage_val_iff {s t : Set X} (hs : IsOpen s) :
    IsOpen (s ↓∩ t) ↔ IsOpen (s ∩ t) :=
  ⟨fun h ↦ by simpa using hs.isOpenMap_subtype_val _ h,
    fun h ↦ (Subtype.preimage_coe_self_inter _ _).symm ▸ h.preimage_val⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsOpen s
h : IsOpen (s ↓∩ t)
⊢ IsOpen (s ∩ t)

Tactic:
simpa using hs.isOpenMap_subtype_val _ h

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem inv_mul {z : ℤ_[p]} (hz : ‖z‖ = 1) : z.inv * z = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
hz : ‖z‖ = 1
⊢ z.inv * z = 1

Tactic:
rw [mul_comm, mul_inv hz]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem coe_map (f : α ↪ β) (s : Finset α) : (s.map f : Set β) = f '' s :=
  Set.ext (by simp only [mem_coe, mem_map, Set.mem_image, implies_true])

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ∀ (x : β), x ∈ ↑(map f s) ↔ x ∈ ⇑f '' ↑s

Tactic:
simp only [mem_coe, mem_map, Set.mem_image, implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_mapFinIdx {l : Array α}
    {f : (i : Nat) → α → (h : i < l.size) → β}
    {g : (i : Nat) → β → (h : i < (l.mapFinIdx f).size) → γ} :
    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) (by simpa using h))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Array α
f : (i : Nat) → α → i < l.size → β
g : (i : Nat) → β → i < (l.mapFinIdx f).size → γ
⊢ (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun i a h => g i (f i a h) ⋯

Tactic:
simp [mapFinIdx_eq_iff]

Result:
no goals

Proof state:
α : Type ?u.101216
β : Type ?u.101244
γ : Type ?u.101290
l : Array α
f : (i : Nat) → α → i < l.size → β
g : (i : Nat) → β → i < (l.mapFinIdx f).size → γ
i : Nat
a : α
h : i < l.size
⊢ i < (l.mapFinIdx f).size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem map_injective (hf : Function.Injective f) : Function.Injective (map f) := fun p q h =>
  ext fun m => hf <| by rw [← coeff_map f, ← coeff_map f, h]

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
h : map f p = map f q
m : ℕ
⊢ f (p.coeff m) = f (q.coeff m)

Tactic:
rw [← coeff_map f, ← coeff_map f, h]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support fun i => f i

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f = mk f.support fun i => f ↑i

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem mul_star_self_eq_zero_iff (x : E) : x * x⋆ = 0 ↔ x = 0

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x * x⋆ = 0 ↔ x = 0

Tactic:
simpa only [star_eq_zero, star_star] using @star_mul_self_eq_zero_iff _ _ _ _ (star x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_else_false {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ h : p, x h

Proof state:
p : Prop
inst✝ : Decidable p
x : p → Prop
⊢ (if h : p then x h else False) ↔ ∃ h, x h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k : α}
    {v : β} : get! (m.insert k v) k = v

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
k : α
v : β
⊢ get! (m.insert k v) k = v

Tactic:
simp_to_model [insert] using List.getValue!_insertEntry_self

Result:
no goals
-- Mathlib/Algebra/CharP/Algebra.lean
lemma RingHom.charP_iff_charP {K L : Type*} [DivisionRing K] [Semiring L] [Nontrivial L]
    (f : K →+* L) (p : ℕ) : CharP K p ↔ CharP L p

Proof state:
K : Type u_1
L : Type u_2
inst✝² : DivisionRing K
inst✝¹ : Semiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p

Tactic:
simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sInf_emptyset [Inhabited s] :
    sInf (∅ : Set s) = default

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
⊢ sInf ∅ = default

Tactic:
simp [sInf]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_eq_iff_natTrailingDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : n ≠ 0) :
    p.trailingDegree = n ↔ p.natTrailingDegree = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
rw [natTrailingDegree, ENat.toNat_eq_iff hn]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.exists_nat_pow_eq [Finite α] (h : SameCycle f x y) :
    ∃ i : ℕ, (f ^ i) x = y

Proof state:
case intro.intro
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
left✝ : i < orderOf f
hi : (f ^ i) x = y
⊢ ∃ i, (f ^ i) x = y

Tactic:
exact ⟨i, hi⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ i) x = y

Tactic:
obtain ⟨i, _, hi⟩ := h.exists_pow_eq'

Result:
case intro.intro
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
left✝ : i < orderOf f
hi : (f ^ i) x = y
⊢ ∃ i, (f ^ i) x = y
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_self (P : Fin 3 → R) : W'.addY P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addY P P = 0

Tactic:
simp only [addY, negY_eq, negAddY_self, addX_self, addZ_self, neg_zero, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
lemma add_sq' (a b : α) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Proof state:
α : Type u
inst✝ : CommSemiring α
a b : α
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

Tactic:
rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem prod_le_prod_iff : s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤ :=
  prod_subset_prod_iff.trans <| by simp

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ ↑s₂ ⊆ ↑s₁ ∧ ↑t₂ ⊆ ↑t₁ ∨ ↑s₂ = ∅ ∨ ↑t₂ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma exterior_singleton_subset_iff_mem_nhds : exterior {a} ⊆ t ↔ t ∈ 𝓝 a

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
t : Set α
a : α
⊢ exterior {a} ⊆ t ↔ t ∈ 𝓝 a

Tactic:
simp [exterior_subset_iff_mem_nhdsSet]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem Ioc_disjoint_Ioc : Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Proof state:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ a₂ ⊓ b₂ ≤ a₁ ⊔ b₁

Tactic:
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico

Result:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : Disjoint (Ico (toDual a₂) (toDual a₁)) (Ico (toDual b₂) (toDual b₁)) ↔ toDual a₁ ⊓ toDual b₁ ≤ toDual a₂ ⊔ toDual b₂
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ a₂ ⊓ b₂ ≤ a₁ ⊔ b₁

Proof state:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : Disjoint (Ico (toDual a₂) (toDual a₁)) (Ico (toDual b₂) (toDual b₁)) ↔ toDual a₁ ⊓ toDual b₁ ≤ toDual a₂ ⊔ toDual b₂
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ a₂ ⊓ b₂ ≤ a₁ ⊔ b₁

Tactic:
simpa only [dual_Ico] using h

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem xor_iff_ne : ∀ {x y : Bool}, xor x y = true ↔ x ≠ y

Proof state:
⊢ ∀ {x y : Bool}, (x ^^ y) = true ↔ x ≠ y

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem relNorm_top : relNorm R (⊤ : Ideal S) = ⊤

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)
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
⊢ (relNorm R) ⊤ = ⊤

Tactic:
simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)

Result:
no goals