harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem dite_tensor {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z))
    (g' : ¬P → (Y ⟶ Z)) : (if h : P then g h else g' h) ⊗ f =
    if h : P then g h ⊗ f else g' h ⊗ f

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (if h : P then g h else g' h) ⊗ f = if h : P then g h ⊗ f else g' h ⊗ f

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_smul_right (x y : F) {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ ⟪x, r • y⟫_𝕜 = r * ⟪x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_smul_left]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ (starRingEnd 𝕜) ((starRingEnd 𝕜) r * ⟪y, x⟫_𝕜) = r * ⟪x, y⟫_𝕜

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ (starRingEnd 𝕜) ((starRingEnd 𝕜) r * ⟪y, x⟫_𝕜) = r * ⟪x, y⟫_𝕜

Tactic:
simp only [conj_conj, inner_conj_symm, RingHom.map_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
theorem cin_cast {aig1 aig2 : AIG α} (s : FullAdderInput aig1)
    (hcast : aig1.decls.size ≤ aig2.decls.size) :
    (s.cast hcast).cin = s.cin.cast hcast

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).cin = s.cin.cast hcast

Tactic:
simp [cast]

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
lemma isPGroup_multiplicative : IsPGroup n (Multiplicative G)

Proof state:
n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
x✝ : G
⊢ Multiplicative.ofAdd x✝ ^ n ^ 1 = 1

Tactic:
simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]

Result:
no goals

Proof state:
n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
⊢ IsPGroup n (Multiplicative G)

Tactic:
simpa [IsPGroup, Multiplicative.forall] using
  fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem transAt_indep {i} (j) (f g : Ω^ N X x) :
    (⟦transAt i f g⟧ : HomotopyGroup N X x) = ⟦transAt j f g⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦transAt i f g⟧ = ⟦transAt j f g⟧

Tactic:
simp_rw [← fromLoop_trans_toLoop]

Result:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
⊢ ⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f g : ↑(Ω^ N X x)
m : (G : Type ?u.353502) → Group G → G → G → G := fun G x x1 x2 => x1 * x2
⊢ ⟦fromLoop i (Path.trans (toLoop i f) (toLoop i g))⟧ = ⟦fromLoop j (Path.trans (toLoop j f) (toLoop j g))⟧

Tactic:
exact congr_fun₂ (congr_arg (m <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦g⟧ ⟦f⟧

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_coe (x : ℝ) : tan (x : Angle) = Real.tan x

Proof state:
x : ℝ
⊢ (↑x).tan = Real.tan x

Tactic:
rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem as_sum_range_C_mul_X_pow (p : R[X]) :
    p = ∑ i ∈ range (p.natDegree + 1), C (coeff p i) * X ^ i :=
  p.as_sum_range.trans <| by simp only [C_mul_X_pow_eq_monomial]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i) = ∑ i ∈ range (p.natDegree + 1), C (p.coeff i) * X ^ i

Tactic:
simp only [C_mul_X_pow_eq_monomial]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
    aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size

Tactic:
simp only [mkAndCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_forIn' {α : Type uu}
    (as : Array α) (init : β) (f : γ → (a : α) → a ∈ as → β → m (ForInStep β)) (hmono : monotone f) :
    monotone (fun x => forIn' as init (f x))

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : Array α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone fun x => forIn' as init (f x)

Tactic:
apply monotone_forIn'_loop

Result:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : Array α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone f

Proof state:
case hmono
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
β : Type u
γ : Type w
inst✝ : PartialOrder γ
α : Type uu
as : Array α
init : β
f : γ → (a : α) → a ∈ as → β → m (ForInStep β)
hmono : monotone f
⊢ monotone f

Tactic:
apply hmono

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_coe_neg_pi_div_two : (↑(-π / 2) : Angle).sign = -1

Proof state:
⊢ (↑(-π / 2)).sign = -1

Tactic:
rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem C_0 : C (0 : R) = 0

Proof state:
R : Type u
inst✝ : Semiring R
⊢ C 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem ne_one : minpoly G F x ≠ (1 : Polynomial (FixedPoints.subfield G F)) := fun H =>
  have := eval₂ G F x
  (one_ne_zero : (1 : F) ≠ 0) <| by rwa [H, Polynomial.eval₂_one] at this

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
H : minpoly G F x = 1
this : Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0
⊢ 1 = 0

Tactic:
rwa [H, Polynomial.eval₂_one] at this

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_lt_pred : a < b → pred a < pred b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
a✝ : a < b
⊢ pred a < pred b

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ a < b → pred a < pred b

Tactic:
intro

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
a✝ : a < b
⊢ pred a < pred b
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_subgroupOf_eq_of_le {H K : Subgroup G} (h : H ≤ K) :
    (H.subgroupOf K).map K.subtype = H

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
rwa [subgroupOf_map_subtype, inf_eq_left]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem coeff_rename_embDomain (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
    (rename f φ).coeff (d.embDomain f) = φ.coeff d

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (embDomain f d) ((rename ⇑f) φ) = coeff d φ

Tactic:
rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem TransOrd.instLexOrd [Ord α] [Ord β]
    [TransOrd α] [TransOrd β] : @TransOrd (α × β) lexOrd

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : TransOrd α
inst✝ : TransOrd β
⊢ TransOrd (α × β)

Tactic:
rw [TransOrd, lexOrd_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : TransOrd α
inst✝ : TransOrd β
⊢ TransCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Ord α
inst✝² : Ord β
inst✝¹ : TransOrd α
inst✝ : TransOrd β
⊢ TransCmp (compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd))

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepFun_iff_iCondIndep {β : ι → Type*}
    (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepFun m' hm' m f μ
      ↔ iCondIndep m' hm' (fun x ↦ MeasurableSpace.comap (f x) (m x)) μ

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepFun m' hm' m f μ ↔ iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ

Tactic:
simp only [iCondIndepFun, iCondIndep, Kernel.iIndepFun]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_symm_top :
    isIdempotentElemEquivClopens.symm ⊤ = ⟨(1 : R), .one⟩ :=
  isIdempotentElemEquivClopens.symm_apply_eq.mpr <| Clopens.ext <| by
    rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_one]; rfl

Proof state:
R : Type u
inst✝ : CommRing R
⊢ ↑⊤ = ↑⊤

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
⊢ ↑⊤ = ↑(isIdempotentElemEquivClopens ⟨1, ⋯⟩)

Tactic:
rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_one]

Result:
R : Type u
inst✝ : CommRing R
⊢ ↑⊤ = ↑⊤
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_vadd (x : E) : IsVonNBounded 𝕜 (x +ᵥ s) ↔ IsVonNBounded 𝕜 s :=
  ⟨fun h ↦ by simpa using h.vadd (-x), fun h ↦ h.vadd x⟩

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
x : E
h : IsVonNBounded 𝕜 (x +ᵥ s)
⊢ IsVonNBounded 𝕜 s

Tactic:
simpa using h.vadd (-x)

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem piecewise_single_erase (x : Π₀ i, β i) (i : ι)
    [∀ i' : ι, Decidable <| (i' ∈ ({i} : Set ι))] : -- Porting note: added Decidable hypothesis
    (single i (x i)).piecewise (x.erase i) {i} = x

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
⊢ ((single i (x i)).piecewise (erase i x) {i}) j = x j

Tactic:
rw [piecewise_apply]

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
⊢ (if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
⊢ (if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j

Tactic:
split_ifs with h

Result:
case pos
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
h : j ∈ {i}
⊢ (single i (x i)) j = x j

case neg
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
h : j ∈ {i}
⊢ (single i (x i)) j = x j

Tactic:
rw [(id h : j = i), single_eq_same]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
⊢ (single i (x i)).piecewise (erase i x) {i} = x

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
⊢ ((single i (x i)).piecewise (erase i x) {i}) j = x j

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
x : Π₀ (i : ι), β i
i : ι
inst✝ : (i' : ι) → Decidable (i' ∈ {i})
j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j

Tactic:
exact erase_ne h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_pow (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
induction n with
| zero => simp
| succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p ^ 0).natDegree = 0 * p.natDegree

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree

Tactic:
rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_X_zero (p : R[X]) : coeff (p * X) 0 = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p * X).coeff 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_self : canonicalEquiv S P P = RingEquiv.refl _

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)

Tactic:
rw [← canonicalEquiv_trans_canonicalEquiv S P P]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ (canonicalEquiv S P P).trans (canonicalEquiv S P P) = RingEquiv.refl (FractionalIdeal S P)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ (canonicalEquiv S P P).trans (canonicalEquiv S P P) = RingEquiv.refl (FractionalIdeal S P)

Tactic:
convert (canonicalEquiv S P P).symm_trans_self

Result:
case h.e'_2.h.e'_10
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ canonicalEquiv S P P = (canonicalEquiv S P P).symm

Proof state:
case h.e'_2.h.e'_10
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
⊢ canonicalEquiv S P P = (canonicalEquiv S P P).symm

Tactic:
exact (canonicalEquiv_symm S P P).symm

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
lemma two_pow_and (n i : ℕ) : 2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat

Proof state:
n i : ℕ
⊢ 2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat

Tactic:
rw [mul_comm, land_comm, and_two_pow]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem le_nadd_self {a b} : a ≤ b ♯ a

Proof state:
a b : Ordinal.{u_1}
⊢ a ≤ b ♯ a

Tactic:
simpa using nadd_le_nadd_right (Ordinal.zero_le b) a

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp]
lemma krullDim_eq_bot_iff : krullDim α = ⊥ ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ ⊥) ↔ IsEmpty α

Tactic:
simp only [le_bot_iff, WithBot.natCast_ne_bot, isEmpty_iff]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ LTSeries α → False ↔ α → False

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊥ ↔ IsEmpty α

Tactic:
rw [eq_bot_iff, krullDim, iSup_le_iff]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ ⊥) ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Preorder α
H : LTSeries α → False
x : α
⊢ ∀ (i : Fin 0), (fun x_1 => x) i.castSucc < (fun x_1 => x) i.succ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_toMatrix' {ι : Type*} [Fintype ι] [DecidableEq ι] (f : (ι → A) →ₗ[A] ι → A) :
    Matrix.det (LinearMap.toMatrix' f) = LinearMap.det f

Proof state:
A : Type u_5
inst✝² : CommRing A
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (ι → A) →ₗ[A] ι → A
⊢ (toMatrix' f).det = LinearMap.det f

Tactic:
simp [← toMatrix_eq_toMatrix']

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem re_add_im (z : ℂ) : (z.re : ℂ) + z.im * I = z :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
z : ℂ
⊢ (↑z.re + ↑z.im * I).re = z.re ∧ (↑z.re + ↑z.im * I).im = z.im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
    (Const.alter m k f).size =
      if m.contains k && (f (Const.get? m k)).isNone then
        m.size - 1
      else if !m.contains k && (f (Const.get? m k)).isSome then
        m.size + 1
      else
        m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).size =
    if (m.contains k && (f (get? m k)).isNone) = true then m.size - 1
    else if (!m.contains k && (f (get? m k)).isSome) = true then m.size + 1 else m.size

Tactic:
simp_to_raw using Raw₀.Const.size_alter

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem card_eq_card_functions_add_card_relations :
    L.card =
      (Cardinal.sum fun l => Cardinal.lift.{v} #(L.Functions l)) +
        Cardinal.sum fun l => Cardinal.lift.{u} #(L.Relations l)

Proof state:
L : Language
⊢ L.card = (sum fun l => lift.{v, u} #(L.Functions l)) + sum fun l => lift.{u, v} #(L.Relations l)

Tactic:
simp only [card, mk_sum, mk_sigma, lift_sum]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearEquiv.isUnit_det (f : M ≃ₗ[R] M') (v : Basis ι R M) (v' : Basis ι R M') :
    IsUnit (LinearMap.toMatrix v v' f).det

Proof state:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ ?B * (toMatrix v v') ↑f = 1

case B
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R

Tactic:
simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit ((toMatrix v v') ↑f).det

Tactic:
apply isUnit_det_of_left_inverse

Result:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ ?B * (toMatrix v v') ↑f = 1

case B
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
lemma IsMulFreimanHom.congr (hf₁ : IsMulFreimanHom n A B f₁) (h : EqOn f₁ f₂ A) :
    IsMulFreimanHom n A B f₂ where
  mapsTo := hf₁.mapsTo.congr h
  map_prod_eq_map_prod s t hsA htA hs ht h'

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod

Tactic:
rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
  hf₁.map_prod_eq_map_prod hsA htA hs ht h']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem sum_nat_mod (s : Multiset ℕ) (n : ℕ) : s.sum % n = (s.map (· % n)).sum % n

Proof state:
s : Multiset ℕ
n : ℕ
⊢ s.sum % n = (map (fun x => x % n) s).sum % n

Tactic:
induction s using Multiset.induction <;> simp [Nat.add_mod, *]

Result:
no goals